Information Technology Reference
In-Depth Information
Execute Delegated Operation
∀
x
∈{
q
1
,...,
q
m
}
:
¬∃
y
∈
σ
.
procs
:
σ
.
rq locks
(
y
)
.
has
(
x
)
∀
x
∈{
q
1
,...,
q
m
}
:
σ
.
rq locked
(
x
)
de f
=
σ
.
push env
(
p
,
x
)
.
delegate obtained rq locks
(
p
, {
q
1
,...,
q
m
}
)
Γ
p
::
execute delegated
(
s
w
,
x
, {
q
1
,...,
q
m
}
)
σ
;
s
p
,
σ
→
p
::
s
w
;
leave delegated
;
s
p
,
σ
Leave Delegated Execution Operation
¬
σ
.
envs
(
p
)
.
is empty
¬
σ
.
obtained rq locks
(
p
)
.
is empty
σ
de f
=
σ
.
pop env
(
p
)
.
pop obtained rq locks
(
p
)
Γ
p
::
leave delegated
;
s
p
,
σ
→
p
::
s
p
,
σ
Notification mechanism.
Processors can notify each other. A notification can option-
ally include a value. The formalization uses channels to describe such communication.
Channels are described in Milner's
π
-calculus [23]. In the
π
-calculus, the expression
c
P
denotes a process that is waiting for a notification sent on a channel
c
. Once the
notification has been received, the value of the notification is bound to the variable
x
and the process continues with the expression
P
. The notification comes from a process
that executes
cy
(
x
)
.
Q
to emit the value
y
on the channel
c
before executing
Q
.
The formalization reuses the channel idea in two flavors: once as a notification mech-
anism with a value and once as a notification mechanism without a value. A proces-
sor sends a notification with a value
r
over a channel
a
as it executes the operation
result
(
.
. Similarly, the process sends a notification without a value over a channel
a
by executing the operation
notify
(
a
,
r
)
. For both cases, any processor can wait for a
notification by executing the operation
wait
(
a
)
a
)
. In case a notification on a channel
a
carries a value, the value can be accessed with
a
data
. This way of accessing the value
of a channel is different from the way it is done in the
.
-calculus,
each value is bound to a variable. This formalization does not define a new variable for
the value. Instead, it uses
a
π
-calculus. In the
π
data
to identify the value of a channel
a
.
A number of inference rules describe the interaction between a processor that sent
a notification over a channel and a processor that is waiting for a notification over the
same channel. Two main cases can be distinguished: either a processor sends a noti-
fication to itself or it sends a notification to a different processor. The first case is the
non-separate case and the latter case is the separate case. In each of these two main
cases, the channel carries a notification with or without a value. For each of these sub
cases, there is one inference rule.
In the non-separate case, one processor has a
result
(
.
a
,
r
)
operation or a
notify
(
a
)
operation at the beginning of its action queue and a
wait
(
a
)
operation on the same
channel later in the action queue. In this case, the
wait
(
a
)
operation can be removed
along with the
result
(
operation. If the
channel carries a value, then the value must be installed on the processor, by substituting
all occurrences of
a
a
,
r
)
operation, respectively the
notify
(
a
)
.
data
with the posted value in all the statements
s
p
after the
wait
(
a
)
operation.
Search WWH ::
Custom Search