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.
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.
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.
Effpi is an experimental toolkit for strongly-typed message-passing programs in Dotty (a.k.a. the future Scala 3 programming language), with verification capabilities based on type-level model checking.
This fgg package is a minimal and basic prototype of Featherweight Go and Featherweight Generic Go, as presented in the related publication below.
The tool allows to
Godel2 is a model checker for MiGo types that returns results of
liveness and safety checks for channels and mutex locks, as well as
the presence of data races on shared pointers.
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.
mpstk is a toolkit for specifying multiparty protocols and verifying their properties (e.g., deadlock-freedom and liveness).
MultiCrusty is a Rust implementation for Multiparty Session Types.
This artifact, for the related OOPSLA 2020 publication below, covers the verification results presented in the paper.
ocaml-mpst is a communication library powered by Multiparty Session Types (abbreviated as MPST) in OCaml. Thus it ensures:
--- under the assumption that all communication channels are used linearly.
Pabble is a parametric extension of Scribble primarily designed for describing communication protocols in parallel computing.
Rumpsteak is a Rust framework for safely and efficiently implementing message-passing asynchronous programs. It uses multiparty session types to statically guarantee the absence of communication errors such as deadlocks.
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.
Session* is a toolchain for specifying message passing protocols using Refined Multiparty Session Types and safely implementing the distributed endpoint programs in F*.
STScript is a toolchain that generates TypeScript APIs for communication-safe web development over WebSockets using routed MPST (RouST). STScript uses TypeScript, ReactJS, and NodeJS as an implementation language, client framework and server framework respectively.
Multiparty session types (MPST) provide a typing discipline for message-passing concurrency, ensuring deadlock freedom for distributed processes. We present νScr (Nu-Scribble), an extensible toolchain, implemented in OCaml, for MPST-based protocols. The toolchain can convert multiparty protocols in the Scribble protocol description language into global types in the MPST theory; global types are projected into local types, and local types are converted to their corresponding communicating finite state machine (CFSM).