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 ReSpi a session-based variant of pi-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 pi-calculus is extended to ReSpi, 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.
Reversible session-based pi-calculus / TIEZZI, Francesco; Yoshida, Nobuko. - In: THE JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING. - ISSN 2352-2216. - STAMPA. - 84:(2015), pp. 684-707. [10.1016/j.jlamp.2015.03.004]
Reversible session-based pi-calculus
TIEZZI, Francesco;
2015
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 ReSpi a session-based variant of pi-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 pi-calculus is extended to ReSpi, 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.File | Dimensione | Formato | |
---|---|---|---|
TiezziYoshida15.pdf
Accesso chiuso
Dimensione
651.04 kB
Formato
Adobe PDF
|
651.04 kB | Adobe PDF | Richiedi una copia |
I documenti in FLORE sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.