SPLASH 2023
Sun 22 - Fri 27 October 2023 Cascais, Portugal
Fri 27 Oct 2023 16:00 - 16:18 at Room I - distribution & networking 2 Chair(s): Elisa Gonzalez Boix

Multiparty session types (MPST) are a specification and verification framework for distributed message-passing systems. The communication protocol of the system is specified as a \emph{global type}, from which a collection of \emph{local types} (local process implementations) is obtained by \emph{endpoint projection}. A global type is a single disciplining entity for the whole system, specified by \emph{one designer} that has full knowledge of the communication protocol. On the other hand, distributed systems are often described in terms of their \emph{components}: a different designer is in charge of providing a subprotocol for each component. The problem of modular specification of global protocols has been addressed in the literature, but the state of the art focuses only on dual input/output compatibility. Our work overcomes this limitation. We propose the first MPST theory of \emph{multiparty compositionality for distributed protocol specification} that is semantics-preserving, allows the composition of two or more components, and retains full MPST expressiveness. We introduce \emph{hybrid types} for describing subprotocols interacting with each other, define a novel \emph{compatibility relation}, explicitly describe an algorithm for composing multiple subprotocols into a \emph{well-formed global type}, and prove that compositionality preserves projection, thus retaining semantic guarantees, such as liveness and deadlock freedom. Finally, we test our work against real-world case studies and we smoothly extend our novel compatibility to MPST with delegation and explicit connections.

Fri 27 Oct

Displayed time zone: Lisbon change

16:00 - 17:30
distribution & networking 2OOPSLA at Room I
Chair(s): Elisa Gonzalez Boix Vrije Universiteit Brussel
16:00
18m
Talk
Hybrid Multiparty Session Types: Compositionality for Protocol Specification through Endpoint Projection
OOPSLA
Lorenzo Gheri University of Liverpool, Nobuko Yoshida University of Oxford
DOI
16:18
18m
Talk
Mechanizing Session-Types using a Structural View: Enforcing Linearity without Linearity
OOPSLA
Chuta Sano McGill University, Ryan Kavanagh McGill University, Brigitte Pientka McGill University
DOI
16:36
18m
Talk
Message Chains for Distributed System Verification
OOPSLA
Federico Mora University of California at Berkeley, Ankush Desai Amazon Web Services, Elizabeth Polgreen University of Edinburgh, Sanjit A. Seshia University of California at Berkeley
DOI
16:54
18m
Talk
Randomized Testing of Byzantine Fault Tolerant AlgorithmsDistinguished Paper
OOPSLA
Levin N. Winter Delft University of Technology, Florena Buse Delft University of Technology, Daan de Graaf Delft University of Technology, Klaus von Gleissenthall Vrije Universiteit Amsterdam, Burcu Kulahcioglu Ozkan Delft University of Technology
DOI
17:12
18m
Talk
Validating IoT Devices with Rate-Based Session Types
OOPSLA
Grant Iraci University at Buffalo, Cheng-En Chuang University at Buffalo, Raymond Hu Queen Mary University of London, Lukasz Ziarek University at Buffalo
DOI