Precise subtyping for asynchronous multiparty sessions
File(s)
Published version
Author(s)
Ghilezan, Silvia
Pantović, Jovanka
Prokić, Ivan
Scalas, Alceste
Yoshida, Nobuko
Type
Conference Paper
Abstract
Session subtyping is a cornerstone of refinement of communicating processes: a process implementing a session type (i.e., a communication protocol) T can be safely used whenever a process implementing one of its supertypes T′ is expected, in any context, without introducing deadlocks nor other communication errors. As a consequence, whenever T T′ holds, it is safe to replace an implementation of T′ with an implementation of the subtype T, which may allow for more optimised communication patterns.
We present the first formalisation of the precise subtyping relation for asynchronous multiparty sessions. We show that our subtyping relation is sound (i.e., guarantees safe process replacement, as outlined above) and also complete: any extension of the relation is unsound. To achieve our results, we develop a novel session decomposition technique, from full session types (including internal/external choices) into single input/output session trees (without choices).
Previous work studies precise subtyping for binary sessions (with just two participants), or multiparty sessions (with any number of participants) and synchronous interaction. Here, we cover multiparty sessions with asynchronous interaction, where messages are transmitted via FIFO queues (as in the TCP/IP protocol), and prove that our subtyping is both operationally and denotationally precise. In the asynchronous multiparty setting, finding the precise subtyping relation is a highly complex task: this is because, under some conditions, participants can permute the order of their inputs and outputs, by sending some messages earlier or receiving some later, without causing errors; the precise subtyping relation must capture all such valid permutations — and consequently, its formalisation, reasoning and proofs become challenging. Our session decomposition technique overcomes this complexity, expressing the subtyping relation as a composition of refinement relations between single input/output trees, and providing a simple reasoning principle for asynchronous message optimisations.
We present the first formalisation of the precise subtyping relation for asynchronous multiparty sessions. We show that our subtyping relation is sound (i.e., guarantees safe process replacement, as outlined above) and also complete: any extension of the relation is unsound. To achieve our results, we develop a novel session decomposition technique, from full session types (including internal/external choices) into single input/output session trees (without choices).
Previous work studies precise subtyping for binary sessions (with just two participants), or multiparty sessions (with any number of participants) and synchronous interaction. Here, we cover multiparty sessions with asynchronous interaction, where messages are transmitted via FIFO queues (as in the TCP/IP protocol), and prove that our subtyping is both operationally and denotationally precise. In the asynchronous multiparty setting, finding the precise subtyping relation is a highly complex task: this is because, under some conditions, participants can permute the order of their inputs and outputs, by sending some messages earlier or receiving some later, without causing errors; the precise subtyping relation must capture all such valid permutations — and consequently, its formalisation, reasoning and proofs become challenging. Our session decomposition technique overcomes this complexity, expressing the subtyping relation as a composition of refinement relations between single input/output trees, and providing a simple reasoning principle for asynchronous message optimisations.
Date Issued
2021-01-04
Date Acceptance
2020-12-01
Citation
Proceedings of the ACM on Programming Languages, 2021, 5, pp.1-28
ISSN
2475-1421
Publisher
Association for Computing Machinery (ACM)
Start Page
1
End Page
28
Journal / Book Title
Proceedings of the ACM on Programming Languages
Volume
5
Copyright Statement
© 2021 Copyright held by the owner/author(s). This work is licensed under a Creative Commons Attribution-ShareAlike 4.0 International License (https://creativecommons.org/licenses/by-sa/4.0/)
License URL
Sponsor
Engineering & Physical Science Research Council (EPSRC)
Engineering & Physical Science Research Council (EPSRC)
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (E
Engineering and Physical Sciences Research Council
Engineering & Physical Science Research Council (EPSRC)
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (EPSRC)
Engineering and Physical Sciences Research Council
Engineering & Physical Science Research Council (E
The National Cyber Security Centre (NCSC)
Grant Number
EP/T006544/1
EP/K011715/1
ERI 025567 (EP/K034413/1)
PO 20131167
EP/L00058X/1, PO 20131167
EP/N027833/1
20103649
EP/T014709/1
EP/V000462/1
EP/V000462/1
4214176 / RFA 20601
Source
POPL 2021
Publication Status
Published
Start Date
2021-01-17
Finish Date
2021-01-22
Coverage Spatial
Virtual