はじめに

今回は、昨年のACM PODC (Principle of Distributed Computing)でDijkstra賞を受賞した、以下の発表について解説します。

B. Alpern, F. B.Schneider, "Defining liveness," in proceedings of published in Information Processing Letters, vol. 21, no. 4, pp. 181-185, Oct. 1985.

歴史的背景

1960年代から、ITシステムが徐々にビジネスの重要な業務を肩代わりするようになりました。その当時は、トランザクションを扱うシステムが出始め、日本でも、みどりの窓口で今でも後継が使われているマルスというトランザクション管理システムが生まれた時期です。

システムは大規模化して行き、仕様も複雑になっていきました。「こんな場合(異常系も含めて)に、どう処理するべきか」の"こんな場合"を網羅的にリストアップし、その全ての対応を考えるのは、人間の頭（想像）だけでは限界がありました。しかし、システムがインフラの一部に組み込まれていく中で、「仕様漏れで障害が起きました」は許されるはずがありません。そのため、システムが思い通りに（安全に）動くか、を定量的に知ることは、非常に重要なトピックでした。

そんな中、1977年にLeslie Lamport氏が"Proving the Correctness of Multiprocess Programs"という論文を出し、この中で初めてSafetyとLivenessという用語が誕生します。これ以降、現在でもSafetyとLivenessと言う用語は使われ続けています。

今回紹介する論文は、Livenessを数式的に定義し、さらに正しく動作するシステムが持つあらゆる特徴は、SafetyとLivenessの積集合に含まれることを証明しました。

前提知識

まずは、この論文を読むに当たっての前提知識を説明します。

LivenessとSafety

二つとも、システムやプログラムが持つ特徴(Property)です。これら二つは、Concurrency controlの巨匠、Lamport先生の論文で最初に登場しました。

L. Lamport, "Proving the Correctness of Multiprocess Programs," IEEE Transaction on Software Engineering, vol. SE-3, no. 2, pp. 125-143, Mar. 1977.

それぞれ、以下のように表現されます。

Liveness: 最終的に良いことが起きる
Safety: 悪いことが起きない

ここでいう良いことと悪いこととは、以下のような意味です。

良いこと(Good)：システムやプログラムが、開発者やユーザーが期待した計算を終えること、または期待した状態になること
悪いこと(Bad)：エラーが発生すること、またはエラー状態に陥ったりデッドロックなどにより終了状態以外の状態から抜け出せなくなること

Livenessは、例えばNoSQLでよく言われる結果整合性 (Eventual consistency)が分かりやすいかもしれません。

悪いこと(Bad)の例

具体的に何をGoodとし、Badとするかは、そのプログラムの要件や状況次第としか言えません。例えば、エラーが発生した場合にそれをBadとして良いのですが、必ずしもBadが発生したからといってシステムが救いようのない状態に陥ると断定する必要はありません。 Badなことが起きたあとでも、Goodなことが起きて、システムが正常状態に復帰することはあって良いのです。

以下に一般的な悪いことの例を記載します。

Deadlock: 複数のプロセスが、互いにロックしているリソースの解放を、半永久的に待ち続けてシステムが止まる現象

デッドロックは、複数のプロセスが複数のリソースを同時に利用して処理する状況において発生し得ます。 S2PLのように、順番にロックをとっていく仕組みだと発生し得ます。ちなみに、デッドロックが発生しうる状況は、Coffman conditionと呼ばれます。

Critical section: 複数の処理で共有された単一のリソース

適切なロックの処理を行わずに、複数のプロセスがクリティカルセクションに同時に行われると、データの不整合が発生するなどの破綻がおきます。

内容

論文の内容に入っていきましょう。

この論文のメインポイントの一つは、Livenessの定義を数式的に行なったことです。

ですが、式を見る前に持って頂きたいイメージがあります。それは、プログラムにはたくさんの処理が定義されており、一つの処理が行われると、そのプログラムを動かすシステムの状態が変わっていく、ということです。状態遷移図を知っている人からすると当たり前かもしれません。式を見る上では、状態遷移図を頭に浮かべ、その上でLivenessの定義が、最終的にGoodな状態に到達可能かどうか、を表しているか確認してみてください。

では、式を見ていきましょう。

$\forall \alpha: \alpha \in S^{*}: (\exists \beta: \beta \in S^{\omega}:\alpha\beta\models P)$

式の中に登場する変数の説明は以下の通りです。

- システムの状態の集合
- システムの状態の無限長の列
- この列の要素は、状態の方ではなく、その状態遷移を引き起こした実行(executions)とする
- 世の中のあらゆるプログラムにおけるexecutionは、 $S^{\omega}$ の要素としてモデル化される
- システムの状態の有限長の列
- $S^{\omega}$ と同じく、この列の要素は、その状態を引き起こした(部分)実行 (partial executions)とする
- 実行 $\alpha$ の後に実行 $\beta$ が発生することを意味する
- execution $\alpha\beta$ で到達する状態が特徴 $P$ を持つことを意味する

$\alpha\beta \models P$ から見ていきましょう。これは、「 $\alpha$ が発生した後に、 $\beta$ が発生して到達した状態が、 $P$ という特徴に含まれる」という意味です。

次に、 $\exists \beta: \beta \in S^{\omega}$ を見ていきましょう。これは、「ありとあらゆる状態遷移(つまり $S^{\omega}$ )の中で探したら、○○を満たす $\beta$ がある」という意味です。

では、 $\exists \beta: \beta \in S^{\omega}:\alpha\beta\models P$ を繋げましょう。これは、「ありとあらゆる状態遷移(つまり $S^{\omega}$ )の中には、実行 $\alpha$ が発生した後の状態から、 $P$ という特徴に含まれる状態に到達しうる実行 $\beta$ が少なくとも1つはある」という意味になります。

最後に $\alpha \in S^{*}$ ですが、これはそのプログラムでありえるシステムの状態遷移の中のあらゆる実行 $\alpha$ を指します。

ですので、全部まとめると、「プログラムとしてありえる全ての状態からは、その後 $P$ という特徴を持つ状態に移行するための実行が必ずある」となります。そのため、 $P$ がシステムとして正常な状態とするなら、そこに行き着く過程が必ずある、ということです。よって、この式を満たすプログラム（状態遷移）は、Livenessということです。

おまけ

論文では、他の先行研究で提案されたLivenessの定義についても記載されており、上記の定義がそれと比べて直感的に的を得ていることを説明しています。

あと、すでに提案されているSafetyの定義についても触れられています。

$\forall \sigma: \sigma \in S^{\omega}:$
$\sigma \not\models P \rightarrow (\exists i:0\leq i:(\forall \beta: \beta \in S^{\omega}: \sigma_{i}\beta \not\models P))$

「 $P$ に含まれない状態に陥ってしまったら、どんな遷移が発生しても、もう $P$ に含まれる状態になることはない」という意味ですね。

ここまで感覚がつかめてきたら、他のLivenessの定義も理解できてくると思います。あとは、読者の皆様におまかせします。

余談（おわりに）

以前、会社内で、システムの挙動を状態遷移で設計するか、フローチャートで設計するか、と話題になったことがあります。フローチャートは、正常性の動きの流れを示す、という意味では良く、チームに新しい開発者が参加した際などには役にたつかもしれません。しかし、システムの健全性という観点で言うと、発生する実行や状態の網羅性を捉えることができるという意味では状態遷移ですね。