The following is a list of software tools that I have collaborated on.
The tools are implemented for either Java (StMungo and Mungo) or Scala (Papaya and Scribble-Scala) and are based on the notion of session types or typesates, for the verification of communication protocols among participants in distributed systems.
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:
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 containing 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 WebsiteThe Papaya tool is an implementation for Scala of global typestate analysis where unrestricted aliasing is allowed. It is implemented as a compiler library for Scala, allowing it to be embedded into real-world programs, verifying at compile time that protocols are being adhered to by all instances.
The protocols are expressed as singleton classes and thus are written in Scala itself. A protocol is linked to a class by using the @Typestate annotation, and the tool will generate errors or warning if instances of this class does not respect the protocol, or if a protocol is potentially left unfinished.
Paper Source Website TutorialThe 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