A Denotational Semantics for Handel-C - Formal Methods and Hybrid Real-Time Systems - page 47

other prialt executing at the same time, and vice versa . The default guard (!?) is
always enabled. The input ( c ? x ) and output ( c ! e ) guards perform their actions
taking one clock-cycle, while the default guard (!?) acts in “zero-time”, so the
subsequent process starts execution immediately. It is this “instant” execution
of !? guards that so complicates the formal semantics of Handel-C, as discussed
extensively in [5].

2.3 Restrictions
We have a mix of parallel processes and global shared variables, so Handel-C
has a restriction which states that no variable should ever be assigned to by
two different processes during one clock cycle. It is allowable to have different
processes write to the same variable on different clock cycles. The Handel-C
language reference manual [1] states that different parallel processes generally
should not write to the same variable, but that if they do, the programmer has
a proof obligation to show that these writes never occur during the same clock
cycle.
This extends to disallowing the simultaneous writing of two different values
to the same channel — however having multiple readers of a channel at any one
time is permitted.
Another key restriction imposed by Handel-C is that during any clock-cycle,
all the relative priorities of all prialt s executing during that cycle must be
consistent with one another in that no priority cycles are introduced when all
their preferences are merged.

3 Previous and Related Work

Early work on the formal semantics of Handel-C concentrated on a subset of the
language that did not contain the prialt construct [6,7]. The approach adopted
was in the style of the “Irish School” of the VDM [8] which drew its inspiration
from the pioneering work in VDM of Dines Bjorner and his colleagues [9].
However it soon became clear that prialt would have to be included. It
cannot be simulated using ordinary communication and switch statements, and
it has a number of effects on the overall semantics. Also, we viewed the task of
developing a formal semantics for Handel-C as being an true exercise in domain
modelling [10,11], as our intention was to model an existing artefact, warts and
all, rather than construct a nice simple well-behaved hardware process algebra.
A formal description of prialt resolution without consideration of default
clauses was presented in [12]. An initial denotational semantics was developed
[13] which incorporated this prialt resolution semantics. Then the prialt
model of [12] was then extended to handle default clauses properly and an op-
erational semantics for Handel-C incorporating this was developed [4,5]. The
operational semantics had to introduce a notion of prioritised transitions in or-
der to correctly capture the behaviour of default guards. This additional notion
of priority was completely different and orthogonal to the priorities expressed
by the prialt construct.