チェシャ猫の消滅定理

数学にプログラミング、素敵なもの何もかも。

July Tech Festa 2018 で分散システムの検証について話してきました / #JTF2018

先日行われた July Tech Festa 2018 で、モデル検査を使った分散アルゴリズムの検証について発表してきました。

前半はオートマトンによるシステムの記述と検査の基礎について、後半は三種類のツール SPIN、TLA+、P による記述方法の紹介、といった内容です。

後半のソースコード紹介が散文的な感じになってしまって、いまいちメリットが伝わらない感じだったので、次回があればもっとエモいスライドにしようと思います。

分散アルゴリズムの形式化

定理証明による検証

今回の話の流れとして「分散システムにはモデル検査が有効」と述べていますが、必ずしも定理証明が分散システムの検証に向かないという趣旨ではありません。

例えば、定理証明器 Coq によって分散システムを証明するためのフレームワークとして Verdi が開発されています。

github.com

さらに、Coq は実行可能なコードも出力できるので、Coq で Raft 合意アルゴリズムを証明したものから OCaml を出力して作られた「証明済み分散 KVS」も公開されています。

トランザクションコミットの形式化

今回の発表では、分散アルゴリズムの例として、古典的な二相コミット（を単純化したもの）を使用しました。元ネタになっているのは以下の論文で、発表中取りあげた TLA+ による形式化もこれに基づきます。

www.microsoft.com

アブストラクトを読むとわかる通り、実はこの論文は二相コミットに関するものではありません。「トランザクションコミットに Paxos を使用した」というのが趣旨で、二相コミットは単なる引き立て役です。とはいえ今回の発表と無関係というわけでもなく、Paxos を用いたコミットについても TLA+ コードが載っているので、興味がある人は読んでみると面白いでしょう。

各ツールの簡単な紹介

SPIN

spinroot.com

今回紹介した中では、おそらくもっともメジャーなツールです。日本語の書籍も出ています。

形式化の特徴

記述には Promela と呼ばれる DSL を使用します。C 言語にチャンネルと非決定性を足したような言語ですが、配列以外のデータ構造のサポートがほとんどないため複雑な処理を書こうとすると辛いことがあります。

チャンネルの送受信はそれぞれ ! と ? です。pi 計算にルーツを持つ記号ですが、*1今風に言うなら Go 言語をイメージするとわかりやすいでしょう。

非決定性は if .. fi または do .. od 内のブランチとして記述し、ブランチの先頭の文が実行可能なものの中から非決定的に次の状態が定義されます。例えば

if
:: chan_a ! msg -> ...
:: chan_b ? msg -> ...
fi

と書くと、この if 節全体として chan_a への送信または chan_b からの受信のうちその状態において可能なもの（両方なら非決定的）が選択されます。

ちなみに発表中でも述べましたが、SPIN のチャンネルは完全な FIFO です。もちろんこれはこれで便利なのですが、表現しづらい状況もあって、例えば今回の例で使用した「Transaction Manager から Resource Manager 全体に Commit 命令をブロードキャスト」はとても書きにくい例です。

「ブロードキャスト用のキュー」を用意すると最初の RM が受信した時点でメッセージがキューから消えてしまい他の RM が読めなくなります。「受信できるかどうか確認だけする文」もありますが、これを使うと逆にチャンネル内に残ったメッセージを処理する方法に困ります。さらに、システムが停止したタイミングで中身が残ったチャンネルがあると、SPIN は一種のデッドロックであると考えエラーを報告します。

困った末、今回は各 RM 宛に一つづつチャンネルを用意するという形になりました。

検査の特徴

特定のプロセスの特定の箇所における条件を記述するために assert 文が使えます。通常のプログラム言語と同じように使ってももちろん機能しますが、SPIN の場合はその並列性を生かして「条件を監視するだけのプロセス」を用意しておくという tips が使えます。

byte counter = 0;

proctype Incrementer {
    do
    :: counter = counter + 1;
    od
}

proctype Monitor {
    do
    :: assert(counter < 2)
    od
}

上のシステムの実行パスの中には、例えば次のような実行パスがエラーとして含まれます。

  1. Incrementer が遷移して counter を 0 から 1 へ
  2. もう一度 Incrementer が遷移して counter を 1 から 2 へ
  3. Monitor が遷移して assert 文を踏む

Incrementer と Monitor は実際には積オートマトンとして検査されるため、任意のタイミングの組み合わせについて、つまり Incrementer が n 回続けて遷移した後に Monitor が遷移するパターンはすべて検査されます。要するに「他のプロセスがどんな動き方をしても常に counter < 2」という大域的な条件が検査できるわけです。

