MobilityReadingGroup

Reversible Session-Based Pi-Calculus

Francesco TIEZZI, Nobuko YOSHIDA

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 ect of previously executed interactions. This permits to take different computation paths along the same session, as well as to revert 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 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 commitable sessions, where computation can go forward and backward until the session is committed by means of a specific irreversible action.

@article{TY2015,
  author = {Francesco Tiezzi and Nobuko Yoshida},
  title = {{Reversible Session-Based Pi-Calculus}},
  journal = {JLAMP},
  volume = {84},
  issue = {5},
  pages = {684--707},
  publisher = {Elsevier},
  year = 2015
}

@article{TY2015,
  author = {Francesco Tiezzi and Nobuko Yoshida},
  title = {{Reversible Session-Based Pi-Calculus}},
  journal = {Journal of Logical and Algebraic Methods in Programming},
  volume = {84},
  issue = {5},
  pages = {684--707},
  publisher = {Elsevier},
  doi = "10.1016/j.jlamp.2015.03.004",
  year = 2015
}