Information Technology Reference
In-Depth Information
Lastly, there is a variant for the case where
b
has a non-separate type. In this case,
the instruction creates the object on
p
. Processor creation, locking, and lock releasing
is not necessary. The required call stack lock on
p
is given because otherwise
p
would
be waiting.
Create Instruction - Non-Separate
de f
=
type of
(
Γ
,
b
)
(
d
,
h
,
c
)
h
=
•
o
de f
=
σ
.
new obj
(
c
)
de f
=
σ
.
add obj
(
p
,
o
)
r
de f
σ
=
σ
.
ref
(
o
)
ais fresh
Γ
p
::
create
b
.
f
(
e
1
,...,
e
n
)
;
s
p
,
σ
→
p
::
write
(
b
.
name
,
r
)
;
b
.
f
(
e
1
,...,
e
n
)
;
provided
¬
f
.
class type
.
inv exists
∨
f
.
exported
then
nop
else
eval
(
a
,
f
.
class type
.
inv
)
;
wait
(
a
)
end
;
s
p
,
σ
Flow control instructions.
The
if
e
then
s
t
else
s
f
end
instruction executes
s
t
if the
expression
e
evaluates to true. Otherwise the instruction executes
s
f
. There is one in-
ference rule for this instruction. In a first step, the instruction evaluates the expression
e
using a fresh channel
a
and then waits for a notification on
a
. In a second step, it
uses the
provided
operation to either execute
s
t
or
s
f
, depending on the value of the
expression.
If Instruction
ais fresh
Γ
p
::
if
e
then
s
t
else
s
f
end
;
s
p
,
σ
→
p
::
eval
(
a
,
e
)
;
wait
(
a
)
;
provided
a
.
data
then
s
t
else
s
f
end
;
s
p
,
σ
The
until
e
loop
s
l
end
instruction executes a sequence of
s
l
instructions until the
expression
e
evaluates to true. If
e
is true initially, then
s
l
never gets executed. There
is one inference rule for this instruction. First, the instruction evaluates
e
using a fresh
channel
a
. Then it waits for a notification on
a
. Next, it uses the
provided
operation
to check whether
e
evaluates to true or false. If
e
is true, then it is done. Otherwise, it
executes
s
l
followed by another
until
e
loop
s
t
end
operation.
Search WWH ::
Custom Search