また LTL による検査も可能です。この場合は定義の中に直接書き込むのではなく、外部ファイルとして準備して実行時にオプションで与えます。その他、詳しくは以前に開催した勉強会の資料を参照してください。

TLA+

AWS 内で S3 や DynamoDB の検証に採用されたことで有名なツールです。

cacm.acm.org

GUI サポート (TLA Toolbox) が充実している他、マニュアルやチュートリアルの類も公開されているので始めるための敷居は割と低いです。とりあえず雰囲気を掴みたいなら ビデオチュートリアル を眺めてみるのもよいでしょう。"These videos are not light entertainment." という脅し文句が太字で書かれていますが、言うほど難しくはありませんし、スクリプトも付いています。

形式化の特徴

生のままの TLA+ では、システムの初期状態と遷移を直接記述します。スライド中のサンプルよりもっと簡単な例で見たほうが分かりやすいでしょう。

VARIABLE b

Init ==
    /\ b = TRUE

Next == b' = ~b

1 ステップごとに真偽値を反転させるだけのシステムです。b' は b の遷移先での値を表します。検査についてはこの後で述べますが、この Init を初期状態、Next を遷移関係として指定して検査させることになります。

プロセスについては陽には現れません。複数のプロセスが存在する場合、ナイーブにはそれらすべてを状態については /\ で、遷移については \/ でそれぞれ繋いで人間が積オートマトンを書くことになります。例えばこの真偽値反転システムが二つ非同期で動いているとしたら以下のようになります。

VARIABLES b1, b2

Init ==
    /\ b1 = TRUE
    /\ b2 = TRUE

Next ==
    \/ b1' = ~b1
    \/ b2' = ~b2

今回の発表で触れたのはここまでですが、実際にシステムを表現しようとすると、人間が明示的に各ステップを状態遷移に書き換える必要があるため非常に大変です。

この問題を解決するユーティリティとして、TLA+ では +CAL あるいは PlusCal と呼ばれるプログラミング言語チックな DSL も用意していて、ブロックコメント内に +CAL を記述すると、自動的に TLA+ の記法に変換されるようになっています。まずは単純な例から。

--algorithm SingleOscillator {
    variable b = TRUE;
    {
        while (TRUE) {
            b := ~b;
        }
    }
}

ここから生成される TLA+ の仕様は以下のようになります。

VARIABLE b

vars == << b >>

Init == (* Global variables *)
        /\ b = TRUE

Next == b' = ~b

Spec == Init /\ [][Next]_vars

手書きの場合とおおむね同じような出力になりました。最後の Spec は検査に使用する LTL 式ですが、後ほど説明します。

さらに、複数プロセスがある場合の +CAL 記述は次のようになります。

--algorithm MultiOscillator {
    process (oscillator \in {0, 1, 2})
    variable b = TRUE; {
        start:while (TRUE) {
            b := ~b;
        }
    }
}

新しい要素として、ラベル start が導入されました。ラベルはブレイクポイントのように働き、不可分実行される単位を決めます。

生成される TLA+ 仕様は以下です。ハイライトがないとちょっと見づらいですね。

VARIABLE b

vars == << b >>

ProcSet == ({0, 1, 2})

Init == (* Process oscillator *)
        /\ b = [self \in {0, 1, 2} |-> TRUE]

oscillator(self) == b' = [b EXCEPT ![self] = ~b[self]]

Next == (\E self \in {0, 1, 2}: oscillator(self))

Spec == Init /\ [][Next]_vars

先ほどと違うのは、変数 b が単なる TRUE から [self \in {0, 1, 2} |-> TRUE]、すなわちプロセスの識別子を取って TRUE を返す関数に変わっていることです。これに伴って遷移条件 Next もパラメータを導入した形に変わっています。\E は存在量化子なので、遷移の条件は「プロセス 0, 1, 2 のいずれか一つについて遷移 occillator が発生」と読むことができます。

検査の特徴

TLA+ でも、検査すべき性質として常に成立する条件 (Invariant) もしくは LTL による指定 (property) が可能です。

また、システムの遷移として Init と Next をナイーブに与える代わりに、LTL 式を指定することもできます。上で登場している

Spec == Init /\ [][Next]_vars

という記述がそれです。_vars の部分は状態として含める変数の集合を指定しますが、特に意図がない限り VARIABLES に定義したものをすべて入れておけば大丈夫です。

