Information Technology Reference
In-Depth Information
environment and
to
g
0
.After
g
0
performed the delegated execution, it can
unlock its own request queue. In the meantime, processor
p
removes
{
q
1
,...,
q
m
}
from
its obtained request queue locks to enable
g
0
to proceed with the delegated execution.
The
return
operation comes in two variants: one for queries and one for commands.
{
q
1
,...,
q
m
}
Return Operation - Query
⎨
⎩
if r
=
void
∧
σ
.
ref obj
(
r
)
.
class type
.
is exp
∧
σ
.
handler
(
r
)
=
q
(
σ
x
,
σ
x
.
last imported ref
)
where
σ
x
de f
de f
=
(
σ
,
r
)
=
σ
.
deep import
(
q
,
r
)
otherwise
(
σ
,
r
)
de f
=
σ
.
pop env
(
p
)
.
revoke locks
(
q
,
p
)
Γ
p
::
return
(
a
,
r
,
q
)
;
s
p
,
σ
→
p
::
result
(
a
,
r
)
;
s
p
,
σ
Return Operation - Command
σ
de f
=
σ
.
pop env
(
p
)
.
revoke locks
(
q
,
p
)
Γ
p
::
return
(
a
,
q
)
;
s
p
,
σ
→
p
::
provided
σ
.
locks passed
(
q
)
then notify
(
a
)
else nop end
;
s
p
,
σ
σ
The variant for queries returns the result and the locks. The variant for commands only
returns the locks. Both variants take a channel
a
and the caller processor
q
. For queries,
the channel is used to return the result. For this purpose, the operation takes a reference
r
that points to the result. Processor
q
is waiting for this result on channel
a
. This can be
seen in the
call
operation, which issues an
apply
operation and a subsequent
wait
(
)
operation. The
apply
operation calls the
return
operation with the same channel
a
.
To return the result to
q
, processor
p
executes a
result
on
a
. The value to be returned
is not always
r
directly. If
r
points to an object of expanded class type and
q
a
p
,then
q
must deep import the object. In all other cases,
q
can take
r
as the return value. An
explanation why the deep import operation is necessary can be found in Sec. 4.6. For
commands, the channel is used to signal to
q
that the locks have been returned in case
q
passed its locks. This can be determined by looking at the state:
=
.
In both variants of the
return
operation,
p
removes the passed locks from the stacks
of retrieved locks. In case
q
did not pass any locks, the removed entries might be the
empty set. Processor
p
also removes its top environment because this environment is no
longer needed. In case of an asynchronous postcondition evaluation, this environment
temporarily gets delegated to the evaluating processor.
Until now, the discussion left out the non-fresh once routines and the attributes.
Non-fresh once functions already have a result. The
apply
operation just needs to get
this result from the state and return it. For non-fresh once procedures it does not even
have to do this. The only obligation is the evaluation of the invariant. The evaluation
of the invariant requires the call stack lock of
p
. This lock is given if the condition
¬
σ
.
σ
.
locks passed
(
q
)
holds. For attributes, note that an instance of
ATTRIBUTE
is also
an instance of
EXPRESSION
. Hence, the operation evaluates the attribute expression
and returns the result of the evaluation. The invariant does not have to be evaluated in
this case.
locks passed
(
p
)
Search WWH ::
Custom Search