Stardust meeting at Glasgow
(18th and 19th December 2023)

Location

The meeting will be held on December 18th and 19th, 2023, at the University of Glasgow (Sir Alwyn Williams Building, see map, in rooms 422 and 423). The meeting will be held in both in-person and hybrid sessions. Instructions on how to join the hybrid sessions will be sent via email. In case of problems or further information, contact Simon Fowler.

Monday 18th December (09:00 - 17:00)

09:00 - 09:25 Arrival and coffee Outside SAWB 423
09:25 - 10:30

Technical session 1

09:25: Welcome and day overview

09:30: Designing Asynchronous Multiparty Protocols with Crash-Stop Failures (Ping Hou, Oxford)

10:00: Towards Mailbox Typing for Erlang (Duncan Paul Attard, Glasgow)

 SAWB 423
10:30 - 11:00 Coffee Outside SAWB 423
11:00 - 12:00

Technical session 2

11:00: Erlang Semantics in Coq (Simon Thompson, Kent)

11:30: Synchronisability and Communicating Session Automata (Amrita Suresh, Oxford)

 SAWB 423
12:00 - 13:30 Lunch Outside SAWB 423
13:30 - 14:30

Technical session 3

13:30: Event-Driven Multiparty Session Actors (Simon Fowler, Glasgow)

14:00: Behavioural Types for Local-First Software (Roland Kuhn, Actyx)

 SAWB 423
14:30 - 15:00 Coffee Outside SAWB 423
15:00 - 17:00

Technical session 4 and discussion

15:00: Asynchronous Subtyping by Trace Relaxation (Andy King, Kent)

15:30: Structured discussion

 SAWB 423
18:00 Dinner Ashoka (Ashton Lane)

Tuesday 19th December (09:00 - 13:00)

09:00 - 09:30 Coffee Outside SAWB 422
09:30 - 11:00

Status reports and discussion

 SAWB 422
11:00 - 11:30 Coffee Outside SAWB 422
11:30 - 12:00

Industry session

11:30: Discussion of issues and ideas from industry partners

 SAWB 422
12:00 Closing and lunch TBA

Status reports

  1. Glasgow (Simon Gay)
  2. Kent (Laura Bocchi)
  3. Oxford (Nobuko Yoshida)

