Timed Runtime Monitoring for Multiparty Conversations

Rumyana Neykova, Laura Bocchi, Nobuko Yoshida

In [tMPST] we present a real-time extension of Multiparty Session Types to the verification and enforcement of time-related properties in Python. The prototype implementation is available at bottom of this page.

1. Context and Background

(Untimed) Multiparty Session Types (MPSTs) have been applied in an existing framework for verification of choreographic sessions in Python ([1]). This framework is embedded into the OOI infrastructure using Scribble, a practical incarnation of MPSTs, as a specification language for global protocols. Some resources:

2. An Application of Timed Multiparty Session Types

In the OOI infrastructure time plays a crucial role. In most of the OOI use-cases, service requests are augmented with deadlines and services are scheduled to execute at certain time intervals to minimise energy consumption. In [tMPST] we have extended the MPSTs framework with time to accommodate these requirements. In this section we discuss a practical application of the timed MPTSs presented in [tMPST].

Timed Specifications

We have extended Scribble with clocks and clock constraints; (timed) global specifications are checked by the Scribble compiler for feasibility and wait-freedom, and then projected by the Scribble toolchain (as in Section 2 [tMPST]). The figure below shows how we express the Global protocol for the WordCount example in Scribble. Clocks constraints and reset predicates are enclosed by square brackets. In [x@M:x=0,reset(x)] the constraint states that the next action of M, namely sending the task to W, must be executed when the value of clock x of M is 0, and then the clock of M must be reset.
Temperature calculation: the timed global protocol in Scribble
Temperature calculation: the timed global protocol in Scribble

Timed Implementations: from Timed Processes to Python

We extend the Python conversation API with time for distributed runtime processes. The figure below shows the Python program for process the master role. Letter s denotes the session, while w and a are the queues of W and R, respectively. The conversation API has two main primitives (we abstract on the session initialisation): send and receive. For instance, send(a).task sends a message of type task to R, and the receive is dual. Each participant is implemented as a virtual thread using a Python library for cooperative scheduling called "gevent". We extended the API with the primitive s.delay which correspond to the delay operator of our calculus. In order to handle time violations we have introduced the primitive s.timeout which raises an error if the next instruction cannot be completed in the given time frame.
Temperature calculation: the timed process for participant M in the Python extension
WordCount example: the timed process for participants M, W and A in the Python extension

Running the Implementation

The implementation can be downloaded here.
The instructions for installing and running the prototype are in the included file readme.txt. If case of any problem while installing or running the application please contact us.
Remark: In the prototype, time is expressed in seconds. In order to speed up the demonstration, the delays l (latency) and w (sampling time) of the running example have not been set to the values in the paper (and in the OOI case study), but to smaller values. These values can be modified by editing the timed local types in the zip file (see the file readme.txt included in the .zip for the location of the corresponding files).