StMungo

StMungo (Scribble to Mungo) is a Java-based tool used to translate Scribble local protocol specifications into typestate specifications. It is implemented using the ANTLR v4.5 framework. After the translation, we use the Mungo tool to statically typecheck protocol implementation. We start from a multiparty protocol defined as Scribble global protocol and then use the Scribble tools to validate and project into local protocols describing the interactions from the view-point of each of the participants. For every Scribble local protocol, StMungo produces .mungo files containing:

  • a typestate specification describing the local protocol as a sequence of method calls;
  • an API for the participant implementing the methods in the typestate;
  • a main() method skeleton calling the methods in the typestate.

Paper Source Website

Mungo

Mungo is a Java front-end tool used to statically check the order of method calls. It is implemented using the JastAdd framework. A protocol definition is described as a sequence of method calls, the order of which determines the validity of the object protocol. A typestate file cpntaining this protocol definition is defined and associated to a class.

The Mungo tool checks that the object instantiating the class performs method calls by following its declared typestate. If the object respects the typestate, then .java files are produced, for every .mungo file in the program. Finally, the Java tools can be used to compile and run the standard Java code. If the typestate is violated, Mungo reports the errors.

Paper Source Website

Scribble-Scala

The Scribble-Scala tool contains a version of the Scribble tool that, given a multiparty protocol specification, can generate Scala APIs for implementing each participant in a type-safe, protocol abiding way. The API generation leverages a decomposition of the multiparty protocol into type-safe peer-to-peer interactions between pairs of participants, which in turn, allows to implement the API internals on top of the existing lchannels library for type-safe binary session programming.

As a result, several technically challenging aspects in the implementation of multiparty sessions are solved “for free”, at the underlying binary level. This includes distributed multiparty session delegation: this artifact implements it for the first time.

Paper API Gen lchannels Tutorial