Claudio Antares Mezzina ; Francesco Tiezzi ; Nobuko Yoshida - Checkpoint-based rollback recovery in session programming

lmcs:12654 - Logical Methods in Computer Science, January 10, 2025, Volume 21, Issue 1 - https://doi.org/10.46298/lmcs-21(1:2)2025
Checkpoint-based rollback recovery in session programmingArticle

Authors: Claudio Antares Mezzina ; Francesco Tiezzi ; Nobuko Yoshida

    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 languages 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. Programmers 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.


    Volume: Volume 21, Issue 1
    Published on: January 10, 2025
    Accepted on: November 25, 2024
    Submitted on: December 6, 2023
    Keywords: Computer Science - Programming Languages,Computer Science - Logic in Computer Science

    Consultation statistics

    This page has been seen 123 times.
    This article's PDF has been downloaded 58 times.