チェックポイントと中断のある実行

保存域は、各時点で $S \cup \{\bot\}$ の元 $c$ を 1 つ保持する（$\bot$ は「まだ何も保存されていない」ことを表す）。実行中のプロセスはメモリ上に状態 $m \in S$ をもち、次の操作を行う。

• 開始・再開: $c \ne \bot$ なら $m \leftarrow c$、$c = \bot$ なら $m \leftarrow s_0$ とする。
• ステップ: $m \notin D$ のとき $m \leftarrow T(m)$ とする。
• 保存（チェックポイント）: $c \leftarrow m$ とする。いつ保存するかは任意である。
• 中断: メモリ上の $m$ が失われる。その後、再開から続ける。中断はどの時点でも（ステップや保存の途中でも）起こりうる。

$m \in D$ になったら、$m$ を結果として返して終わる。次の 2 つの性質を考える。

• 完全性: 保存されるのは状態 $m$ の全体で、再開で読み戻される値は保存された $m$ そのものである。
• 原子性: 保存の途中で中断が起きても、その後の保存域の値は、保存の前の値か、保存しようとした $m$ のどちらかである。