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;
2015-01-01

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 in questo prodotto:
File Dimensione Formato  
TiezziYoshida15.pdf

accesso aperto

Tipologia: Versione Editoriale
Licenza: PUBBLICO - Creative Commons
Dimensione 651.04 kB
Formato Adobe PDF
651.04 kB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11581/390635
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 22
  • ???jsp.display-item.citation.isi??? 17
social impact