Stardust meeting at Kent
(12th-13th September 2022)

Location

The meeting will be held on September 12th and 13th 2022 at the University of Kent (Keynes College, see map, in Atrium Foyer and KLT2). This will be an in person meeting on September 12th with hybrid sessions on September 13th. Instructions to join the hybrid event online will be sent by email. If you have problems or need further information, please contact Laura Bocchi.

Monday 12 September

10:30 - 12.30	Arrival	Atrium Foyer
12:30 - 13.30	Lunch	Atrium Foyer
13:30 - 14.00	Updates by the sites	KLT2
14:00 - 15:30	Talks 14:00: A Model of Grey Failures for actor-based systems (Laura Bocchi) 14:30: Special Delivery: Programming with Mailbox Types (Simon Fowler) 15:00: Generalised Multiparty Session Types with Crash-Stop Failures (Fangyi Zhou)	KLT2
15:30 - 16.00	Coffee break	Foyer atrium
16:00 - 17:30	Talks 16:00:A Multiparty Session Typing Discipline for Fault-Tolerant Event-Driven Distributed Programming (Raymond Hu) 16:30 : Stay Safe under Panic: Affine Rust Programming with Multiparty Session Types (Nicolas Lagaillardie) 17:00 :A Monitoring Tool for Linear-Time µHML (Duncan Attard)	KLT2
17:30 - 18.30	Discussion	KLT2

Tuesday 13 September

9:30 - 10.30	Updates (repeat) by academic partners	KLT2 and online
10:30 - 11.00	Coffee break	Atrium Foyer
11:00 - 12.00	Updates by industry partners 11:00 : Natalia Chechina (Erlang Solutions) 11:20 : Roland Kuhn (Actyx) 11:40 : Discussion	KLT2 and online
12:00 - 12.30	Planning and closing	KLT2 and online
12:30 - 13:30	Lunch	Atrium Foyer

Abstracts & Slides

• A Monitoring Tool for Linear-Time µHML (by Duncan Attard)
  We present the implementation of a prototype tool that runtime checks specifications written in a maximally-expressive safety fragment of the linear-time modal µ-calculus called maxHML. Our technical development is founded on previous results that give a compositional synthesis procedure for generating monitors from maxHML formulae. This paper instantiates this synthesis to a first-order setting, where systems produce executions containing events that carry data. We augment the logic with predicates over data, and extend the synthesis procedure to generate executable monitors for Erlang, a general-purpose programming language. These monitors are instrumented via inlining to induce minimal runtime overhead. Our monitoring algorithm also maintains information, which it uses to explain how verdicts are reached. (joint work with Luca Aceto, Antonis Achilleos, Léo Exibard, Adrian Francalanza, and Anna Ingólfsdóttir).
• A model of grey failure for actor-based systems (by Laura Bocchi)
  Existing models for the analysis of concurrent processes tend to focus on fail-stop failures, where processes are either working or permanently stopped, and their state (working/stopped) is known. In fact, systems are often affected by grey failures: failures that are latent, possibly transient, and may affect the system in subtle ways that later lead to major issues (such as crashes, limited availability, overload). We introduce a model of actor-based systems with grey failures, based on two interlinked layers: an actor model, given as an asynchronous process calculus with discrete time, and a failure model that represents failure patterns to inject in the system. Our failure model captures not only fail-stop node and link failures, but also grey failures (e.g., partial, transient). We give a behavioural equivalence relation based on weak barbed bisimulation to compare systems on the basis of their ability to recover from failures, and on this basis we define some desirable properties of reliable systems. By doing so, we reduce the problem of checking reliability properties of systems to the problem of checking bisimulation. (joint work with Julien Lange, Simon Thompson, and Laura Voinea)
