Towards Reversible Sessions

Francesco Tiezzi
(IMT Institute for Advanced Studies, Lucca, Italy)
Nobuko Yoshida
(Imperial College, London, U.K.)

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.

In Alastair F. Donaldson and Vasco T. Vasconcelos: Proceedings 7th Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software (PLACES 2014), Grenoble, France, 12 April 2014, Electronic Proceedings in Theoretical Computer Science 155, pp. 17–24.
Published: 12th June 2014.

ArXived at: https://dx.doi.org/10.4204/EPTCS.155.3 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org