Rollback Recovery in Session-based Programming

Submitted Manuscript 
Maude sources


To react to unforeseen circumstances or amend abnormal situations (e.g., runtime errors) 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. We prove that rollbacks in our language always bring the system to previous visited states and that 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 using MAUDE. We show that the language satisfies error-freedom and progress of a session, demonstrate the practical effectiveness of the proposed approach by a means of a speculative execution scenario from the reversibility literature, and illustrate how the approach applies to both binary and multiparty sessions.