Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Checkpoint-based rollback recovery in session programming

Claudio Antares Mezzina, Francesco Tiezzi, Nobuko Yoshida

TL;DR

The paper introduces cherry-pi, a reversible session calculus with explicit commit, rollback, and abort primitives to enable checkpoint-based rollback recovery in communication-centric systems. A decidable, type-level compliance framework ensures that rollbacks cannot undo checkpoints imposed by other participants, guaranteeing rollback safety and progress, and this safety is validated via a MAUDE-based implementation. The authors demonstrate the approach with a video-on-demand example, provide formal semantics and typing rules, and prove key properties including error-freedom, progress, and commit persistency. A MAUDE-based compliance checker and executable type configurations illustrate practical feasibility, while speculative-parallelism scenarios reveal the approach's potential in real-world fault-tolerant and parallel systems.

Abstract

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.

Checkpoint-based rollback recovery in session programming

TL;DR

The paper introduces cherry-pi, a reversible session calculus with explicit commit, rollback, and abort primitives to enable checkpoint-based rollback recovery in communication-centric systems. A decidable, type-level compliance framework ensures that rollbacks cannot undo checkpoints imposed by other participants, guaranteeing rollback safety and progress, and this safety is validated via a MAUDE-based implementation. The authors demonstrate the approach with a video-on-demand example, provide formal semantics and typing rules, and prove key properties including error-freedom, progress, and commit persistency. A MAUDE-based compliance checker and executable type configurations illustrate practical feasibility, while speculative-parallelism scenarios reveal the approach's potential in real-world fault-tolerant and parallel systems.

Abstract

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.
Paper Structure (20 sections, 15 theorems, 24 equations, 15 figures, 1 table)

This paper contains 20 sections, 15 theorems, 24 equations, 15 figures, 1 table.

Table of Contents

  1. Introduction
  2. Linguistic primitives to explicitly program reversible sessions.
  3. Asynchronous commits.
  4. Outline.
  5. A reversible video on demand service example
  6. The $\mathtt{cherry\text{-}pi}$ calculus
  7. Syntax
  8. Semantics
  9. Rollback safety
  10. Session types and typing
  11. Compliance checking
  12. MAUDE implementation.
  13. Properties of $\mathtt{cherry\text{-}pi}$
  14. Useful lemmata
  15. Rollback properties
  16. ...and 5 more sections

Key Result

Theorem 4.2

Let $T_1$ and $T_2$ be two session types, checking if $T_1 \dashV T_2$ holds is decidable.

Figures (15)

  • Figure 1: VOD example: (a) a full description without commit actions; (b,d) runs with undesired rollback; (c) a run with satisfactory rollback.
  • Figure 2: $\mathtt{cherry\text{-}pi}$ syntax.
  • Figure 3: $\mathtt{cherry\text{-}pi}$ runtime syntax (the rest of processes $P$ and expressions $e$ are as in Fig. \ref{['fig:syntax_cherry_pi']}).
  • Figure 4: $\mathtt{cherry\text{-}pi}$ semantics: auxiliary labelled relation.
  • Figure 5: Structural congruence for $\mathtt{cherry\text{-}pi}$
  • ...and 10 more figures

Theorems & Definitions (37)

  • Example 3.1
  • Example 3.2
  • Definition 4.1: Compliance
  • Theorem 4.2
  • proof
  • Definition 4.3: Rollback safety
  • Example 4.4
  • Example 5.1
  • Lemma 6.1: Swap Lemma
  • proof
  • ...and 27 more