A sound algorithm for asynchronous session subtyping and its implementation
File(s)Sound Algorithm for Asynchronous Session.pdf (656.88 KB)
Published version
Author(s)
Bravetti, Mario
Carbone, Marco
Lange, Julien
Yoshida, Nobuko
Zavattaro, Gianluigi
Type
Journal Article
Abstract
Session types, types for structuring communication between endpoints in distributed systems, are recently being integrated into mainstream programming languages. In practice, a very important notion for dealing with such types is that of subtyping, since it allows for typing larger classes of system, where a program has not precisely the expected behaviour but a similar one. Unfortunately, recent work has shown that subtyping for session types in an asynchronous setting is undecidable. To cope with this negative result, the only approaches we are aware of either restrict the syntax of session types or limit communication (by considering forms of bounded asynchrony). Both approaches are too restrictive in practice, hence we proceed differently by presenting an algorithm for checking subtyping which is sound, but not complete (in some cases it terminates without returning a decisive verdict). The algorithm is based on a tree representation of the coinductive definition of asynchronous subtyping; this tree could be infinite, and the algorithm checks for the presence of finite witnesses of infinite successful subtrees. Furthermore, we provide a tool that implements our algorithm. We use this tool to test our algorithm on many examples that cannot be managed with the previous approaches, and to provide an empirical evaluation of the time and space cost of the algorithm.
Date Issued
2021-03-04
Date Acceptance
2021-02-02
Citation
Logical Methods in Computer Science, 2021, 17 (1), pp.1-35
ISSN
1860-5974
Publisher
Technical University of Braunschweig
Start Page
1
End Page
35
Journal / Book Title
Logical Methods in Computer Science
Volume
17
Issue
1
Copyright Statement
© M. Bravetti, M. Carbone, J. Lange, N. Yoshida, and G. Zavattaro. This work is licensed under the Creative Commons Attribution License. To view a copy of this license, visit https://creativecommons.org/licenses/by/4.0/ or send a letter to Creative Commons, 171 Second St, Suite 300, San Francisco, CA 94105, USA, or Eisenacher Strasse 2, 10777 Berlin, Germany
License URL
Sponsor
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (EPSRC)
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
Engineering & Physical Science Research Council (EPSRC)
The National Cyber Security Centre (NCSC)
Identifier
https://lmcs.episciences.org/7238
Grant Number
ERI 025567 (EP/K034413/1)
EP/K011715/1
PO 20131167
EP/L00058X/1, PO 20131167
EP/N027833/1
20200046
EP/T014709/1
EP/V000462/1
EP/V000462/1
EP/T006544/1
4214176 / RFA 20601
Subjects
0101 Pure Mathematics
0802 Computation Theory and Mathematics
0803 Computer Software
Publication Status
Published
Article Number
5974
Date Publish Online
2021-03-04