Under a reversible semantics, computation steps can be undone. This paperaddresses the integration of reversible semantics into process languages forcommunication-centric systems, equipped with behavioral types. In prior work, we introduced a monitors-as-memories approach to seamlesslyintegrate reversible semantics into a process model in which concurrency isgoverned by session types (a class of behavioral types), covering binary(two-party) protocols with synchronous communications. Although such a modeloffers a simple setting for showcasing our approach, its expressiveness israther limited. Here we substantially extend our approach, and use it to define reversiblesemantics for a very expressive process model that accounts for multiparty(n-party) protocols (choreographies), asynchronous communication, decoupledrollbacks, and process passing. As main technical result, we prove that ourmultiparty, reversible semantics is causally-consistent.
展开▼
