Information Technology Reference
In-Depth Information
has been designed to be readable and familiar to programmers,
interruptible
is an
advanced construct that encapsulates several aspects of asynchronous interaction, which
we discuss at the end of this section.
The intended communication protocol in our example is clarified in Scribble as two
nested
interruptible
statements. The outer statement, on lines 6-22, corresponds to
the options for User and Controller to end the protocol via the
stop
and
timeout
inter-
rupts. An
interruptible
consists of a main body of protocol actions, here lines 7-18,
and a set of interrupt message signatures, lines 19-22. The statement stipulates that
each participant behaves by either (a) following the protocol specified in the body until
finished for their role, or (b) raising or detecting a specified interrupt at any point during
(a) and exiting the statement. Thus, the outer
interruptible
states that
U
can interrupt
the body (and end the protocol) by a
stop()
message, and
C
by a
timeout()
.
The body of the outer
interruptible
is a labelled recursion statement with label
X
.
The
continue X;
inside the recursion (line 17) causes the flow of the protocol to return
to the top of the recursion (line 7). This recursion corresponds to the loop implied
by the sequence diagram that allows User to pause and resume repeatedly. Since the
recursion body always leads to the
continue
, Scribble protocols of this form state that
the loop should be driven indefinitely by one role, until one of the interrupts is raised
by
another
role. This communication pattern cannot be expressed in multiparty session
types without
interruptible
.
The body of the
X
-recursion is the inner
interruptible
, which corresponds to the
option for User to pause the stream. The stream itself is specified by the
Y
-recursion, in
which
A
continuously sends
data()
messages to
U
. The inner
interruptible
specifies
that
U
may interrupt the
Y
-recursion by a
pause()
message, which is followed by the
resume()
message from
U
before the protocol returns to the top of the
X
-recursion.
Challenges of Asynchronous Interrupts in MPST.
The following summarises our
observations from the extension and usage of MPST with asynchronous interrupts. We
find the basic operational meaning of
interruptible
, as illustrated in the above exam-
ple, is readily understood by architects and developers, which is a primary consideration
in the design of Scribble. The challenges in this extension are in the design of the sup-
porting runtime and verification techniques to preserve the desired safety properties in
thepresenceof
interruptible
. The challenges stem from the fact that
interruptible
combines several tricky, from a session typing view, aspects of communication
// Well-formed, but incorrect semantics:
// Naive mixed-choice is not well-formed
1
1
// the recursion cannot be stopped
choice at
A{
2
2
par
{
// A should make the choice..
3
3
rec
Y{
rec
Y{
4
4
data()
from
A
to
U;
data()
from
A
to
U;
5
5
continue
Y; }
continue
Y; }
6
6
}
and
{
}
or
{
7
7
// Does not stop the recursion
// ..not U
8
8
pause()
from
U
to
A;
pause()
from
U
to
A;
9
9
}
}
10
10
resume()
from
U
to
A;
resume()
from
U
to
A;
11
11
Fig. 3.
Naive, incorrect interruptible encoding attempts using parallel (left) and choice (right)
