Information Technology Reference
In-Depth Information
Wait and Result Operation - Non-Separate
Γ
p
::
result
(
a
,
r
)
;
s
w
;
wait
(
a
)
;
s
p
,
σ
→
p
::
s
w
;
s
p
[
r
/
a
.
data
]
,
σ
Wait and Notify Operation - Non-Separate
Γ
p
::
notify
(
a
)
;
s
w
;
wait
(
a
)
;
s
p
,
σ
→
p
::
s
w
;
s
p
,
σ
In the separate case, one processor has a
result
(
a
,
r
)
or a
notify
(
a
)
operation at the
beginning of its action queue and a different processor has a
wait
(
a
)
somewhere in
its action queue. In this situation, the
wait
(
can be
removed from the action queues. In case the notification has a value, the value can be
installed in the statements
s
p
,afterthe
wait
(
a
)
,
result
(
a
,
r
)
,and
notify
(
a
)
a
)
operation.
Wait and Result Operation - Separate
Γ
p
::
s
w
;
wait
(
a
)
;
s
p
|
q
::
result
(
a
,
r
)
;
s
q
,
σ
→
p
::
s
w
;
s
p
[
r
/
a
.
data
]
|
q
::
s
q
,
σ
Wait and Notify Operation - Separate
Γ
p
::
s
w
;
wait
(
a
)
;
s
p
|
q
::
notify
(
a
)
;
s
q
,
σ
→
p
::
s
w
;
s
p
|
q
::
s
q
,
σ
The operations presented here must be used so that each
wait
operation can be resolved
with exactly one
result
or
notify
operation. To define this condition more precisely,
we define that one statement
s
1
weakly precedes a statement
s
2
if and only if
s
1
occurs
earlier than
s
2
in the same action queue or
s
1
and
s
2
occur in different action queues.
One statement
s
1
strongly precedes a statement
s
1
if and only if
s
1
occurs earlier than
s
2
in the same action queue. With these definitions, the condition says:
-
For each
wait
(
a
)
operation there must be either exactly one
result
(
a
,
r
)
or ex-
actly one
notify
(
a
)
operation.
-
For each
result
(
a
,
r
)
or
notify
(
a
)
operation there must be exactly one
wait
(
a
)
operation.
-
Each
result
(
a
,
r
)
or
notify
(
a
)
operation weakly precedes the
wait
(
a
)
operation.
Expression evaluation mechanism.
An expression can either be a literal, an entity, or a
query call. The query call can contain actual arguments that are expressions themselves.
This section discusses the general mechanism to evaluate expressions. It focuses on the
general approach and defers the evaluation of particular expressions to later sections.
The operation
eval
(
)
operation determines the value
r
of the expression
e
and then sends a notification with
value
r
on channel
a
. This means that each
eval
(
a
,
e
)
takes a channel
a
and an expression
e
. Each
eval
(
a
,
e
a
,
e
)
operation creates a
result
(
a
,
r
)
operation in the action queue. It is therefore important to follow each
eval
(
a
,
e
)
opera-
tion with exactly one
wait
(
a
)
to receive the notification with the value.
Search WWH ::
Custom Search