Information Technology Reference
In-Depth Information
Similarly, processor
p
can execute the
read
(
operation to read a value of an entity
with name
x
and send the value over channel
a
.The
read
operation does not present
its result in a
result
operation because, unlike an
eval
operation, a
read
operation
always produces a result for the surrounding action queue. It is easier to do the substi-
tution of the channel access directly. A later section introduces the
eval
operation for
entity expressions. This variant of the
eval
operation makes use of the
read
operation
and presents the result in a
result
operation.
x
,
a
)
Read Value Operation
Γ
p
::
read
(
x
,
a
)
;
s
p
,
σ
→
p
::
s
p
[
σ
.
val
(
p
,
x
)
/
a
.
data
]
,
σ
Finally, there is the
set not fresh
operation in a variant for once functions and in
a variant for once procedures. This operation sets the once status of a once routine.
The variant
set not fresh
sets the once status of a once function
f
to non-fresh
with value
r
.If
f
is of separate type, then the once function becomes non-fresh on all
processors in the system. If
f
has a non-separate type, then
f
becomes non-fresh only
on processor
p
.Thevariant
set not fresh
(
(
f
,
r
)
f
)
sets the once status of a once procedure
f
to non-fresh on processor
p
.
Set Once Routine Not Fresh Operation - Function
f
∈
FUNCTION
∧
f
.
is once
σ
de f
=
σ
.
set once func not fresh
(
p
,
f
,
r
)
Γ
p
::
set not fresh
(
f
,
r
)
;
s
p
,
σ
→
p
::
s
p
,
σ
Set Once Routine Not Fresh Operation - Procedure
f
∈
FUNCTION
∧
f
.
is once
σ
de f
=
σ
.
set once proc not fresh
(
p
,
f
)
Γ
p
::
set not fresh
(
f
)
;
s
p
,
σ
→
p
::
s
p
,
σ
Flow control mechanism.
In addition to flow control instructions in the user code,
there are flow control operations, which implement flow control in the inference rules.
This way, fewer inference rules are required because multiple variants can be handled
in one inference rule.
The
provided
x
then
s
t
else
s
f
end
operation takes the condition
x
as an argument.
The operation either executes
s
t
if
x
indicates that the condition is true or
s
f
if
x
indicates
that the condition is false. For each possibility there is one inference rule. The condition
x
can either be an instance of
BOOLEAN
or it can be a reference that points to an object
of class type
BOOLEAN
. To decide which branch to take, the operation must evaluate
x
.If
x
is an instance of
BOOLEAN
, then it can determine which instance
x
is, i.e.,
true
or
false
.If
x
is a reference, then it must get the referenced object and see which boolean
value it represents. For this purpose, it evaluates the attribute
item
of the referenced
object.
Search WWH ::
Custom Search