mpstk

Creative Commons License
This work is licensed under a Creative Commons Attribution 4.0 International License.

mpstk: the MultiParty Session Types toolKit

mpstk is a toolkit for specifying multiparty protocols and verifying their properties (e.g., deadlock-freedom and liveness).

mpstk is based on the new, generalised theory of multiparty session types presented in the companion paper:

Alceste Scalas and Nobuko Yoshida. Less is More: Multiparty Session Types Revisited. POPL 2019.

Software requirements

NOTE: if you are using the preconfigured virtual machine of the POPL'19 artifact, you can skip this section and jump to the usage instructions.

The following software packages must be installed in order to compile and use mpstk:

mpstk has been tested on GNU/Linux (Ubuntu 16.04 and 18.04), and its code is written with portability in mind. It should run on other operating systems (especially Unix-like ones) with little or no adaptations.

Compiling

Simply run:

sbt package

The build system will automatically download all mpstk dependencies (including the Scala compiler, and its runtime).

Usage

Currently, mpstk provides two tools:

The toolkit supports two types of protocol specification:

mpstk includes various examples: they are illustrated below.

Reproducing the results in the companion paper

Reproducing Tables 4 and 5

The following scripts allow to easily reproduce Tables 4 and 5 of the companion paper (between parentheses, the expected execution time on an Intel Core i7 CPU @3.60 GHz).

In all cases, it is possible to save the results in CSV format, simply by adding the option --output-csv=<CSVFILE> when invoking the scripts. For more details, see ./bin/mpstk verify --help.

Variations of Table 5

Table 5 in the companion paper measures the time needed by mpstk to verify a specification against a property; in particular, it measures the time needed to invoke mCRL2's tool pbes2bool, and retrieve its result. This is the dominating time in the verification procedure.

mpstk can produce two other related measurements, through the option --benchmark-type=<T> — where <T> can be either:

The results of all benchmark variants should be very similar: realtime should be (on average) around 1% faster than the default benchmark, while endtoend should be around 1% slower.

Verifying other examples

The examples/ directory contains all the examples in the companion paper, and more. Some files have descriptive names, while others refer to their position in the paper:

instrument-control.ctx Deadlocked typing context, taken from Example 3.10 of this JACM paper.
instrument-control-fixed.global Adaptation (with bugfix) of Example 3.10 of this JACM paper.
multiparty-game.global Running example from this ECOOP'17 paper.
multiparty-workers.ctx Table 2, protocol 4 (“independent multiparty workers”).
oauth2.global Opening example in Section 1.
payload-subtype.ctx Small example used to explain how mpstk handles subtyping.
popl19-ex5.11-a.ctx Example 5.11, case ΓA.
popl19-ex5.11-b.ctx Example 5.11, case ΓB.
popl19-ex5.11-c.ctx Example 5.11, case ΓC.
popl19-ex5.6.ctx Example 5.6.
popl19-ex5.7.ctx Example 5.7.
popl19-sec2.3.ctx The unsafe typing context discussed in Section 2.3.
popl19-sec5.ctx The safe, but deadlocked, typing context discussed in the opening of Section 5.
popl19-sec7-m3.ctx The safe, but deadlocked, typing context discussed in Section 7, point (M3).
rec-map-reduce.ctx Table 2, protocol 3 (“recursive map/reduce”).
rec-two-buyers.ctx Table 2, protocol 2 (“recursive two-buyer”).
two-buyers.global Classic two-buyer protocol from session types literature, taken from this POPL'08 paper (Section 3.2) and this JACM paper (Example 3.8).
streaming.global Simple streaming protocol taken from this POPL'08 paper (Section 3.2) and this JACM paper (Example 3.9).

All examples can be verified by invoking the tool as expected, e.g.:

./bin/mpstk verify examples/popl19-ex5.11-c.ctx

Additionally, the examples-bad/ directory contains various global types that are not projectable, according to Definition 3.2 in the companion paper. For more details, one can invoke, e.g.:

./bin/mpstk project examples-bad/instrument-control.global

and see the resulting error messages: they show which projections are not defined, and why.

Checking the implementation of Table 3

The multiparty session typing context properties verified by mpstk are implemented as mCRL2 µ-calculus formulas, by strictly following the definitions of Table 3 in the companion paper.

Each property is defined as a .mcf file, and is provided as part of the program resources:

By visually inspecting the contents of the .mcf files above, it should be possible to grasp their direct correspondence with Table 3 in the companion paper. Still, such .mcf files use several mCRL2 sorts (e.g., Session, Role, Message, ...) that are defined elsewhere. For more details, please see how session typing contexts are encoded in mCRL2.

