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