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

Multiparty session types (MSTs) provide efficient means to specify and verify asynchronous message-passing systems. For a global type, which specifies all interactions between roles in a system, the implementability problem asks whether there are local specifications for all roles such that their composition is deadlock-free and generates precisely the specified executions. Decidability of the implementability problem is an open question. We answer it positively for global types with generalised choice, which allow a sender to send to different receivers and a receiver to receive from different senders upon branching. To achieve this, we generalise results from the domain of high-level message sequence charts (HMSCs). This connection also allows us to comprehensively investigate how HMSC techniques can be adapted to the MST setting. This comprises techniques to make the problem algorithmically more tractable as well as a variant of implementability that may open new design space for MSTs. Inspired by potential performance benefits, we introduce a generalisation of the implementability problem that we, unfortunately, prove to be undecidable.

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