Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Last revision Both sides next revision | ||
language:langs:chp [2020/07/09 07:35] rajit [More on channel expressions and probes] |
language:langs:chp [2023/04/09 19:27] rajit [Arrays: dynamic v/s non-dynamic indices] |
||
---|---|---|---|
Line 2: | Line 2: | ||
The CHP sublanguage is an evolution of Dijkstra' | The CHP sublanguage is an evolution of Dijkstra' | ||
- | < | + | < |
chp { | chp { | ||
/* program goes here */ | /* program goes here */ | ||
Line 14: | Line 14: | ||
* '' | * '' | ||
- | * '' | + | * '' |
* '' | * '' | ||
* '' | * '' | ||
- | * '' | + | * '' |
- | * '' | + | * '' |
+ | |||
+ | ==== Typechecking ==== | ||
+ | |||
+ | Expressions are evaluated using the [[language: | ||
+ | |||
+ | Variables can be set via either assignment statements or via receive operations. When an integer variable of bit-width //w1// is set to an integer value of bitwidth //w2//, then | ||
+ | * If // | ||
+ | * If // | ||
+ | * If // | ||
+ | An integer cannot be assigned a Boolean value or vice versa. Explicit conversion via '' | ||
+ | |||
+ | The same rules outlined above apply to receive operations, where the value being assigned is the value received from the channel. To support int/bool conversion during a receive operation, we also support the following extended syntax: | ||
+ | * '' | ||
+ | * '' | ||
===== Composition operators ===== | ===== Composition operators ===== | ||
Line 24: | Line 38: | ||
Sequential composition uses the '';'' | Sequential composition uses the '';'' | ||
- | Parallel composition uses the '' | + | Since circuit instances implicitly run in parallel, |
- | + | ||
- | Internal parallelism where the two statements do not write a variable that is read by the other can use the '' | + | |
- | < | + | < |
x+,y+;z- | x+,y+;z- | ||
</ | </ | ||
This corresponds to setting '' | This corresponds to setting '' | ||
- | ==== Conditional execution ==== | + | ===== Conditional execution |
The selection statement uses the guarded command syntax. The statement | The selection statement uses the guarded command syntax. The statement | ||
- | < | + | < |
[ g1 -> S1 | [ g1 -> S1 | ||
[] g2 -> S2 | [] g2 -> S2 | ||
Line 49: | Line 61: | ||
Often a circuit simply waits for some condition to be true before proceeding. This would be written | Often a circuit simply waits for some condition to be true before proceeding. This would be written | ||
- | < | + | < |
[ cond -> skip ] | [ cond -> skip ] | ||
</ | </ | ||
This happens so often that there is syntactic sugar to support this particular construct, shown below: | This happens so often that there is syntactic sugar to support this particular construct, shown below: | ||
- | < | + | < |
- | [code] | + | [cond] |
</ | </ | ||
For example, | For example, | ||
- | < | + | < |
| | ||
</ | </ | ||
Line 65: | Line 77: | ||
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: | 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 | [| g1 -> S1 | ||
[] g2 -> S2 | [] g2 -> S2 | ||
Line 75: | Line 87: | ||
In the published literature, non-deterministic selections are usually written using a thin bar '' | In the published literature, non-deterministic selections are usually written using a thin bar '' | ||
- | ==== Loops ==== | + | ===== Arrays: dynamic v/s non-dynamic indices ===== |
+ | |||
+ | Suppose an array '' | ||
+ | <code act> | ||
+ | int x[10]; | ||
+ | </ | ||
+ | |||
+ | Now when '' | ||
+ | <code act> | ||
+ | chp { | ||
+ | ... | ||
+ | x[0] := x[0] + 1; | ||
+ | ... | ||
+ | } | ||
+ | </ | ||
+ | uses '' | ||
+ | <code act> | ||
+ | chp { | ||
+ | ... | ||
+ | x[i] := x[i] + 1; | ||
+ | ... | ||
+ | } | ||
+ | </ | ||
+ | uses '' | ||
+ | |||
+ | |||
+ | ===== Loops ===== | ||
Loops/ | Loops/ | ||
- | < | + | < |
*[ g1 -> S1 | *[ g1 -> S1 | ||
[] g2 -> S2 | [] g2 -> S2 | ||
Line 88: | Line 126: | ||
One of the most common cases in using loops is the infinite repetition. This is typically the " | One of the most common cases in using loops is the infinite repetition. This is typically the " | ||
- | < | + | < |
*[ true -> S ] | *[ true -> S ] | ||
</ | </ | ||
Since this is so common, the following syntactic sugar is provided to make this even more compact: | Since this is so common, the following syntactic sugar is provided to make this even more compact: | ||
- | < | + | < |
*[ S ] | *[ S ] | ||
</ | </ | ||
Using this, the classic greatest common divisor algorithm can be written as follows: | Using this, the classic greatest common divisor algorithm can be written as follows: | ||
- | < | + | < |
chp { | chp { | ||
*[ X?x,Y?y; | *[ X?x,Y?y; | ||
Line 110: | Line 148: | ||
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: | 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 ] | *[ S <- G ] | ||
</ | </ | ||
A do-while loop can have only one guard. This program executes '' | A do-while loop can have only one guard. This program executes '' | ||
+ | |||
+ | Loop guards can only use local variables. Hence, it is an error if a variable appearing in a loop guard is either (i) a global variable; or (ii) accessible via the port list of the process; or (iii) involves a channel probe. This ensures that loop guards cannot include any shared variables. | ||
+ | |||
+ | ===== Advanced expression syntax ===== | ||
==== Channels in expressions ==== | ==== Channels in expressions ==== | ||
Line 119: | Line 161: | ||
Channels can be used in expressions in two ways: | Channels can be used in expressions in two ways: | ||
* The //explicit probe// of a channel can be used using the syntax ''# | * The //explicit probe// of a channel can be used using the syntax ''# | ||
- | * The channel itself can be used within an expression. This is detailed below. | + | * 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: | 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 | *[ [| #A -> A?x | ||
[] #B -> B?x | [] #B -> B?x | ||
Line 130: | Line 172: | ||
</ | </ | ||
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 '' | 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 -> A?x | *[[#A -> A?x | ||
[]#B -> B?x | []#B -> B?x | ||
Line 143: | Line 185: | ||
If '' | If '' | ||
- | < | + | < |
- | *[[A=3 -> X!true; | + | [A=3 -> X!true; |
- | | + | []A!=3 -> X!false; |
- | ] | + | ] |
</ | </ | ||
Here, '' | Here, '' | ||
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 '' | 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 '' | ||
- | < | + | < |
x:=A | x:=A | ||
</ | </ | ||
might fail, the following alternative will not. | might fail, the following alternative will not. | ||
- | < | + | < |
[#A];x:=A | [#A];x:=A | ||
</ | </ | ||
+ | ==== Functions in expressions ==== | ||
+ | |||
+ | The CHP language supports functions in expressions. These functions can be templated, and must operate on '' | ||
==== More on channel expressions and probes ==== | ==== More on channel expressions and probes ==== | ||
The interaction of Boolean expressions, | The interaction of Boolean expressions, | ||
- | < | + | < |
[ #A | #B -> ... | [ #A | #B -> ... | ||
[] #C -> ... | [] #C -> ... | ||
Line 168: | Line 213: | ||
</ | </ | ||
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 ''# | 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=0 | B=0 -> ... | [ A=0 | B=0 -> ... | ||
[] #C -> ... | [] #C -> ... | ||
Line 176: | Line 221: | ||
What about: | What about: | ||
- | < | + | < |
[| ~(#A | ~#B) -> ... | [| ~(#A | ~#B) -> ... | ||
[] #C -> ... | [] #C -> ... | ||
|] | |] | ||
</ | </ | ||
- | In the first guard, there is a negated probe on '' | + | In the first guard, there is a negated probe on '' |
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. | 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? ^ | ^ Original expression ^ Elaborated expression ^ Negated probe? ^ | ||
- | | '' | + | | '' |
| '' | | '' | ||
| '' | | '' | ||
Line 193: | Line 238: | ||
| '' | | '' | ||
| '' | | '' | ||
+ | |||
+ | 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, | In the case of integer expressions, | ||
Line 199: | Line 246: | ||
| '' | | '' | ||
| '' | | '' | ||
+ | | '' | ||
- | Note that since probes are only allowed in guards of selection statements, negated probes are not possible in other contexts. | + | Essentially every channel variable '' |
+ | ===== Advanced channels ===== | ||
+ | ==== Exchange channels ==== | ||
+ | Exchange channels are those where data is exchanged between sender and receiver, and this is indicated directly in the channel type. The syntax for exchange channels is: | ||
+ | * '' | ||
+ | * '' | ||
+ | In this case, we assume that the exchange send will initiate the operation, and hence only the exchange receive can be probed. This doesn' | ||
+ | ==== Split synchronization ==== | ||
+ | Four-phase handshake channels involve two synchronizations. If you need to make this explicit in the CHP, the '' | ||
+ | |||
+ | ===== Syntactic replication ===== | ||
+ | |||
+ | There are three common uses of syntactic replication in CHP, and the language has syntactic support for them. The first two correspond to scenarios where you have a number of items separated by semicolon or comma. The syntax for this follows the generic template for [[language: | ||
+ | |||
+ | <code act> | ||
+ | (; i : 4 : x[i] := 0) | ||
+ | </ | ||
+ | |||
+ | corresponds to | ||
+ | |||
+ | <code act> | ||
+ | x[0] := 0; x[1] := 0; x[2] := 0; x[3] := 0 | ||
+ | </ | ||
+ | |||
+ | Note the missing trailing semicolon. Following this with another statement in sequence would be written | ||
+ | |||
+ | <code act> | ||
+ | (; i : 4 : x[i] := 0 ); | ||
+ | x[0] := 1 - x[1] | ||
+ | </ | ||
+ | |||
+ | Similarly, the semicolon can be replaced with a comma to specify parallel execution. | ||
+ | |||
+ | Syntactic replication is also supported for guarded commands. | ||
+ | |||
+ | <code act> | ||
+ | [ v = 0 -> x := x - v | ||
+ | [] ( [] i : 3 : v = i+2 -> x := x + i | ||
+ | ] | ||
+ | </ | ||
+ | |||
+ | is the same as | ||
+ | |||
+ | <code act> | ||
+ | [ v = 0 -> x := x - v | ||
+ | [] v = 0+2 -> x := x + 0 | ||
+ | [] v = 1+2 -> x := x + 1 | ||
+ | [] v = 2+2 -> x := x + 2 | ||
+ | ] | ||
+ | </ | ||
+ | |||
+ | This construct can be used to work around one of the current restrictions of CHP. A natural way to write a merge process in ACT is: | ||
+ | <code act> | ||
+ | *[ C?c; I[c]?d; O!d ] | ||
+ | </ | ||
+ | This will error out because the CHP has a //dynamic// channel access---i.e. the channel accessed is computed at run-time. While this is supported for int arrays, for example, that is because there is an efficient compilation mechanism for large int arrays (via memory macros). To work around this restriction, | ||
+ | <code act> | ||
+ | *[ C?c; [ ([] i : N : c = i -> I[i]?d) ]; O!d ] | ||
+ | </ | ||
+ | where '' | ||
+ | |||
+ | ====== The chp-txt sublanguage ====== | ||
+ | |||
+ | Since the CHP syntax is quite different from commonly used programming languages, we have provided a variation called '' | ||
+ | <code act> | ||
+ | chp-txt { | ||
+ | /* chp-txt program goes here */ | ||
+ | } | ||
+ | </ | ||
+ | The basic statements, expression syntax, etc. remains unchanged from the CHP language. What is different is the syntax for loops, selection statements, and short-cuts, plus additional syntax for baseline send and receive operations. | ||
+ | ==== Send and receive ==== | ||
+ | |||
+ | In addition to the syntax | ||
+ | <code act> | ||
+ | X!e | ||
+ | </ | ||
+ | for a send operation, '' | ||
+ | <code act> | ||
+ | send (X, e) | ||
+ | </ | ||
+ | In addition to the syntax | ||
+ | <code act> | ||
+ | X?v | ||
+ | </ | ||
+ | for a receive operation, '' | ||
+ | <code act> | ||
+ | recv (X, v) | ||
+ | </ | ||
+ | |||
+ | |||
+ | ==== Conditionals | ||
+ | |||
+ | The selection statement | ||
+ | <code act> | ||
+ | [ g1 -> S1 [] g2 -> S2 [] g3 -> S3 ... [] gn -> Sn ] | ||
+ | </ | ||
+ | is written as follows in '' | ||
+ | <code act> | ||
+ | select { | ||
+ | case g1 : S1; | ||
+ | case g2 : S2; | ||
+ | ... | ||
+ | case gn: Sn | ||
+ | } | ||
+ | </ | ||
+ | The '' | ||
+ | |||
+ | A non-deterministic statement is written the same way, except the keyword '' | ||
+ | |||
+ | Waiting for a condition is a commonly used operation. This was written in chp as '' | ||
+ | <code act> | ||
+ | wait-for (condition) | ||
+ | </ | ||
+ | |||
+ | ==== Loops ==== | ||
+ | |||
+ | A simple while loop written in CHP as | ||
+ | <code act> | ||
+ | *[ G -> S ] | ||
+ | </ | ||
+ | is written in '' | ||
+ | <code act> | ||
+ | while (G) { | ||
+ | S | ||
+ | } | ||
+ | </ | ||
+ | A while loop with multiple guards of the form | ||
+ | <code act> | ||
+ | *[ G1 -> S1 [] G2 -> S2 ... [] Gn -> Sn ] | ||
+ | </ | ||
+ | is written as | ||
+ | <code act> | ||
+ | while { | ||
+ | case G1 : S1; | ||
+ | case G2 : S2; | ||
+ | ... | ||
+ | case Gn : Sn | ||
+ | } | ||
+ | </ | ||
+ | A do-loop is written: | ||
+ | <code act> | ||
+ | do { | ||
+ | S | ||
+ | } while (G) | ||
+ | </ | ||
+ | Finally, an infinite loop is written: | ||
+ | <code act> | ||
+ | forever { | ||
+ | S | ||
+ | } | ||
+ | </ | ||
+ | |||
+ | ==== An example ==== | ||
+ | |||
+ | The CHP program: | ||
+ | <code act> | ||
+ | chp { | ||
+ | *[ L?x; R!x ] | ||
+ | } | ||
+ | </ | ||
+ | would be written in '' | ||
+ | <code act> | ||
+ | chp-txt { | ||
+ | | ||
+ | recv (L, x); send (R, x) | ||
+ | } | ||
+ | } | ||
+ | </ | ||
+ | |||
+ | The CHP program: | ||
+ | <code act> | ||
+ | chp { | ||
+ | *[ L?x; [ x > 0 -> R!x [] else -> skip ] ] | ||
+ | } | ||
+ | </ | ||
+ | would be written | ||
+ | <code act> | ||
+ | chp-txt { | ||
+ | | ||
+ | recv (L, x); | ||
+ | select { | ||
+ | case x > 0 : send (R, x); | ||
+ | else : skip | ||
+ | } | ||
+ | } | ||
+ | } | ||
+ | </ |