Information Technology Reference
In-Depth Information
2
The Language
We introduce here the “mathematical” version of a stripped-down Handel-C,
which albeit simpler, has all the essential features of the full language.
2.1
Syntax
We have variables ( x
Var ), and we assume the existence of an expression syn-
tax ( e
Exp ) whose details need not concern us here. We also have identifiers
for channels ( c
Ch ), and we consider all the above as having either boolean or
integer type, and occasionally use b to denote a boolean-valued expression. We
also have the notion of guards ( g ∈ Grd ), which denote the offering and accept-
ing of communication actions. Guards either denote a desire to perform output of
an expression's value along a channel ( c ! e ), to receive input via a channel into a
variable ( c ? x ), or a skip/default guard which always succeeds (!?).
g
G ::= c ? v
|
c ! e
|
!?
A syntax of a process p : Proc is as follows:
p ::= 0
|
1
|
x := e
|
p 1 ; p 2 |
p 1
p 2 |
p 1 b p 2 |
b
p
|
g i
p i i∈ 1 ...n
The last clause is shorthand for a list of guard-process pairs.
2.2
Behaviour
We can briefly summarise the behaviour of a Handel-C process as follows: 0 does
nothing, in zero time; 1 does nothing, but takes one clock cycle to do it; x := e
assigns the value of e into x , taking one clock cycle; ( p 1 ; p 2 ) first executes p 1 ,
and once it has terminated immediately starts p 2 ;( p 1
p 2 ) runs both p 1 and
p 2 in lock-step parallel, terminating when they have both finished; ( p 1 b p 2 )
evaluates b and executes p 1 immediately if b is True , otherwise it runs p 2 ;and
b ∗ P tests b and if True it runs P and then repeats, otherwise it terminates.
The
construct (“prialt”) is an ordered sequence of guard-process
pairs. Guards are either communication actions or a default guard to be activated
if no communication guard is active. The default guard, if present, must be last.
The sequence of guards in a prialt denotes that prialt 's priority preference,
considered as relative priority — i.e. it prefers its first guard to its second, its
second to its third, and so on.
Each guard is checked against the process environment to see if it is able to
execute. If no guards are so enabled, then the prialt blocks until the next clock
cycle when it tries again. If one or more guards are enabled, then the first such
in the list is executed, and then the corresponding process is executed. An input
guard ( c ? x ) is enabled if there is a corresponding output guard ( c ! e )insome
g i
p i
Search WWH ::




Custom Search