A Sound Algorithm for Asynchronous Session Subtyping and its Implementation
2021
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.
- Correction
- Source
- Cite
- Save
- Machine Reading By IdeaReader
0
References
0
Citations
NaN
KQI