Towards Reversible Sessions

TL;DR

This paper introduces a reversible extension to session-based pi-calculus, enabling automatic undoing of interactions and exploring the theoretical foundations for reversible concurrent communication systems.

Contribution

It develops a reversible session calculus with memory devices and proposes a session type discipline for static verification of reversible distributed systems.

Findings

Reversible sessions allow undoing previous interactions.

A memory-based reversible calculus is proposed.

Potential for safer, verifiable reversible distributed communication.

Abstract

In this work, we incorporate reversibility into structured communication-based programming, to allow parties of a session to automatically undo, in a rollback fashion, the effect of previously executed interactions. This permits taking different computation paths along the same session, as well as reverting the whole session and starting a new one. Our aim is to define a theoretical basis for examining the interplay in concurrent systems between reversible computation and session-based interaction. We thus enrich a session-based variant of pi-calculus with memory devices, dedicated to keep track of the computation history of sessions in order to reverse it. We discuss our initial investigation concerning the definition of a session type discipline for the proposed reversible calculus, and its practical advantages for static verification of safe composition in communication-centric distributed software performing reversible computations.