Information Technology Reference
In-Depth Information
Loop Instruction
ais fresh
Γ
p
::
until
e
loop
s
l
end
;
s
p
,
σ
→
p
::
eval
(
a
,
e
)
;
wait
(
a
)
;
provided
a
.
data
then
nop
else
s
l
;
until
e
loop
s
l
end
end
;
s
p
,
σ
Assignment instructions.
e
assigns the value of the
expression
e
to the entity
b
. The instruction first evaluates the expression
e
and then
waits for a notification on a fresh channel
a
. Once it gets this notification, it uses the
write
operation to set the value to the entity
b
.
An assignment instruction
b
:
=
Assignment
ais fresh
Γ
p
::
b
:
=
e
;
s
p
,
σ
→
p
::
eval
(
a
,
e
)
;
wait
(
a
)
;
write
(
b
.
name
,
a
.
data
)
;
s
p
,
σ
5.5
Termination
The system terminates when it reaches a configuration where all action queues are
empty, i.e., when there is no more work to do.
6Con lu ion
In this paper we have presented a formal specification of the SCOOP model, based
on operational semantics. We have demonstrated that this level of rigor is necessary if
the specification is to be used as a guideline for an implementation. In particular, we
were able to clarify a number of omissions and ambiguities in the available informal
specification, which had gone undetected in other formalizations:
-
Are processor locks fine-grained enough? We require request queue locks and call
stack locks.
-
Which locks must be passed? Which locks can be passed? We pass all the locks we
actually have. We pass these locks both for normal lock passing and for separate
callbacks.
-
How do we move object structures from one processor to another processor without
violating the invariant? The deep import operation must be used.
-
When do we set the status of a fresh once routine to non-fresh? The status of the
once routine must be set to non-fresh before deep importing.
-
When can a postcondition be evaluated asynchronously? The postcondition can be
evaluated asynchronously if every feature call in the postcondition only requires a
lock that was obtained in the synchronization step and if the postcondition does not
involve lock passing.
Search WWH ::
Custom Search