Behind the scenes

API documentation

To build the API documentation, invoke:

sbt doc

The resulting documentation will be available in target/scala-2.12/api/mpstk/ (online copy).

Overview of the mpstk source code

This section provides a brief description of each mpstk source code file.

Core data structures

mCRL2 encoding and verification

Tools

Extending mpstk

mpstk can be easily extended to verify new behavioural properties (defined as mCRL2 µ-calculus formulas) of session typing contexts. The procedure can be inferred from the source code of mcrl2/Property.scala:

  1. define a new object MyProperty that extends the abstract class Property:
    case object MyProperty extends Property(descr, filename, shortName)
    where:
    • descr is a human-readable description;
    • filename is the filename of an mCRL2 formula file (minus its .mcf extension). This name is also used to reference the new property by the mpstk verify command line tool;
    • shortName is a shorthand used, e.g., in the headers of tables and CSV files;
  2. add MyProperty to the set Properties.all;
  3. add the file filename.mcf of the new property the program resources directory.

The missing part in the procedure above is how to actually write the filename.mcf file, so that it can be correctly used to verify the mCRL2 process specifications generated by mcrl2/Spec.scala. To do it, it is necessary to know how typing contexts are encoded in mCRL2.

Encoding session typing contexts in mCRL2

NOTE: this section uses some formal notation defined in the companion paper, and assumes that readers have some familiarity with the mCRL2 model checker.

Overview

Take a typing context Γ. In a nutshell, the goal of the mCRL2 encoding is to:

  1. turn each entry s[p]:T ∈ Γ into a sequential mCRL2 process, that performs input/output actions according to Definition 2.8 (rules [Γ-&] and [Γ-⊕]). In particular, mCRL2's choice operator “+” should model external/internal choices;
  2. then, compose the sequential processes above in parallel, to model the communications of Γ (Definition 2.8, rule [Γ-Comm]). In particular, the mCRL2's parallel composition operator “||”, together with “allow”/“comm”, should model synchronisation of inputs/outputs with matching labels/payloads.

Structure of autogenerated mCRL2 specifications

To achieve the above goal, mpstk converts a typing context Γ (internally represented as a Context instance) into a mCRL2 process specification (internally represented as a Spec instance) consisting of three parts:

  1. a fixed preamble, available in the file mpst-preamble.mcrl2. It defines:
    • various mCRL2 sorts that correspond to the syntax of multiparty session types: Session, Role, Message, Payload (for details on the handling of payloads, see below);
    • actions i / o / t (for “tau”), that correspond, respectively, to the input / output / communication labels of Definition 2.8 in the companion paper (with a minor difference: the encoded t actions do not discard the payload type);
  2. an autogenerated mCRL2 process called “context”, that is the actual typing context encoding. The process “context”, in turn, uses other autogenerated process definitions:
    • one process for each entry s[p]:T ∈ Γ. Such processes use the i / o actions defined in the preamble, and the choice operator “+” to model branching/selection session types. Such processes are composed in parallel in the definition of “context”;
    • more process definitions to model the recursive sub-terms (if any) of each entry s[p]:T ∈ Γ.
  3. a fixed initial process declaration, available in the file mpst-init.mcrl2. It declares that “context” (i.e., the mCRL2-encoded session typing context defined above) is the initial mCRL2 process that is verified against µ-calculus formulas. In particular, the initial process declaration uses the operators “allow” / “comm” to specify that i/o actions synchronise by producing t actions.

NOTE: the encoding above is purposedly designed with a fixed preamble. The reason is that, by using the generic sorts and actions defined in mpst-preamble.mcrl2, one can develop generic µ-calculus formulas, that can be used to verify any (encoded) session typing context — without depending on the actual sessions, roles, message labels, and payloads used therein. This feature is exploited in the µ-calculus formulas provided by mpstk, and can be leveraged to extend the tool.

The encoding in practice

To better grasp the explanation above, it is possible to inspect the results of the mCRL2 encoding, by using the --keep-temp option of mpstk verify. E.g., by executing:

./bin/mpstk verify --keep-temp examples/oauth2.global

mpstk will not erase its temporary working directory, and will print its path.

If such a temporary directory is <DIR>, then the autogenerated file <DIR>/context.mcrl2 contains various comments that show how the initial global type is transformed throughout the encoding, and what part of the multiparty protocol corresponds to each autogenerated mCRL2 process.

