MobilityReadingGroup

Armus

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.

BitML

A domain-specific language for smart contracts with a computationally sound embedding into Bitcoin

CAMP

CAMP: Cost-Aware Multiparty Session Protocols

This is the artifact for the related publication below. The artifact comprises: A library for specifying cost-aware multiparty protocols. The raw data used for comparing the cost models with real execution costs. The cost-aware protocol specifications of the benchmarks that we studied. The library for specifying cost-aware protocols also provides functions for extracting cost equations from them, and for estimating recursive protocol latencies (i.e. average cost per protocol iteration).

codeINspire

Let it recover: Multiparty Protocol Induced Recovery

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

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.

Effect-Sessions

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)

Effpi

Verified message-passing programs in Dotty

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.

EMTST: Engineering the Meta-theory of Session Types

Libraries for mechanising the theory of session types calculi in Coq.

Featherweight Go and Featherweight Generics Go

A design for generics in Go inspired by Featherweight Java

This fgg package is a minimal and basic prototype of Featherweight Go and Featherweight Generic Go, as presented in the related publication below.

GMC Syn

Tool for synthesising a choreography from Genalised Multiparty Compatible CFSMs

The tool allows to

• Check that a set of CFSM is Generalised Multiparty Compatible (GMC)
• Synthesise a choreography (global graph) which is equivalent to the input CFSMs.

Godel Checker

Go model checker for MiGo types

godel-checker is a model checker for MiGo types, and uses the output of the MiGo type extractor gospal. This tool is part of the Go static verification framework described in this work.

Godel2

Go model checker for MiGo types, version 2

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

Channel Liveness and Safety checker

Gong is a liveness and safety checker for MiGo types.

HAPI

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.

KMC

a tool for checking k-multiparty compatibility in communicating session automata

Lchannels

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.

mpstk

the Mutliparty Session Types toolKit

mpstk is a toolkit for specifying multiparty protocols and verifying their properties (e.g., deadlock-freedom and liveness).

mpstpp

Multiparty Session Types Plus +

MultiCrusty

MultiCrusty is a Rust implementation for Multiparty Session Types.

This tool allows the user to write and check communication protocols directly in Rust. It can also be used with Scribble or KMC.

Multiparty PGCD

Multiparty Motion Coordination: From Choreographies to Robotics Programs

This artifact, for the related OOPSLA 2020 publication below, covers the verification results presented in the paper.

ocaml-mpst

a communication library powered by Multiparty Session Types in OCaml

ocaml-mpst is a communication library powered by Multiparty Session Types (abbreviated as MPST) in OCaml. Thus it ensures:

• Deadlock-freedom,
• Protocol fidelity (communication will take place according to a prescribed protocol) and
• Communication safety (you do not get any type-mismatch errors)

--- under the assumption that all communication channels are used linearly.

Pabble

Parameterised Scribble

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

Parallel Algebraic Language

A Haskell EDSL for building session-typed parallel code.

Rumpsteak

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.

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.

Scribble-Go

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:

• support for role-parametricity;
• support for Go.

SePi

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.

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.

Session OCaml

A novel library for concurrent/distributed programming in OCaml

Session-ocaml is an implementation of session types in OCaml.

Session Type Providers

STP is a type provider for F# that generates APIs from protocol specifications

STP is a type provider in F# that generates APIs from protocol specifications.

Session*

A Toolchain for Statically-Verified Refinements for Multiparty Protocols

Session* is a toolchain for specifying message passing protocols using Refined Multiparty Session Types and safely implementing the distributed endpoint programs in F*.

STScript

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.

Zooid

𝝼scr

An implementation of MPST toolchain in OCaml

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).