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

in a central location. Once all this has occurred, the resolve phase determines
which communication requests are going to be granted. In the action phase, all
the assignment statements selected earlier, and all the communication actions
just resolved, are carried out simultaneously. The clock tick signals the end of
the action phase.
The set of prialt s that are input to Resolve are those lodged centrally during
the request phase. Conceptually, resolution occurs at the transition between the
request and resolution phases and results in the two outputs as mentioned above.
During the resolution phase, the resulting channel-map and blocked prialt -sets
are examined to determine what activities will occur.
Let us consider an example involving default clauses in that manner that
causes most semantic diculty. This example has two prialt s in parallel, with
the second having a default clause which itself contains a statement that subse-
quently invokes a prialt :

c !66 → || d !99 →

0 , !?

→

( b

∗ P ; c ? x →

0 0 )

Let us consider the case where b happens to be false. Initially we have a situation
where there are no potentially active guards, so the first prialt blocks, while
the second immediately activates its default clause. The while-loop has a false
condition, so immediately terminates, and this introduces another prialt to the
mix. At this point the program has evolved to look like this:

c !66 → 0 || c ? x → 0

This requires us to lodge a new request, with the existing ones still in place,
and to re-perform the resolution step. As a result, channel c becomes active,
transferring value 66 across to variable x .
Prialts nested inside default clauses of other prialts may become active in the
same clock cycle as those enclosing prialts, which requires us to iterate the sel -
req - res loop several times, in any given clock cycle. Managing this micro-cycle
activity severely complicates the semantics 2 .

5 Semantic Framework

The “prialt-free” denotational semantics in [13], inspired by [29], was based on
the notion of “branching sequences” or trees, where non-branching sequences
denoted deterministic sequences of actions, and branching was used to model a
choice point, such as the conditions of a while-loop or if-statement.
However, this model becomes far too complex when faced with the need to
handle multiple choice points per clock-cycle, so the full semantics described here
is given in terms of sets of “typed assertion traces”. These are sets of sequences of
actions (state-transformers), each action typed according to the phase in which

2 Interestingly, the underlying hardware doesn't iterate, as it computes what is to be
active in any given clock cycle using combinatorial logic.