EVENT

Event News

ERATO Project Colloquium by Thomas Haas and Nobuko Yoshida

On Tuesday 20 August, Thomas Haas (Technical University of Braunschweig) and Nobuko Yoshida (University of Oxford) will give talks for our project colloquium. Further details can be found below.

Talk 1:

Formal specification language CAT for weak memory models and bounded model checking with Dartagnan

Speaker:

Thomas Haas (Technical University of Braunschweig)

Abstract:

Modern compilers, CPUs, and GPUs perform many optimisations on program executions, such as reordering of memory operations. While these optimisations are invisible to single-threaded programs, they are observable in concurrent programs and can lead to extra, possibly buggy behaviours when not accounted for. The range of behaviours permitted by hardware and/or source language are described by their so-called (weak) memory models.
In order to uniformly formulate these (wildly different) memory models, Jade Alglave and Luc Maranget developed the CAT language. In this tutorial we will present the CAT language, its features, and how it is used to define an axiomatic program semantics. We also present the bounded model checker Dartagnan which can find bugs in programs under weak memory models, taking both the program and the memory model as input.

Talk 2:

Nobuko Yoshida (University of Oxford)

Speaker:

Separation and Encodability in Mixed Choice Multiparty Sessions

Abstract:

Multiparty session types (MPST) are a type discipline for enforcing the structured, deadlock-free communication of concurrent and message-passing programs. Traditional MPST have a limited form of choice in which alternative communication possibilities are offered by a single participant and selected by another. Mixed choice multiparty session types (MCMP) extend the choice construct to include both selections and offers in the same choice.
This talk presents a mixed choice synchronous multiparty session calculus and its typing system, which guarantees communication safety and deadlock-freedom. We then talk expressiveness of nine subcalculi of MCMP-calculus by examining their encodability (there exists a good encoding from one to another) and separation (there exists no good encoding from one calculus to another). The highlight is the binary (2-party) mixed sessions by Casal et al (2022) is strictly less expressive than the MCMP-calculus.
A joint work with Kirstin Peters appeared in LICS'24 (https://arxiv.org/abs/2405.08104)