Information Technology Reference
In-Depth Information
Practical Interruptible Conversations
Distributed Dynamic Verification with Session Types and Python
Raymond Hu
1
, Rumyana Neykova
1
, Nobuko Yoshida
1
,
Romain Demangeon
1
, and Kohei Honda
2
1
Imperial College London
2
Queen Mary, University of London
Abstract.
The rigorous and comprehensive verification of communication-based
software is an important engineering challenge in distributed systems. Drawn
from our industrial collaborations [33,28] on Scribble, a choreography descrip-
tion language based on multiparty session types, this paper proposes a dynamic
verification framework for structured interruptible conversation programming.
We first present our extension of Scribble to support the specification of asyn-
chronously interruptible conversations. We then implement a concise API for
conversation programming with interrupts in Python that enables session types
properties to be dynamically verified for distributed processes. Our framework
ensures the global safety of a system in the presence of asynchronous interrupts
through independent runtime monitoring of each endpoint, checking the confor-
mance of the local execution trace to the specified protocol. The usability of our
framework for describing and verifying choreographic communications has been
tested by integration into the large scientific cyberinfrastructure developed by the
Ocean Observatories Initiative. Asynchronous interrupts have proven expressive
enough to represent and verify their main classes of communication patterns, in-
cluding asynchronous streaming and various timeout-based protocols, without re-
quiring additional synchronisation mechanisms. Benchmarks show conversation
programming and monitoring can be realised with little overhead.
1
Introduction
The main engineering challenges in distributed systems include finding suitable speci-
fications that model the range of states exhibited by a system, and ensuring that these
specifications are followed by the implementation. In message passing applications, rig-
orous specification and verification of communication protocols is particularly crucial:
a protocol is the interface to which concurrent components should be independently
implementable while ensuring their composition will form a correct system as a whole.
Multiparty Session Types (MPST) [17,6] is a type theory for communication-oriented
programming, originating from works on types for the
-calculus, towards tackling this
challenge. In the original MPST setting, protocols are expressed as types and static type
checking verifies that the system of processes engaged in a communication session (also
referred to as a
conversation
) conforms to a globally agreed protocol. The properties en-
joyed by well-typed processes are communication safety (no unexpected messages or
races during the execution of the conversation) and deadlock-freedom.
π
