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

Priority in concurrent processes is dicult to treat formally but many ex-
amples abound, in both the CSP setting [14,15,16,17]. and in the more general
process algebra areas [18,19,20]. The CSP treatment either fails to handle re-
cursion, or is too complex and general, while the more general process algebra
work is closer to what is required. Unfortunately, priority in Handel-C does
not fit neatly into the priority schemes that have been considered, as described
in [20]
Other work involving formal techniques and Handel-C has been reported,
and includes the use of the Ponder policy specification language [21] as a ba-
sis for implementing firewalls [22], as well as techniques for performing behav-
ioural transformations from Haskell programs into Handel-C implementations
[23]. Beyond the scope of Handel-C, there is considerable work on using formal
techniques to develop safety-critical embedded systems, of which the languages
Esterel [24,25,26] and Lustre [27,28] are two key examples.

4O rv ewof prialt Semantics

We present here a brief overview of the prialt semantics presented in [5], with an
explanation of how it can be interfaced with the denotational semantics described
later on in this paper.
In any given clock cycle, there will be zero or more prialt s commencing
execution. A guard is deemed to be potentially active if elsewhere there is a
complementary guard in some other prialt active during the same clock cy-
cle. The process of determining which guards, if any, become active, is called
Resolution .
In [12] resolution is viewed formally as a function Resolve that takes a set
of Prialt Requests ( PriSet ), and returns a pair called a Resolution ( Resltn ),
consisting of an Channel-Prialt Map ( CPMap )andthesetof prialt sthathave
remained blocked.

Prialt
CPMap = Ch

PriSet = P

PriSet
Resltn = CPMap

→

× PriSet

Resolve : PriSet → Resltn

A Prialt Request is simply modelled as a sequence of guards, i.e simply as the
corresponding prialt -statement with the continuation processes stripped out.
The Channel-Prialt Map identifies which channels are going to be active and
maps them to those prialt s which will participate in communication over that
channel.
In order to model the semantics of prialt , we view a clock-cycle as being
composed of four phases: selection ( sel ); request ( req ); resolve ( res ); and action
( act ). During the selection phase, flow of control decisions are taken by evaluat-
ing conditions for if-statements and while-loops. During the request phase, any
prialt s which have been selected lodge their prioritised communication requests