Information Technology Reference
In-Depth Information
Application Operation - Non-Fresh Once Routine
f
∈
ROUTINE
∧
f
.
is once
∧¬
σ
.
is fresh
(
p
,
f
)
σ
.
handler
(
r
0
)=
p
¬
σ
.
locks passed
(
p
)
σ
de f
=
σ
.
pass locks
(
q
,
p
,
l
)
.
push env with feature
(
p
,
f
,
r
0
,
(
r
1
,...,
r
n
))
ais fresh
Γ
p
::
apply
(
a
,
r
0
,
f
,
(
r
1
,...,
r
n
)
,
q
,
l
)
;
s
p
,
σ
→
p
::
provided
f
.
class type
.
inv exists
∧
f
.
exported
then
eval
(
a
,
f
.
class type
.
inv
)
;
wait
(
a
)
else
nop
end
;
provided
f
∈
FUNCTION
then
return
(
a
,
σ
.
once result
(
p
,
f
)
,
q
)
else
return
(
a
,
q
)
end
;
s
p
,
σ
Application Operation - Attribute
f
∈
ATTRIBUTE
σ
.
handler
(
r
0
)=
p
¬
σ
.
locks passed
(
p
)
σ
de f
=
σ
.
pass locks
(
q
,
p
,
l
)
.
push env with feature
(
p
,
f
,
r
0
,
())
a
is f resh
Γ
p
::
apply
(
a
,
r
0
,
f
,
()
,
q
,
l
)
;
s
p
,
σ
→
p
::
eval
(
a
,
f
)
;
wait
(
a
)
;
return
(
a
,
a
.
data
,
q
)
;
s
p
,
σ
.
(
,...,
)
Creation instructions.
A creation instruction has the form
create
b
f
e
1
e
n
where
b
is the target entity,
f
is the creation procedure, and
e
1
,...,
e
n
are the actual arguments.
Assume that
b
is of type
(
d
,
g
,
c
)
. A processor
p
that executes this instruction takes the
following steps:
1. Processor
q
creation.
-
If
b
is separate, i.e.,
g
, then create a new processor.
-
If
b
has an explicit processor specification, i.e.,
g
=
=
α
,then
•
take the processor denoted by
α
if it already exists.
•
create a new processor if the processor denoted by
α
does not exist yet.
,thentake
p
.
2. Locking. Lock the request queue of
q
if the following conditions hold:
-
Processor
p
and processor
q
are different.
-
Processor
p
does not have
q
's request queue lock.
-
Processor
q
does not have
p
's request queue lock.
-
If
b
is non-separate, i.e.,
g
=
•
Search WWH ::
Custom Search