Mixed Choice in Asynchronous Multiparty Session Types Artifact

Read full text
Authors: Laura Bocchi, Raymond Hu, A. Laura Voinea, Simon Thompson
Cited by: 1

Abstract

This artifact demonstrates the prototype toolchain presented in the paper "Mixed Choice in Asynchronous Multiparty Session Types". It allows the user to:1. Specify the message-passing protocol using our mixed-choice extension of the Scribble protocol language. Our tool statically validates the syntactic well-formedness conditions based on the theory presented in the paper. If the protocol is valid, it generates two Erlang modules for each role: * A protocol-enforcing generic behaviour module: gen_ .erl This module is a library that programmers use but do not modify. It provides a protocol- and role-specific gen_statem wrapper that enforces the protocol rules for the given role. It encapsulates the EFSM logic derived from the protocol for this role, including state transitions, message handling, and runtime mechanisms for mixed-choice and garbage collection. It exposes a public API for sending messages. * A template callback module: .erl This module provides a template implementation of a user program on top of the generic behaviour module. Code generation creates placeholder callback functions for handling EFSM events. The programmer can modify these (and add new ones) to implement the required application-specific logic (e.g., local computations after receiving a message, internal decisions for selecting protocol choices, etc.).2. Adapt and complete the generated template programs. The programmer can complete the program as follows: * Modify and extend the placeholder functions in the template ( .erl) with application-specific logic. * Configure how the different roles will be launched and connected at startup. This may include: * Launching a process for each role in the protocol. * Distributing the initial contact information (process IDs) so the roles know how to communicate with each other (the connection function generated in .erl can be used for this). * Providing supervision of these processes for fault tolerance.

Publication details

Journal / source
Zenodo (CERN European Organization for Nuclear Research)
Publication date
27 February 2026