This is an old revision of the document!


The chp sublanguage

The CHP sublanguage is an evolution of Dijkstra's guarded commands notation and Hoare's CSP. It is a programming notation augmented with send/receive primitives for communication and parallel composition. A chp program is specified in ACT as follows:

chp { 
   /* program goes here */
}

Basic statements

The basic statements in the language are:

  • skip: does nothing
  • x:=E: assignment statement; the expression E is evaluated, and the result is assigned to variable x
  • x+: short-hand for x:=true
  • x-: short-hand for x:=false
  • X!e: communication action (send). The expression e is evaluated and sent over channel X. Communication is blocking (slack zero).
  • X?v: communication action (receive). v is a variable, and the value received on channel X is assigned to v

Composition operators

Sequential composition uses the ; separator. So S;T is the statement S followed by the statement T, like many standard programming languages.

Since circuit instances implicitly run in parallel, there's no actual requirement for an explicit parallel composition operator at the level of circuit modules. Internal parallelism where the two statements do not write a variable that is read by the other can use the , separator. The comma has a higher binding power compared to semicolon.

  x+,y+;z-

This corresponds to setting x and y to true in parallel. Only after both are complete, z is set to false.

Conditional execution

The selection statement uses the guarded command syntax. The statement

 [ g1 -> S1
 [] g2 -> S2
 [] g3 -> S3
 ...
 [] gn -> Sn
 ]

is a deterministic selection statement. g1 through gn are Boolean expressions (guards), and S1 through Sn are statements. Operationally, the selection statement waits for one of the guards to be true, and then executes the corresponding statement. It can be viewed as a generalized if-statement or a case statement in a traditional programming language. The primary difference is that if all the guards are false, the program waits for one of the guards to become true.

The statement is deterministic, because the syntax means that the programmer asserts that at most one guard can be true when control reaches the selection statement.

Often a circuit simply waits for some condition to be true before proceeding. This would be written

[ cond -> skip ]

This happens so often that there is syntactic sugar to support this particular construct, shown below:

[code]

For example,

 [xi];xo+

is a program fragment that waits for xi to become true, and then sets xo to true.

In the deterministic selection, the last guard can be the keyword else; this form of the deterministic selection is guaranteed to be non-blocking, and else is simply short-hand for the condition that all the other guards are false.

Sometimes the selection statement can have multiple guards that are true. This requires the use of a non-deterministic circuit (an arbiter) to resolve the choice, and introduces implementation overhead. Hence, the programmer is required to use different syntax for non-deterministic selections to make this overhead explicit and visible. A non-deterministic selection is written as follows:

[| g1 -> S1
[] g2 -> S2 
...
[] gn -> Sn
|]

In the published literature, non-deterministic selections are usually written using a thin bar | rather than the thick bar []. However, this can create some ambiguities in parsing. For example, consider the statement [ a → y:=b | c | d → skip ]. This can be parsed in a number of ways, and it is not clear which one was the intended option.

Loops

Loops/repetitions use a syntax similar to selections, with the addition of the Kleene star.

*[ g1 -> S1
[] g2 -> S2
 ...
[] gn -> Sn
]

The behavior of this loop is the following. If any of the guards is true, then the corresponding statement is executed and the loop repeats. If all the guards are false, the loop terminates. Note that loops in ACT only support deterministic choice.

One of the most common cases in using loops is the infinite repetition. This is typically the “outer” loop in programs that describe most circuits. This would be written

*[ true -> S ]

Since this is so common, the following syntactic sugar is provided to make this even more compact:

*[ S ]

Using this, the classic greatest common divisor algorithm can be written as follows:

chp { 
 *[ X?x,Y?y;
   *[ x > y -> x := x - y
   [] x < y -> y := y - x
    ];
    O!x
  ]
}

One last supported construct is a do-while loop. The main difference between the standard loop and the do-loop is that we are guaranteed that the loop will execute at least one iteration. This information can be useful during circuit synthesis. The syntax for a do-while loop is:

*[ S <- G ]

A do-while loop can have only one guard. This program executes S, and then evaluates the guard G. If G is true, then the loop repeats; otherwise, the loop terminates.

Channels in expressions

Channels can be used in expressions in two ways:

  • The explicit probe of a channel can be used using the syntax #A. The probe is a Boolean expression that indicates that there is a communication action pending/being attempted on the channel. The explicit probe is only permitted in the guards of selection statements.
  • The channel itself can be used within an expression. This is detailed below. Channel expressions are not permitted in loop guards.

