Information Technology Reference
In-Depth Information
Global types (
G
) below correspond to Scribble protocols. Scopes are made explicit
by the use of scope variables
S
, corresponding to the dynamic scope generation present
in the implementation in
§
3.1. Roles in types are denoted by
r
, and labels with
l
.
r
:
S
;
G
|
μ
→
{
l
i
.
G
i
}
|
|
|{|
|}
x
.
G
|
|
|
G
::=
r
G
G
G
l
by
r
x
end
Eend
i
∈
I
{
l
i
.
T
i
}
|
{
l
i
.
T
i
}
|
|
T
::=
r
!
r
?
T
T
i
∈
I
i
∈
I
S
;
T
|{|
S
;
T
|
μ
| |
T
|}
r
!
l
T
|}
r
?
l
x
.
T
|
x
|
end
|
Eend
The main primitive is the interaction with directed choice:
r
→
r
:
l
i
.
G
i
}
i
∈
I
is a com-
munication between the sender
r
and the receiver
r
which involves a choice between
several labels
l
i
, the corresponding continuations are denoted by the
G
i
. Parallel com-
position
G
1
|
{
G
2
allows the execution of interactions not linked by causality.
Our types feature a new interrupt mechanism by explicit interruptible scopes: we
write
;
G
to denote a creation of an interruptible block identified by scope
S
, containing protocol
G
, that can be interrupted by a message
l
from
r
and contin-
ued after completion (either normal or exceptional) with protocol
G
. This construct
corresponds to the
interruptible
of Scribble, presented in
S
{|
G
|}
l
by
r
2. Note that we allow
interruptible scopes to be nested. This syntax (and the related properties) can be easily
extended to multiple messages from different roles. We use
Eend
(resp.
end
) to denote
the exceptional (resp. normal) termination of a scope.
The local type syntax (
T
) given above follows the same pattern, but the main differ-
ence is that the interruptible operation is divided into two sides, one
side for the roles
which can send an interrupt
§
S
r
!
l
;
T
,andthe
side for the roles which should
{|
T
|}
S
r
?
l
;
T
.
expect to receive an interrupt message
{|
T
|}
S
2
G
ResCont
=
U
→
C
:req;
C
→
A
:start
{|
μ
X
.
{|
μ
Y
.
A
→
U
: data;
Y
|}
pause by
U
;
S
1
U
→
A
:resume;
X
|}
stop by
U
,
timeout by
C
;
end
Above we describe a global type which corresponds to the Scribble protocol in Fig-
ure 2. The explicit naming of the scopes,
S
1
and
S
2
, correspond to the dynamic scope
generations in
3.1, and are required to formalise the semantics of local types.
We define the relation
G
§
G
as:
r
→
r
:
{
l
i
.
G
i
}
i
∈
I
G
i
S
S
{|
G
|}
l
by
r
;
G
0
{|
Eend
|}
l
by
r
;
G
0
G
G
implies
S
;
G
0
{|
G
|}
S
G
G
implies
G
|
G
0
G
|
G
0
{|
G
|}
l
by
r
l
by
r
;
G
0
and say
G
is a
derivative
of
G
if
G
∗
G
.Wedefine
configurations
as a pair of a
mapping from a session channel to a local type and a collection of queues (a mapping
from a session channel to a vector of the values). Configurations model the behaviour of
a network of monitored agents. We say a configuration
Δ
,
Σ
Δ
,
Σ
corresponds to a collection
of global types
G
1
,...,
G
l
whenever
Σ
is empty and the environment
Δ
is a projection
Σ
)isdefined
using the contexts with the scopes. Formal definitions can be found in [35].
The correctness of our theory is ensured by Theorem 1, which states a local en-
forcement implies global correctness: if a network of monitored agents (modelled as
a configuration) corresponds to a collection of well-formed specifications and makes
some steps by firing messages, then the network can perform reductions (consuming
these messages) and eventually reaches a state that corresponds to a collection of well-
formed specifications, obtained from the previous one. This property guarantees that
Σ
→
Δ
,
of
G
1
,...,
G
l
. The reduction semantics of the configuration (
Δ
,
