一句话：将可逆语义扩展到异步多方会话协议，并证明其回滚满足因果一致性。
在带行为类型的通信中心进程语言中，可逆语义允许撤销计算步骤，但已有工作仅覆盖同步通信的二元协议，表达力受限。本文把“监视器即记忆”方法扩展到更丰富的进程模型，支持多方（n-party）协议、异步通信、解耦回滚和抽象传递，从而为多方协议定义可逆语义。为便于技术处理，作者还提出一种带原子回滚的替代可逆语义，并证明它可刻画解耦回滚。主要结果是证明该多方协议可逆语义满足因果一致性，即回滚不会破坏因果依赖，为可逆通信系统的正确性提供语义保证。
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.
@article{paperbot1273,
title = {Causal Consistency for Reversible Multiparty Protocols},
author = {Claudio Antares Mezzina and Jorge A. Pérez},
journal = {Logical Methods in Computer Science},
volume = {Volume 17, Issue 4},
year = {2021},
doi = {10.46298/lmcs-17(4:1)2021}
}