Information Technology Reference
In-Depth Information
precondition as a wait condition. It goes through a number of iterations. Each iteration
obtains the request queue locks and then evaluates the precondition. If the precondition
is satisfied, then the
check pre and lock rqs
operation finishes. Otherwise it unlocks
the request queues and then starts a new iteration. If the
check pre and lock rqs
operation finishes,
p
can be assured that it obtained all the request queue locks and the
precondition holds.
Check Postcondition and Unlock Request Queues Operation
q
de f
=
{
q
1
,...,
q
m
}
p
∈
q
{
e
0
}∪
i
=
0
...
n
targets
(
e
i
)
if e
=
e
0
.
w
(
e
1
,...,
e
n
)
{}
de f
=
targets
(
e
)
otherwise
i
=
1
...
n
{
(
e
i
,
w
,
i
)
}∪
args
(
e
i
)
if e
=
e
0
.
w
(
e
1
,...,
e
n
)
{}
de f
=
args
(
e
)
otherwise
⎨
⎩
if
q
=
{}∧
∀
x
∈
targets
(
f
.
post
)
:
(
Γ
σ
.
handler
(
σ
.
val
(
p
,
controlling entity
(
x
)
.
name
))
∈
q
)
∧
¬∃
(
x
,
y
,
z
)
∈
args
(
f
.
post
)
,
t
,
h
,
c
:
(
Γ
x
:
t
∧
controlled
(
t
)
∧
y
.
formals
(
z
)
:
(
!
,
h
,
c
)
∧
c
.
is ref
)
then
q
otherwise
{
p
}
de f
∈
g
0
de f
=
q
\
g
0
{
g
1
,...,
g
j
}
ais fresh
Γ
p
::
check post and unlock rqs
(
{
q
1
,...,
q
m
},
f
)
;
s
p
,
σ
→
p
::
provided
f
.
post exists
∧
g
0
=
p
then
issue
(
g
0
,
execute delegated
(
eval
(
a
,
f
.
post
)
;
wait
(
a
)
;
issue
(
g
1
,
unlock
)
;
...
;
issue
(
g
j
,
unlock
)
,
σ
.
envs
(
p
)
.
top
, {
q
1
,...,
q
m
}
)
;
unlock
)
;
pop obtained rq locks
else
provided
f
.
post exists
then
eval
(
a
,
f
.
post
)
;
wait
(
a
)
else
nop
end
;
issue
(
q
1
,
unlock
)
;
...
;
issue
(
q
m
,
unlock
)
;
pop obtained rq locks
end
;
s
p
,
σ
Search WWH ::
Custom Search