π-calculus, Session Types research at Imperial College

Tools & Software

Tools and software developed by our group.

Dynamic deadlock verification for general barrier synchronisation

Armus is a dynamic verification tool for deadlock detection and avoidance specialised in barrier synchronisation. Barriers are used to coordinate the execution of groups of tasks, and serve as a building block of parallel computing. Our tool verifies more barrier synchronisation patterns than current state-of-the-art. To improve the scalability of verification, we introduce a novel event-based representation of concurrency constraints, and a graph-based technique for deadlock analysis. The implementation is distributed and fault-tolerant, and can verify X10 and Java programs.

DinGo hunter
Static deadlock detection tool for Go

dingo-hunter is a static deadlock detection tool for the Go language. The tool leverages session graph synthesis to detect potential deadlocks and unsafe concurrency patterns in the source code.

Effects as sessions, session as effects

The effect-sessions library is an implementation of session types in Haskell, via an effect system encoding by embedding session types into an effect system. (POPL’16 artifact)

Tool for synthesising a choreography from Genalised Multiparty Compatible CFSMs

The tool allows to

Channel Liveness and Safety checker

Gong is a liveness and safety checker for MiGo types.

Read More
Happy Asynchronous Pi Calculus

HAPI is a programming language developed by Lasse Nielsen which provides an intuitive syntax for the asynchronous pi-calculus with multiparty session types.

Type-safe session programming in Scala

lchannels is a Scala library for type-safe session programming. It provides linear I/O channels, which allow to transfer data locally, or over a network. Its API allows to

  1. define protocols, represented as a set of continuation-passing style classes, and
  2. easily write programs that interact according to such protocols

The Scala type checker can examine the resulting code and spot many protocol violations at compile time.

Parameterised Scribble

Pabble is a parametric extension of Scribble primarily designed for describing communication protocols in parallel computing.

Scribble Project
Protocol description language

The Scribble project is a joint effort with Cognizant, OOI and Red Hat established to realise multiparty session types as application-level protocols. It consists of a core language Scribble and tools/IDE support. A research version of Scribble is available from Raymond Hu, please contact him for details.

A concurrent programming language with refined session types
SePi is a concurrent, message-passing programming language based on the pi-calculus. The language features synchronous, bi-directional channel-based communication. Programs use primitives to send and receive messages as well as offer and select choices. Channel interactions are statically verified against session types describing the kind and order of messages exchanged, as well as the number of processes that may share a channel. In order to facilitate a more precise control of program properties, SePi includes assume and assert primitives at the process level and refinements at the type level. Read More
Session Actor
An actor framework in Python with support for session types

Session Actor is an actor framework in Python with support for session types. An actor can implement multiple session types (roles) in a similar way as an object can implement multiple interfaces. The framework supports automatic discovery of roles and runtime checks for protocol compliance.

Session C programming framework
Multiparty session programming in C

Session C is a communication-safe programming framework which combines multiparty session types with the C programming language.

Session Java
Session-based distributed programming in Java

A Java extension with support for Session Types.