Reversible Session-Based Pi-Calculus
File(s)1-s2.0-S2352220815000346-main.pdf (979.94 KB)
Published Version
Author(s)
Tiezzi, F
Yoshida, N
Type
Journal Article
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 to take different computation paths along the same session, as well as to revert the whole session and start 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 propose ReSπ a session-based variant of π-calculus using memory devices to keep track of the computation history of sessions in order to reverse it. We show how a session type discipline of π-calculus is extended to ReSπ, and illustrate its practical advantages for static verification of safe composition in communication-centric distributed software performing reversible computations. We also show how a fully reversible characterisation of the calculus extends to committable sessions, where computation can go forward and backward until the session is committed by means of a specific irreversible action.
Editor(s)
De Nicola, R
Date Issued
2015-04-15
Date Acceptance
2015-03-31
Citation
Journal of Logical and Algebraic Methods in Programming, 2015, 84 (5), pp.684-707
ISSN
2352-2208
Publisher
Elsevier
Start Page
684
End Page
707
Journal / Book Title
Journal of Logical and Algebraic Methods in Programming
Volume
84
Issue
5
Copyright Statement
© 2015 The Authors. Published by Elsevier Inc. This is an open access article under the CC
BY license (http://creativecommons.org/licenses/by/4.0/).
BY license (http://creativecommons.org/licenses/by/4.0/).
License URL
Publication Status
Published