• Special Delivery: Programming with Mailbox Types (by Simon Fowler)
  Actor-based languages such as Erlang and Elixir are well-suited to distributed programming due to the concept of a *mailbox*: a message queue local to each thread of execution. However, actor languages are vulnerable to subtle yet insidious programmer errors such as protocol violations and communication mismatches, which can be difficult to locate and fix. Mailbox types, proposed by de'Liguoro and Padovani in 2018, are a behavioural type system which captures the contents of a mailbox using a commutative regular expression, and can rule out common communication errors such as protocol violations, payload mismatches, and some deadlocks. In this work, we present the first theoretical and practical integration of mailbox types into a programming language. Unlike session type systems, the many-writer, single-reader nature of mailboxes poses nontrivial challenges for language integration. We address these challenges through the use of Kobayashi's notion of quasi-linearity, and develop a co-contextual algorithmic type system based on backwards bidirectional typing. (joint work with Simon Gay, Phil Trinder, and Franciszek Sowul)
• A Multiparty Session Typing Discipline for Fault-Tolerant Event-Driven Distributed Programming (by Raymond Hu)
  Multiparty Session Types (MSTs) is a types systems approach to specifying multiparty message passing protocols and verifying their process implementations. A long standing challenge for MSTs is reasoning about failure handling of protocol participants -- a crucial requirement for practical applicability of MSTs to many distributed systems. In this work, we draw inspiration from real-world distributed systems, notably Apache Spark, to develop an MST framework for fault-tolerant application protocols, supported by an event-driven model of session concurrency. Our framework ensures communication safety and progress for well-typed systems in the presence of asynchronous and concurrent process failures; moreover, event-driven concurrency enables progress in the presence of multiple, concurrently interleaved sessions, which is not guaranteed in traditional session calculi. We have used our prototype Scala toolchain to implement a session-typed version of the Spark cluster manager, which is fully capable of running existing third-party Spark user applications without any code modification. (joint work with Malte Viering, Patrick Eugster and Lukasz Ziarek)
• Stay Safe under Panic: Affine Rust Programming with Multiparty Session Types (by Nicolas Lagaillardie)
  Communicating systems comprise diverse software components across networks. To ensure their robustness, modern programming languages such as Rust provide both strongly typed channels, whose usage is guaranteed to be affine (at most once), and cancellation operations over binary channels. For coordinating components to correctly communicate and synchronise with each other, we use the structuring mechanism from multiparty session types, extending it with affine communication channels and implicit/explicit cancellation mechanisms. This new typing discipline, affine multiparty session types (AMPST), ensures cancellation termination of multiple, independently running components and guarantees that communication will not get stuck due to error or abrupt termination. Guided by AMPST, we implemented an automated generation tool (MultiCrusty) of Rust APIs associated with cancellation termination algorithms, by which the Rust compiler auto-detects unsafe programs. Our evaluation shows that MultiCrusty provides an efficient mechanism for communication, synchronisation and propagation of the notifications of cancellation for arbitrary processes. We have implemented several usecases, including popular application protocols (OAuth, SMTP), and protocols with exception handling patterns (circuit breaker, distributed logging). (joint work with Rumyana Neykova, and Nobuko Yoshida)
• Generalised Multiparty Session Types with Crash-Stop Failures (by Fangyi Zhou)
  Session types enable the specification and verification of communicating systems. However, their theory often assumes that processes never fail. To address this limitation, we present a generalised multiparty session type (MPST) theory with crash-stop failures, where processes can crash arbitrarily. Our new theory validates more protocols and processes w.r.t. previous work. We apply minimal syntactic changes to standard session pi-calculus and types: we model crashes and their handling semantically, with a generalised MPST typing system parametric on a behavioural safety property. We cover the spectrum between fully reliable and fully unreliable sessions, via optional reliability assumptions, and prove type safety and protocol conformance in the presence of crash-stop failures. Introducing crash-stop failures has non-trivial consequences: writing correct processes that handle all possible crashes can be difficult. Yet, our generalised MPST theory allows us to tame this complexity, via model checkers, to validate whether a multiparty session satisfies desired behavioural properties, e.g. deadlock-freedom or liveness. We implement our approach using the mCRL2 model checker, and evaluate it with examples extended from the literature. (joint work with Adam D. Barwell, Alceste Scalas, and Nobuko Yoshida)