MobilityReadingGroup

π-calculus, Session Types research at the University of Oxford

Rollback Recovery in Session Based Programming
Claudio ANTARES MEZZINA , Francesco TIEZZI , Nobuko YOSHIDA
25th International Conference on Coordination Models and Languages (COORDINATION). p. 195 - 213

To react to unforeseen circumstances or amend abnormal situations in communication-centric systems, programmers are in charge of “undoing” the interactions which led to an undesired state. To assist this task, session-based lan- guages can be endowed with reversibility mechanisms. In this paper we propose a language enriched with programming facilities to commit session interactions, to roll back the computation to a previous commit point, and to abort the session. Rollbacks in our language always bring the system to previous visited states and a rollback cannot bring the system back to a point prior to the last commit. Pro- grammers are relieved from the burden of ensuring that a rollback never restores a checkpoint imposed by a session participant different from the rollback requester. Such undesired situations are prevented at design-time (statically) by relying on a decidable compliance check at the type level, implemented in MAUDE. We show that the language satisfies error-freedom and progress of a session.

This paper received the best paper award at Coordination 2023.

@inproceedings{MTY2023,
  author = {Claudio Antares Mezzina and Francesco Tiezzi and Nobuko Yoshida},
  title = {{Rollback Recovery in Session Based Programming}},
  booktitle = {25th International Conference on Coordination Models and Languages},
  pages = {195--213},
  publisher = {Springer},
  year = 2023
}
@inproceedings{MTY2023,
  author = {Claudio Antares Mezzina and Francesco Tiezzi and Nobuko Yoshida},
  title = {{Rollback Recovery in Session Based Programming}},
  booktitle = {25th International Conference on Coordination Models and Languages},
  pages = {195--213},
  publisher = {Springer},
  doi = "10.1007/978-3-031-35361-1_11",
  year = 2023
}