さらに、WF_vars(A) と SF_vars(A) という記法があらかじめ用意されています。前者は論理式 A についての弱い公平性、後者は強い公平性をそれぞれ表現していて、公平性自体を検査対象にしたり、あるいは公平性を仮定して別の性質を検証できます。

P

github.com

Microsoft Research によるツールです。ちなみに同じチームから .NET 用のフレームワーク P# もリリースされています。

実行可能コードが出力できることを売り文句にしていて、MS Research の公式ブログでも SPIN や TLA+ に対して名指しで優位性を主張しています。SPIN はともかく TLA+ の開発者はかの Lamport 先生で、MS Research 所属なんですけども。

www.microsoft.com

形式化の特徴

P による記述は、他の二つのツールより明らかに複雑です。各プロセス（P では machine と呼ばれます）の定義は、state とその state で反応すべき event、反応の内容を列挙する記述が基本になります。

machine Server {
    start state WaitPing {
        on PING goto SendPong;
    }

    state SendPong {
          entry (payload: machine) {
              send payload, PONG;
              raise SUCCESS;
          }
        on SUCCESS goto WaitPing;
    }
}

上記のコードで定義された machine は以下のようなリアクティブな挙動をします。

  • 初期状態は WaitPing
  • PING イベントを受信すると状態 SendPong に遷移
  • payload に格納されたクライアントの PID 宛に PONG イベントを送り返し、かつ自分自身に SUCCESS を発行
  • 状態 WaitPing に遷移して次のイベントを待機

プロセスと独立にチャンネルが存在する SPIN とは異なり、メッセージの受信は 各 machine が所持している自分用の入力キューを介して行われます。送信側にキューはなく、送信したメッセージは即座に相手の入力キューに積まれます。

コード中に state という予約語が出てきますが、紛らわしいことに、この state は実はオートマトンとしての状態とは必ずしも対応しません。というのも、P では「state を push/pop する」という操作があり、実際にオートマトンとしての状態に相当するのは state がスタックされたものになっているからです。新しい state が push されると、スタックの下側にある state に由来するハンドラは上書きされます。次に挙げたのはやや人工的な例です。

machine Server {
    start stat Init {
        entry {
            ...
            raise UNIT;
        }
        on TIMEOUT do {...}
        on UNIT push WaitPing;
    }

    start state WaitPing {
        on PING goto SendPong;
    }
}

このとき、state Init の上に state WaitPing が積まれた状態になり、WaitPing にいる間も Init で定義された TIMEOUT に対するハンドラが継承されます。

なお、イベントに対して処理を定義する以外にも、特定のイベントが発生した際にメッセージをデキューだけして捨てる ignore、およびデキュー自体をブロックする deferred が存在します。

検査の特徴

P では、検査したい条件も他の machine と同様、イベントハンドリングを用いて定義する必要があります。大域的な条件を検査するための記述は、例えば次のようなものです。

spec Safety observes PONG {
    on PONG do (payload: machine) {
        assert (...);
    }
}

上のように spec と observes を定義すると、指定したイベント（ここでは PONG）がシステム全体のどこかで発生したときは常にキャプチャされるようになり、内部に記述した assert 文の成立をチェックすることができます。ちょうど SPIN で「監視専用のプロセス」を定義したのと同じような仕組みです。

残念なことに、P は LTL による検査を直接にはサポートしません。その代わり、state に cold および hot のラベルを付けることが可能になっています。検査の際には、そのシステムの任意の実行パスが

  • cold 状態を無限回通過するかどうか
  • hot 状態を無限回通過しないかどうか

が検査され、この二つを組み合わせることで LTL に相当する検査を行うことができます。

実は、SPIN ではこれに相当するプロセス (never claim) を処理系が生成してくれているのですが、このあたりをきちんと述べるには、スライドにも名前だけ出てきた Büchi オートマトンに関する説明が必要です。長くなりそうなのでまた記事を改めて解説したいと思います。

まとめ

この記事では、July Tech Festa 2018 での発表スライドを補足する形で、SPIN、TLA+、P のそれぞれについて簡単に紹介しました。ただ、ツールの特徴というか、書き心地みたいなものは実際に触ってみないとわからない部分も大きいので、もし今回の発表でモデル検査に興味を持った方はインストールして動かしてみて頂ければ幸いです。

ところで、ここまで説明しておいてなんですが、個人的には本当の初心者にまず薦めたいモデル検査ツールは Alloy なんですよね。近々 Alloy の初心者向けハンズオンを開催しようという腹案も温めていますが、それはまた別の話。

*1:2018/08/01 勘違いだったので撤回