Causal Consistent Replication in Reversible Concurrent Calculi

TL;DR

This paper introduces a reversible concurrent calculus with a replication operator, providing a syntactical definition of causality and enabling the modeling of infinite behaviors while ensuring causal consistency.

Contribution

It develops a new reversible calculus with replication, offering a clear syntactical notion of concurrency and causal consistency for infinite behaviors.

Findings

First reversible system with infinite behaviors and causal consistency

Defines a syntactical notion of reversible concurrency

Leverages transition systems for concurrency definition

Abstract

Reversible computation is key in developing new, energy-efficient paradigms, but also in providing forward-only concepts with broader definitions and finer frames of study.Among other fields, the algebraic specification and representation of networks of agents have been greatly impacted by the study of reversible phenomena: reversible declensions of the calculus of communicating systems (CCSK and RCCS) offer new semantic models, finer congruence relations, original properties, and revisits existing theories and results in a finer light.However, much remains to be done: concurrency, a central notion in establishing causal consistency--a crucial property for reversibly systems--, was never given a clear and syntactical definition in CCSK.While recursion was mentioned as a possible mechanism to inject infinite behaviors into the systems, replication was never studied.This work offers a solution to both problems, by leveraging a definition of concurrency developed for forward-only calculi using proved transition systems, by endowing CCSK with a replication operator, and by studying the interplay of both notions.The system we obtain is the first reversible system capable of representing infinite behaviors that enjoys causal consistency, for our simple and purely syntactical notion of reversible concurrency.