Information Technology Reference
In-Depth Information
SndM
i
!
v
−−→
q
]
◦
r
]
∗
q
]
◦
]
∗
{
,
,
}
j
[
i
!
v
h
[
d
j
[
v
h
[
d
r
:
sd
i
v
RcvM
i
?
v
−−→
q
]
◦
r
]
∗
q
:
v
]
◦
]
∗
i
[
e
h
[
d
i
[
e
h
[
d
r
:
{
,
i
,
v
}
rv
Our LTS semantics assumes
well-formed
actor systems, whereby every actor iden-
tifier is
unique
;itistermedtobea
tracing semantics
because a distinguished
tracer
actor, identified by the monitoring modality
, receives messages recording external
communication events by
monitored
actors. Formally, we write
A
γ
∗
−→
B
in lieu of
, the least ternary relation satisfying the rules in Fig. 2. These rules
employ
evaluation contexts
, denoted as
A
,γ,
B
∈−→
(described below) specifying which sub-
expressions are active. For instance, an expression is only evaluated when at the top
level variable binding,
x
=
C
,
e
or when the expression denoting the destination of an
output has evaluated to a value,
v
!
C
; the other cases are also fairly standard.
3
We denote
C
C
C
the application of a context
to an expression
e
as
[
e
].
C
::
=
[
−
]
|C
!
e
|
v
!
C|C
(
e
)
|
v
(
C
)
|
case
C
of
g
end
|
x
=
C
,
e
| ...
Communication in actor systems happens in two stages: an actor receives messages,
keeping them in order in its mailbox, and then selectively reads them at a later stage
using pattern matching—rules Rd1andRd2 describe how mailbox messages are tra-
versed in order to find the first one matching a pattern in the pattern list
g
, releasing
the respective guarded expression
e
as a result. We choose only to record
external
com-
munication at tracer processes, i.e., between the system and the environment, and do
not trace internally communication between actors within the system, irrespective of
their modality (see Com); structural equivalence rules,
A
B
, are employed to simplify
the presentation of our rules—see rule Str and the corresponding structural rules. In
Par, the side-condition enforces the
single-receiver
property, inherent to actor systems;
for instance, it prevents a transition with an action
j
!
v
when actor
j
is part of the actor
system
B
. Finally, spawned actors inherit monitorability when launched by a monitored
actor, but are launched as unmonitored otherwise (see Spw). The rest of the transition
rules are fairly standard; consult [15] for details.
≡
Remark 2.
Our tracing semantics sits at higher level of abstraction than that o
ered by
the EVM [7] because trace entries typically contain more information. For instance,
the EVM records internal communication between monitored actors, as an output trace
entry
immediately followed by
the corresponding input trace entry; we here describe
sanitised
traces whereby consecutive matching trace entries are filtered out.
ff
Example 1 (Non-deterministic behaviour).
Our systems exhibit non-deterministic be-
haviour through either internal or external choices [23,18]. Consider the actor system:
h
)
i
[
rcv
x
q
]
∗
]
◦
j
1
[
i
!
v
]
◦
j
2
[
i
!
u
]
◦
A
(
ν
j
1
,
j
2
,
→
obs
!x
end
h
[
e
3
In our formalisation, expressions are not allowed to evaluate under a spawn context,
spw
[
−
].
This di
ff
ers from standard Erlang semantics but allows a lightweight description of function
application spawning; an adjustment in line with Erlang spawning would be straightforward.