Abstracts and slides

  1. Designing Asynchronous Multiparty Protocols with Crash-Stop Failures (Ping Hou, Oxford)
    Session types provide a typing discipline for message-passing systems. However, most session type approaches assume an ideal world: one in which everything is reliable and without failures. Yet this is in stark contrast with distributed systems in the real world. To address this limitation, we introduce Teatrino, a code generation toolchain that utilises asynchronous multiparty session types (MPST) with crash-stop semantics to support failure handling protocols. We augment asynchronous MPST and processes with crash handling branches. Our approach requires no user-level syntax extensions for global types and features a formalisation of global semantics, which captures complex behaviours induced by crashed/crash handling processes. The sound and complete correspondence between global and local type semantics guarantees deadlock- freedom, protocol conformance, and liveness of typed processes in the presence of crashes. Our theory is implemented in the toolchain Teatrino, which provides correctness by construction. Teatrino extends the Scribble multiparty protocol language to generate protocol-conforming Scala code, using the Effpi concurrent programming library. We extend both Scribble and Effpi to support crash-stop behaviour. We demonstrate the feasibility of our methodology and evaluate Teatrino with examples extended from both session type and distributed systems literature.
  2. Towards Mailbox Typing for Erlang (Duncan Paul Attard, Glasgow)
    This talk summarises our current work on mailbox typing applied to Erlang to uncover specific communication errors statically. We introduce mailbox typing, a behavioural typing discipline which naturally fits idiomatic actor-style programming. We position our mailbox typing approach in the context of existing error detection tools currently used in Erlang. Our exposition focuses on instantiating mailbox typing to a programming language and the challenges in mapping this concept to Erlang actors having one implicit mailbox. We highlight our progress in designing a tool for Erlang that leverages prior work and the direction we intend to follow next.
  3. Erlang Semantics in Coq (Simon Thompson, Kent, with Peter Bereczky and Dániel Horpácsi from Eötvös Loránd University, Budapest)
    After describing the context of this work - a longer-term project to make refactoring trustworthy - the talk will describe a semantics for the essential aspects of Erlang fully formalised in the Coq theorem prover. The semantics has three modular, layers: the sequential layer, the process-local layer and the inter-process layer. A number of properties are proved, and notions of program equivalence are also presented. The talk will conclude with a discussion of potential links between this work and the STARDUST project.
  4. Synchronisability and Communicating Session Automata (Amrita Suresh, Oxford)
    In this talk, I will mainly focus on some of the results of my PhD thesis, and highlight some areas of research we are currently investigating. A large part of my thesis included studying the model of communicating automata, i.e. concurrent processes communicating asynchronously via FIFO channels. Since these models are known to have undecidable verification properties, we investigated various subclasses of these automata. In this talk, I will focus mainly on the notion of synchronisability. Roughly, a system is called synchronisable if every execution can be rescheduled so that it meets certain criteria, e.g. a channel bound. However, since there are a lot of conflicting definitions in the literature regarding this notion, we provided a framework that unifies existing definitions and proves decidability (or when the case may be, undecidability) results for these classes. Moreover, I will also talk about some of the current extensions to communicating automata that I am working on, in order to extend these results to potentially faulty communication channels.
  5. Event-Driven Multiparty Session Actors (Simon Fowler, Glasgow)
    Actor languages such as Erlang and Elixir have emerged as popular tools for designing reliable, fault-tolerant distributed applications, but communication patterns used by actors are often informally specified. Multiparty session types (MPSTs) are a type discipline for communication protocols: if a program typechecks according to its session type, then it is guaranteed to fulfil its role in a communication protocol, but the unidirectional communication mechanism used by actors makes it difficult to apply session types to actor languages directly. By combining a flow-sensitive effect system with an event-driven programming model, we show the first statically-typed session type system for actors that can participate in multiple sessions.
  6. Behavioural Types for Local-First Software (Roland Kuhn, Actyx)
    Peer-to-peer systems are the most resilient form of distributed computing, but the design of robust protocols for their coordination is difficult. This makes it hard to specify and reason about global behaviour of such systems. This paper presents swarm protocols to specify such systems from a global viewpoint. Swarm protocols are projected to machines, that is local specifications of peers. This paper introduces an execution model based on log shipping to mitigate this. More precisely, we present specify systems from a global viewpoint, which are projected to machines that yield local specifications. We take inspiration from behavioural types with a key difference: peers communicate through an event notification mechanism rather than through point-to-point message passing. Our goal is to adhere to the principles of local-first software where network devices collaborate on a common task while retaining full autonomy: every participating device can locally make progress at all times, not encumbered by unavailability of other devices or network connections. This coordination-free approach leads to inconsistencies that may emerge during computations. Our main result shows that under suitable well-formedness conditions for swarm protocols consistency is eventually recovered and the locally observable behaviour of conforming machines will eventually match the global specification. The model we propose elaborates on an existing industrial platform and provides the basis for tool support (sketched here and fully described in a companion artifact paper), wherefore we consider this work to be a viable step towards reasoning about local-first and peer-to-peer software systems.
  7. Asynchronous Subtyping by Trace Relaxation (Andy King, Kent)
    Session subtyping answers the question of whether a program in a communicating system can be safely substituted for another, when their communication behaviours are described by session types. Asynchronous session subtyping is undecidable, hence the interest in devising sound, although incomplete, subtyping algorithms. Asynchronous subtyping is formulated in terms of a data-structure called input trees. We show how input trees can be replaced with sets of traces which opens up opportunities for applying abstract interpretation techniques to the problem of session subtyping. Sets of traces which can be relaxed (enlarged) whilst still allowing subtyping to be observed. In particular, relaxations can be chosen which can be finitely represented, even when the input trees are arbitrarily large. We instantiate this strategy using regular expressions and show that it allows subtyping to be mechanically proven for communication patterns that were previously out of reach.