Information Technology Reference
In-Depth Information
When a conversation is initiated at runtime, the monitor at each endpoint generates
a finite state machine (FSM) representation of the local communication behaviour from
the local protocol for its role. In our implementation, the FSM generation is an ex-
tension of the correspondence between MPST and communication automata in [13] to
support
interruptible
sessions (discussed below) and optimised to avoid parallel state
explosion. The monitor tracks the communication actions performed by the endpoint,
and the messages that arrive from the other endpoints, against the transitions permitted
by the FSM. Each monitor thus works to protect both the endpoint from illegal actions
by the environment, and the network from bad endpoints. In this way, our framework is
able to ensure from the local verification of each endpoint that the global progress of the
system as a whole conforms to the original global protocol [7], and that unsafe actions
by a bad endpoint cannot corrupt the protocol state of other compliant endpoints.
This MPST monitoring framework has been integrated into the Python-based run-
time platform developed by the Ocean Observatories Initiative (OOI) [28]. The OOI is
a project to establish a cyberinfrastructure for the delivery, management and analysis of
scientific data from a large network of ocean sensor systems. Their architecture relies on
the combination of high-level protocol specifications of network services (expressed as
Scribble protocols [29]) and distributed runtime monitoring to regulate the behaviour of
third-party applications within the system [31]. Although this work is in collaboration
with the OOI, our implementation can be used orthogonally as a standalone monitoring
framework for distributed Python applications.
Contributions and Summary.
This paper demonstrates the application of multiparty
session types, through the Scribble protocol language, to industry practice by presenting
(1) the first implementation of MPST-based dynamic protocol verification (as outlined
above) that offers the same safety guarantees as static session type checking, and (2) a
use case motivated extension of Scribble to support the first construct for the verification
of asynchronous communication interrupts in multiparty sessions.
We developed the extension of Scribble with asynchronous interrupts to support a
range of OOI use cases that feature protocol structures in which one flow of interactions
can be asynchronously interrupted by another. Examples include various service calls
(request-reply) with timeout, and publish-subscribe applications where the consumer
can request to pause, resume and stop externally controlled sensor feeds. Although the
existing features of Scribble (i.e. those previously established in MPST theory) are suf-
ficiently expressive for many communication patterns, we observed that these important
structures could not be directly or naturally represented without interrupts.
We outline the structure of this paper, summarising the contributions of each part:
§
2 presents a use case for the extension of Scribble with asynchronous interrupts. This
is a new feature in MPST, giving the first general mechanism for nested, multi-
party session interrupts. We explain why implementing this feature is a challenge
in session types. The previous works on exceptions in session types are purely the-
oretical, and are either restricted to binary session types (i.e. not multiparty) [11],
do not support nesting and continuations [11,10], or rely on additional implicit syn-
chronisation [9]. A formal proof of the correctness of our design is given in
§
5.
§
3 discusses the Python implementation of our MPST monitoring framework that we
have
integrated
into
the
OOI
project,
and
demonstrates
the
global-to-local
