Mario Bravetti ; Marco Carbone ; Julien Lange ; Nobuko Yoshida ; Gianluigi Zavattaro - A Sound Algorithm for Asynchronous Session Subtyping and its Implementation

lmcs:5974 - Logical Methods in Computer Science, March 4, 2021, Volume 17, Issue 1 - https://doi.org/10.23638/LMCS-17(1:20)2021
A Sound Algorithm for Asynchronous Session Subtyping and its ImplementationArticle

Authors: Mario Bravetti ; Marco Carbone ; Julien Lange ; Nobuko Yoshida ; Gianluigi Zavattaro

    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.


    Volume: Volume 17, Issue 1
    Published on: March 4, 2021
    Accepted on: February 1, 2021
    Submitted on: December 16, 2019
    Keywords: Computer Science - Programming Languages
    Funding:
      Source : OpenAIRE Graph
    • Exploiting Parallelism through Type Transformations for Hybrid Manycore Systems; Funder: UK Research and Innovation; Code: EP/L00058X/1
    • From Data Types to Session Types---A Basis for Concurrency and Distribution; Funder: UK Research and Innovation; Code: EP/K034413/1
    • Turtles: Protocol-Based Foundations for Distributed Multiagent Systems; Funder: UK Research and Innovation; Code: EP/N027833/1
    • Conversation-Based Governance for Distributed Systems by Multiparty Session Types; Funder: UK Research and Innovation; Code: EP/K011715/1
    • AppControl: Enforcing Application Behaviour through Type-Based Constraints; Funder: UK Research and Innovation; Code: EP/V000462/1
    • POST: Protocols, Observabilities and Session Types; Funder: UK Research and Innovation; Code: EP/T006544/1
    • Behavioural Application Program Interfaces; Funder: European Commission; Code: 778233

    1 Document citing this article

    Consultation statistics

    This page has been seen 1801 times.
    This article's PDF has been downloaded 455 times.