The following program takes the arriving data on two different input channels, and merges them into a data sequence on its output channel:

*[ [| #A -> A?x
   [] #B -> B?x
   |];
   OUT!x
 ]

This is sometimes called a non-deterministic merge. Note that a channel can be probed at either end (i.e. the sender end or the receiver end can probe the channel), but not at both. If we knew that the inputs on A and B are guaranteed to be mutually exclusive, then this can be written

*[[#A -> A?x
  []#B -> B?x
  ]; 
  OUT!x
 ]

and would lead to a more efficient circuit.

Negated probes need some care. The choice between #A and ~#A is actually non-deterministic, because the value of the probe can change from false to true at any time. In fact, implementing complex negated probes can be more challenging than a simple non-deterministic selection since negated probe expressions are non-monotonic. Most compilers will only provide limited support for negated probes.

If A is an input port, then A can participate in a channel expression. For example, we can write:

*[[A=3 -> X!true;A?x
 []A!=3 -> X!false;A?x
 ]

Here, A=3 is a channel expression. This has the following meaning: first, wait for a value to be pending on the input channel A; then compare it to 3. In other words, this expression includes an implicit probe. It also permits the pending value on A to be inspected. Note that A!=3 also includes waiting for a value to be pending on the input channel, and is not the literal negation of the condition corresponding to A=3. In other words, in the program fragment above, the selection statement should be read: wait for a value to be pending on input channel A; if the value is 3, do the first set of statements; otherwise pick the second set of statements.

Channel expressions can be used in any context that includes an expression (e.g. assignment statements, send operations). However, evaluating the expression will result in an error if the probe of the appropriate channels is false; i.e. the assignment statement must be non-blocking. So, if A is an input channel, the statement

x:=A

might fail, the following alternative will not.

[#A];x:=A

More on channel expressions and probes

The interaction of Boolean expressions, probes, and channel expressions can be a bit tricky. For example, consider the following guards:

[ #A | #B -> ... 
[] #C -> ...
]

The standard way ORs (and AND) operators are viewed is via short-circuit evaluation. Hence, the first guard can evaluate to true as soon as either #A or #B is true. Instead, suppose we had:

[ A=0 | B=0 -> ...
[] #C -> ...
]

Now can the first guard evaluate to true if #A is true and the pending value on A is zero? The CHP language is defined so that this is indeed the case, otherwise this would end up being inconsistent with the short-circuit semantics.

What about:

[| ~(#A | ~#B) -> ...
[] #C -> ...
|]

In the first guard, there is a negated probe on A and an ordinary probe on B. Hence, to understand negated probes, short circuit evaluation and channel expressions, it is best to first convert the Boolean expression into negation-normal form (this is the form where negations can only appear on literals). Note that since we can mix Boolean and integer expressions, a literal might be say a comparison between two integer expressions.

Channel expressions can be handled using a combination of short-circuit evaluation and the explicit introduction of a probe. For each literal, if the literal involves a channel expression, then the literal is augmented with a conjunction of the probes needed to evaluate the literal. To see how this works, the following shows a number of channel expressions and their modified versions that make all the probes explicit. We use upper-case variables for channels, and lower-case variables for variables.

Original expression Elaborated expression Negated probe?
~(#A | ~#B) ~#A | #B On A
A = x #A & (A = x) N/A
~(A = x) #A & (A != x) N/A
(A = B) | (A = C) #A & #B & (A=B) | #A & #C & (A = C) N/A
x > 0 | x = A x > 0 | #A & (x=A) N/A
~(x = 0 | x = A) x != 0 & #A & (x != A) N/A
~(x = 0 | #A & (x=A)) x != 0 & (~#A | #A & (x != A)) On A

Note that since using a channel variable is an implicit use of the probe, channel variable expressions are disallowed in the guards of loops.

In the case of integer expressions, the situation can be handled as follows. ERR is used to denote an error.

Original expression Elaborated expression
x + B x + (#B ? B : ERR)
A * B + w (#A ? A : ERR) * (#B ? B : ERR) + w
A > B ? w : B + C ( (#A ? A : ERR) > (#B ? B : ERR) ) ? w : (#B ? B : ERR) + (#C ? C : ERR)

Essentially every channel variable V can be translated into (#V ? V : ERR). Note that this is a different translation compared to guards. Note that since probes are only allowed in guards of selection statements, negated probes are not possible in other contexts.