Information Technology Reference
In-Depth Information
We can now give the semantics of the additional constructs:
[[ rq
g i
]]
=
{
mk req (
{
B
→{
g i }}
)
}
[[ wait
g i
]]
= fix W
•{
mk res (
¬
w
g i
)
}
( w
g i
:: act ([[ rq
g i
]] 9 W )
=
[[ a
g i
[ p i ]]]
i {
( a
g i
= i ) :: res [[ p i ]]
}
The request statement is simply an update of the state's “ B ' component, tagged
as occurring during the req phase. The case-statement simply prepends a guarded
action asserting that e = i to the traces associated with process p i ,suchachoice
being made during the res phase.
The wait
statement is a looping construct, so it has a fixpoint defini-
tion as expected. It would seem obvious that wait
g i
g i
should be the same as
w
), but it is necessary to keep it separate, because not only do
the true and false branches of the wait statement not occur in the sel phase, but
in fact they occur in different phases: the terminating guarded action (
g i
( 1 ; rq
g i
¬
w
g i
)
occurs during the res phase; while the continuation guarded action ( w
g i
)oc-
curs during the act phase.
The reason for this is the same as that encountered in the operational seman-
tics, namely that the decision to end waiting can be made as soon as a prialt
becomes unblocked (during some some res phase), but the decision to wait until
the next clock cycle to try again needs to be deferred until no more sel - req - res
micro-cycles can occur, i.e. once the act phase has been reached. This is because
a subsequent round of request and resolution, caused by a prialt in some default
guard, may cause a blocked prialt to become unblocked. The converse never
happens: once a prialt is unblocked in one microcycle, it can never become
blocked again subsequently.
This means that the Exhaustiveness and Exclusivity healthiness conditions
aren't quite adhered to at this point, as the conditions
do
not occur at the same point in the traces. In fact the latter is delayed until the
act phase. The weakening that we allow is that this works because while the act
condition occurs later in the trace, no events of any significance occur in that
trace from the point in the res phase where w
¬
w
g i
and w
g i
g i
could return false ,uptothe
act point where the predicate can return true .
7.2
Examples
We now present a few small examples simply to show the semantics at work.
In order to keep expressions readable and manageable, we introduce the fol-
lowing shorthand: (i) for (
, x
e )wesimplywrite
{
x
e
}
; (ii) and for
mks req (
{
B
→{
g i }}
)weuse req
g i
. Rather than showing the slot and micro-
cycle structure explicitly, we simply list the actions separated by commas, and
use to to mark the slot boundaries (i.e clock ticks). So
Search WWH ::




Custom Search