Claudio Antares Mezzina ; Jorge A. Pérez - Causal Consistency for Reversible Multiparty Protocols

lmcs:6997 - Logical Methods in Computer Science, October 1, 2021, Volume 17, Issue 4 - https://doi.org/10.46298/lmcs-17(4:1)2021
Causal Consistency for Reversible Multiparty ProtocolsArticle

Authors: Claudio Antares Mezzina ; Jorge A. Pérez

    In programming models with a reversible semantics, computational steps can be undone. This paper addresses the integration of reversible semantics into process languages for communication-centric systems equipped with behavioral types. In prior work, we introduced a monitors-as-memories approach to seamlessly integrate reversible semantics into a process model in which concurrency is governed by session types (a class of behavioral types), covering binary (two-party) protocols with synchronous communication. The applicability and expressiveness of the binary setting, however, is limited. Here we extend our approach, and use it to define reversible semantics for an expressive process model that accounts for multiparty (n-party) protocols, asynchronous communication, decoupled rollbacks, and abstraction passing. As main result, we prove that our reversible semantics for multiparty protocols is causally-consistent. A key technical ingredient in our developments is an alternative reversible semantics with atomic rollbacks, which is conceptually simple and is shown to characterize decoupled rollbacks.


    Volume: Volume 17, Issue 4
    Published on: October 1, 2021
    Accepted on: September 6, 2021
    Submitted on: December 21, 2020
    Keywords: Computer Science - Logic in Computer Science,D.3.1,F.3.2
    Funding:
      Source : OpenAIRE Graph
    • Causal debugging for concurrent systems; Funder: French National Research Agency (ANR); Code: ANR-18-CE25-0007

    2 Documents citing this article

    Consultation statistics

    This page has been seen 1793 times.
    This article's PDF has been downloaded 410 times.