The temporary directory also contains other autogenerated mCRL2 files (with the typical extensions, e.g., .lps, .pbes, .lts): they can be used to manually invoke the mCRL2 tools. For more insight, it is also possible to use the --debug option of mpstk verify: it logs each use of the mCRL2 tools on the autogenerated files.

A note on subtyping and message payloads

The explanation above skims over a subtle, but crucial, detail:

To overcome this limitation, mpstk performs some syntactic pre-processing of typing contexts, before encoding them in mCRL2.

For example, assume T⩽S, and consider the typing context  Γ = s[p]:q⊕m(T).T′, s[q]:p&m(S).S′.  Its mCRL2 encoding must model the reduction  Γ → s[p]:T′,s[q]:S′,  as in Definition 2.8. To this purpose, mpstk pre-processes Γ as follows:

  1. Γ is initially represented as a Context instance;
  2. mpstk collects all outputs that a role r might send to another role r′. In this example, p might send a singleton set of messages M = { m(T) } to role q;
  3. then, Γ is converted into a raw Context instance. The difference is that, unlike Definition 2.4 in the companion paper, the session types in “raw Γ” can have internal/external choices with duplicated message labels;
  4. then, mpstk rewrites the “raw Γ” as follows:
    1. it checks whether q's type contains some external choice that might receive a message m(S) from p;
    2. if so, it checks whether the potential outputs of p (i.e., the set M above) include some message m(T) such that T⩽S (this is why mpstk implements the session subtyping algorithm);
    3. if so, mpstk extends q's external choice with a new option m(T), and the same continuation of the original branch m(S) (this is implemented in raw.MPST.addSubBranches());
    In this example, the original Γ above is rewritten as  Γ′ = s[p]:q⊕m(T).T′, s[q]:p&{m(S).S′,m(T).S′}  (notice the new branch of s[q]).
  5. finally, the rewritten typing context Γ′ is encoded in mCRL2, as explained above. Now, mCRL2 can model synchronisation by simply checking whether an output action m(T) from p to q is matched by an equal input action m(T) by q from p. This models the typing context reduction  Γ′ → s[p]:T′,s[q]:S′,  thus implementing Definition 2.8 as desired.

This explanation can be seen in practice, by executing, e.g.:

./bin/mpstk verify --keep-temp examples/payload-subtype.ctx

and inspecting the autogenerated file context.mcrl2, as illustrated above.

A note on non-tail-recursive types

In the companion paper, Example 5.11 (case ΓC) shows a non-tail-recursive session type μ(t)q⊕m(t).end, where the recursion variable t occurs as payload of the message m. Such types are troublesome (and usually unsupported) in classic session types works (c.f. related work in the companion paper) — but they are seamlessly supported in the new theory behind mpstk.

To translate such non-tail-recursive types and typing contexts into mCRL2 specifications, mpstk proceeds in two steps:

  1. it unfolds the message payloads, ensuring that they have no free variables. This transformation is provided by the method MPST.unfoldPayloads; e.g., the method unfolds the type μ(t)q⊕m(t).end above into μ(t)q⊕m(μ(t')q⊕m(t').end).end
  2. then, mpstk performs the encoding as described above. The unfolded payload is handled transparently, by the same principles that handle the subtyping of message payloads.

This explanation can be seen in practice, by executing, e.g.:

./bin/mpstk verify --keep-temp examples/popl19-ex5.11-c.ctx

and inspecting the autogenerated file context.mcrl2, as illustrated above.

mpstk shares some goals and features with Scribble, the first tool using the theory of session types to implement protocol specification and verification.

However, mpstk ha a fundamental design difference: it is a research tool that strictly adheres to the new, generalised session types theory introduced in the companion POPL'19 paper. Scribble, instead, stems from the classic multiparty session types theory, and adds various extensions and variations on top of it, mainly for the purpose of automatic code generation (that mpstk does not address).

This fundamental difference has two consequences:

  1. mpstk can verify multiparty protocols expressed as typing contexts (.ctx file format); as a bonus, it can also verify global types (.global file format), by projecting them. Scribble, instead, has the opposite design: it is centred on global types, and projections (as in the classic multiparty session types theory). Therefore, it is not suited for verifying protocols that cannot be projected from global types;
  2. in particular, mpstk can seamlessly verify higher-order and non-tail-recursive types, that are not supported by Scribble.

TODOs and future work

Contacts

For questions and enquiries, you can contact the mpstk author:

Alceste Scalas   <alceste (dot) scalas (at) imperial (dot) ac (dot) uk>