Asynchronous Multiparty Session Type Implementability is Decidable – Lessons Learned from Message Sequence Charts
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 JulDisplayed 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 15mTalk | 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 15mTalk | Asynchronous Multiparty Session Type Implementability is Decidable – Lessons Learned from Message Sequence Charts Research Papers Felix Stutz MPI-SWS DOI | ||
16:00 15mTalk | Dynamically Updatable Multiparty Session Protocols Research Papers DOI | ||
16:15 15mTalk | 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 15mTalk | 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 15mTalk | 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 |