Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
|
language:langs:chp [2021/12/29 15:47] rajit [More on channel expressions and probes] |
language:langs:chp [2022/05/13 08:48] rajit |
||
|---|---|---|---|
| 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 40: | Line 40: | ||
| Since circuit instances implicitly run in parallel, there' | Since circuit instances implicitly run in parallel, there' | ||
| - | < | + | < |
| x+,y+;z- | x+,y+;z- | ||
| </ | </ | ||
| Line 48: | Line 48: | ||
| 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 61: | 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 77: | 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 90: | Line 90: | ||
| Loops/ | Loops/ | ||
| - | < | + | < |
| *[ g1 -> S1 | *[ g1 -> S1 | ||
| [] g2 -> S2 | [] g2 -> S2 | ||
| Line 100: | Line 100: | ||
| 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 122: | Line 122: | ||
| 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. | ||
| ==== Channels in expressions ==== | ==== Channels in expressions ==== | ||
| Line 134: | Line 136: | ||
| 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 142: | Line 144: | ||
| </ | </ | ||
| 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 155: | Line 157: | ||
| If '' | If '' | ||
| - | < | + | < |
| *[[A=3 -> X!true;A?x | *[[A=3 -> X!true;A?x | ||
| | | ||
| Line 163: | Line 165: | ||
| 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 | ||
| </ | </ | ||
| Line 174: | Line 176: | ||
| The interaction of Boolean expressions, | The interaction of Boolean expressions, | ||
| - | < | + | < |
| [ #A | #B -> ... | [ #A | #B -> ... | ||
| [] #C -> ... | [] #C -> ... | ||
| Line 180: | Line 182: | ||
| </ | </ | ||
| 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 188: | Line 190: | ||
| What about: | What about: | ||
| - | < | + | < |
| [| ~(#A | ~#B) -> ... | [| ~(#A | ~#B) -> ... | ||
| [] #C -> ... | [] #C -> ... | ||