Information Technology Reference
In-Depth Information
An executing Erlang program is made up of a
system of actors
,Actr, composed in
parallel
,
A
B
, where some identifiers are local (scoped) to subsystems of actors, and
thus not known to the environment, e.g.,
i
in a system
A
ν
(
i
)
B
. Individual actors,
q
]
m
, are uniquely identified by an identifier,
i
, and consist of an expres-
sion,
e
, executing wrt.a local mailbox,
q
(denoted as a list of values). Actor
expressions
typically consist of a sequence of variable binding
x
i
=
e
i
,
terminated by an expression,
e
final
:
denoted as
i
[
e
x
1
=
e
1
,
...
,
x
n
=
e
n
,
e
final
An expression
e
i
in a binding
x
i
=
e
i
,
e
i
+
1
is expected to evaluate to a value,
v
,which
is then bound to
x
i
in the continuation expression
e
i
+
1
. When instead
e
i
generates an
exception,
exit
, it aborts subsequent computations
1
in
e
i
+
k
. Apart from bindings, ex-
pressions may also consist of self references (to the actor's own identifier),
self
, outputs
to other actors,
e
1
!
e
2
, pattern-matching inputs from the mailbox,
rcv
g
end
, or pattern-
matching for case-branchings,
case
e
of
g
end
(where
g
is a list of expressions guarded
by patterns,
p
i
→
e
i
), function applications,
e
1
(
e
2
), and actor-spawning,
spw
e
, amongst
others. Values consist of variables, x, process ids,
i
, recursive functions,
2
μ
y
.λ
x
.
e
, tuples
{
v
1
,...,
v
n
}
and lists,
l
, amongst others.
Remark 1.
The functions fv(
A
) and fId(
A
) return the free variables and free process
identifiers of
A
resp. and are defined in standard fashion. We write
λ
x
.
e
and
d
,
e
for
μ
y
.λ
x
.
e
and y
=
d
,
e
resp. when y
fv(
e
). In
p
→
e
, we replace x in
p
with
whenever
x
fv(
e
). We write
μ
y
.λ
(x
1
,...
x
n
)
.
e
for
μ
y
.λ
x
1
....λ
x
n
.
e
. We elide mailboxes,
i
[
e
],
when empty,
i
[
e
], or when they do not change in the transition rules that follow.
q
]
m
,toa
Specific to our formalisation, we also subject each individual actor,
i
[
e
,
∈{◦,•,∗}
◦
•
∗
monitoring-modality
,
m
denote
monitored
,
unmonitored
and
tracing
actors resp.Modalities play a crucial role in our language semantics, defined
as a labelled transition system over systems,
A
γ
n
,where
,
and
Act
τ
, include
bound
output
labels, (
h
)
i
!
v
,and
input
labels,
i
?
v
and a distinguished
internal
label,
−→
B
, where actions
γ ∈
.In
line with the reactive properties we consider later, our formalisation only traces system
interactions with the environment (send and receive messages) from
monitored
actors.
Thus, whereas unmonitored,
τ
•
, and tracing,
∗
, actors have standard input and output
transition rules
∈{•,∗}
∈{•,∗}
m
m
SndU
RcvU
i
!
v
−−→
i
?
v
−−→
q
]
m
q
]
m
q
]
m
q
:
v
]
m
j
[
i
!
v
j
[
v
i
[
e
i
[
e
actors with a monitored modality,
, i.e.,actors
j
and
i
in rules SndMandRcvMbelow,
produce a residual message reporting the send and receive interactions (
◦
{
sd
,
i
,
v
}
and
{
rv
,
i
,
v
}
resp.) at the tracer's mailbox i.e.,actor
h
with modality
∗
in the rules below; this
models closely the tracing mechanism o
ered by the Erlang Virtual Machine (EVM)
[7]. In our target language, the list of report messages at the tracer's mailbox constitutes
the system trace to be used for asynchronous monitoring.
ff
1
Because of
exit
exceptions, variable bindings cannot be encoded as function applications.
2
The preceding
μ
y
denotes the binder for function self-reference.
