Information Technology Reference
In-Depth Information
Conversation API operation Purpose
create(protocol name, invitation config.yml)
Initiate conversation, send invitations
join(self, role, principal name)
Accept invitation
Send message with operation and payload
send(role, op, payload)
Receive message from role
recv(role)
Asynchronous receive
recv async(self, role, callback)
Create a conversation scope
scope(msg)
Close the connection to the conversation
close()
Fig. 4.
The core Python Conversation API operations
behaviours that session type systems traditionally aim to prohibit, in order to prevent
communication races and thereby ensure the desired safety properties.
A key aspect, due to asynchrony, is that an interrupt may occur in parallel to the ac-
tions of the roles being interrupted (e.g.
pause
by
U
to
A
while
A
is streaming
data
to
U
).
Although standard MPST (and Scribble) support parallel protocol flows, the interesting
point here is that the nature of an interrupt is to preclude further actions in another par-
allel flow under the control of a different role, whereas the basic MPST parallel does
not permit such interference. Figure 3 (left) is a naively incorrect attempt to express this
aspect without interruptible: the second parallel path is never able to intefere with the
first to actually stop the recursion.
Another aspect is that of mixed choice in the protocol, in terms of both communi-
cation direction (e.g.
U
may choose to either receive the next
data
or send a
stop
), and
between different roles (e.g.
U
and
C
independently, and possibly concurrently, interrupt
the protocol) due to multiparty. Moreover, the implicit interrupt choice is truly optional
in the sense that it may never be selected at runtime. The basic choice in standard MPST
(e.g. as defined in [17,13]) is inadequate because it is designed to safely identify a single
role as the decision maker, who communicates exactly one of a set of message choices
unambiguously to all relevant roles. Figure 3 (right) demonstrates a naive mixed choice
that is not well-formed (it breaks the unique sender condition in [13]).
Due to the asynchronous setting, it is also important that
interruptible
does not
require implicit synchronisations to preserve communication safety. The underlying
mechanisms are formalised and the correctness of our extension is proved in
ยง
5.
3
Runtime Verification
This section discusses implementation details of our monitoring framework and the ac-
companying Python API (Conversation API) for writing monitorable, distributed MPST
programs. This work is the first implementation of the theory in [7] in practice, and is
the first (theory or practice) to support a general, asynchronous MPST interrupt mech-
anism in the protocol language and API for endpoint implementation.
We first outline the verification methodology of our framework to clarify the pur-
pose of the main components. Developers write endpoint programs in native Python
using the Conversation API, an MPST-based message passing library that supports
the core MPST primitives for communication programming. The execution of these
