Wed 19 Jul 2023 16:00 - 16:15 at Amazon Auditorium (Gates G20) - ECOOP 3: Distribution Chair(s): Elisa Gonzalez Boix

Multiparty Session Types (MPST) are a typing discipline that guarantees the absence of deadlocks and communication errors in concurrent and distributed systems. However, existing MPST frameworks do not support protocols with dynamic unbounded participants, and cannot express many common programming patterns that require the introduction of new participants into a protocol. This can pose a barrier for the adoption of MPST-based techniques to programming languages that favour the creation of new participants (processes, lightweight threads, etc) that communicate via message passing, such as Go or Erlang.

This paper proposes dynamically updatable unbounded multiparty session protocols, a new session types theory (DMst) that supports protocols with an unbounded number of fresh participants, whose communication structures are dynamically updatable during a protocol execution. We prove that DMst guarantees deadlock-freedom and liveness. We implement a toolchain, GoScr (Go-Scribble), which generates Go implementations from DMst, ensuring by construction, that the different participants will only perform I/O actions that comply with a given protocol specification. We evaluate our toolchain by (1) implementing representative parallel and concurrent algorithms from existing benchmarks, textbooks and literature; (2) showing that GoScr does not introduce significant overheads compared to a naive implementation, for computationally expensive benchmarks; and (3) building three realistic protocols (dynamic task delegation, recursive Domain Name System, and a parallel Min-Max strategy) in GoScr that could not be represented with previous theories of session types.

Wed 19 Jul

Displayed time zone: Pacific Time (US & Canada) change

15:30 - 17:00
ECOOP 3: DistributionResearch Papers at Amazon Auditorium (Gates G20)
Chair(s): Elisa Gonzalez Boix Vrije Universiteit Brussel
15:30
15m
Talk
Synthetic Behavioural Typing: Sound, Regular Multiparty Sessions via Implicit Local Types
Research Papers
Sung-Shik Jongmans Open University of the Netherlands; CWI, Francisco Ferreira Royal Holloway, University of London
DOI
15:45
15m
Talk
Asynchronous Multiparty Session Type Implementability is Decidable – Lessons Learned from Message Sequence Charts
Research Papers
Felix Stutz MPI-SWS
DOI
16:00
15m
Talk
Dynamically Updatable Multiparty Session Protocols
Research Papers
David Castro-Perez University of Kent, Nobuko Yoshida University of Oxford
DOI
16:15
15m
Talk
Designing Asynchronous Multiparty Protocols with Crash-Stop Failures
Research Papers
Adam D. Barwell University of St Andrews and University of Oxford, Ping Hou University of Oxford, Nobuko Yoshida University of Oxford, Fangyi Zhou Imperial College London
DOI Pre-print
16:30
15m
Talk
ConDRust: Scalable Deterministic Concurrency from Verifiable Rust Programs
Research Papers
Felix Suchert Center for Advancing Electronics Dresden, TU Dresden, Lisza Zeidler Composable Operating Systems Group, Barkhausen Institute, Dresden, Jeronimo Castrillon TU Dresden, Germany, Sebastian Ertel Composable Operating Systems Group, Barkhausen Institute, Dresden
DOI
16:45
15m
Talk
Information Flow Analysis for Detecting Non-Determinism in Blockchain
Research Papers
Luca Olivieri Ca’ Foscari University of Venice, Vincenzo Arceri University of Parma, Italy, Luca Negrini Ca’ Foscari University of Venice, Corvallis S.r.l., Fabio Tagliaferro CYS4 Srl, Pietro Ferrara Università Ca' Foscari, Venezia, Italy, Agostino Cortesi Università Ca' Foscari Venezia, Fausto Spoto U. Verona
DOI