Tools and software developed by our group.
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 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.
effect-sessions library is an implementation of session types in
Haskell, via an effect system encoding by embedding session types into
an effect system.
The tool allows to
Gong is a liveness and safety checker for MiGo types.
HAPI is a programming language developed by Lasse Nielsen which provides an intuitive syntax for the asynchronous pi-calculus with multiparty session types.
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
The Scala type checker can examine the resulting code and spot many protocol violations at compile time.
Pabble is a parametric extension of Scribble primarily designed for describing communication protocols in parallel computing.
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.
Scribble-Go is a toolchain for safe distributed programming using role-parametric session types in Go. It extends Scribble, a toolchain for safe distributed programming using basic (non-role-parametric) session types in Java, with:
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 is a communication-safe programming framework which combines multiparty session types with the C programming language.
A Java extension with support for Session Types.
Session-ocaml is an implementation of session types in OCaml.
STP is a type provider in F# that generates APIs from protocol specifications.
This is an Erlang API for programming with gen_server.
We statically analyse the communication flow of a program, given as a multiparty protocol, to extract the causal dependencies between processes and to localise failures. A recovered communication system is free from deadlocks, orphan messages and reception errors.