りりろじさんの「よくわかる（かもしれない）トークン問題」を Spin にやってもらいました

gistfile1.md

説明はあとで（適当に）します。 このファイルを protocol.pml という名前で保存して、次の手順を踏みます：

> spin -a protocol.pml
> gcc pan.c
> ./a.out
> spin -M -t protocol.pml

以上で protocol.pml.ps という PostScript ファイルができあがります。

gistfile2.md

説明

Spin http://spinroot.com/ というモデル検査ツールでプロトコル検証をしています。 りりろじさんの説明でもう十分にわかっていることですが、クライアントが持っているトークンは古くなってサーバに拒絶される可能性があります。 サーバとクライアントの振る舞いを人間が書いて Spin がシミュレートすると、やばい状態に陥っていることが絵で示されます。

シミュレートの結果 protocol.jpg から説明します。 縦に 3 本のラインが走っていますが、左から順に

• Server
• ClientFlash
• ClientJava

が非同期で動いています。

ClientFlash は Server に今持っているトークンが有効かどうか？を確認しています（submit & judge）。 最初のトライは成功しています（judge が 1）。 しかし、二度目のトライは失敗します：その前に ClientJS が Server からトークンの更新を受け取っています（update & renew）。 ClientJS はその後 ClientFlash に新規トークンを通知しているのですが（notice）、あいにく ClientFlash はそれと知らずにもう一度トライし、失敗（judge が 0）になって assertion failed でシミュレート終了です。

TCP の処理などをきちんと書かないと実際のモデルをシミュレートしたことにはなりませんが、このような抽象モデルとシミュレーションによって問題の原因がはっきりする場合があります。

最後にシミュレート本体 protocol.pml の説明をして終わります。 Spin では Promela 言語によってプロセスと通信を記述します。 プロセスは Server, ClientFlash, ClientJS の 3 つです。通信路は

• submit ... ClientFlash -> Server : トークンの新旧判定の要求
• judge ... Server -> ClientFlash : トークンの新旧判定
• update ... ClientJS -> Server : トークン更新の要求
• notice ... ClientJS -> ClientFlash : 新規トークンの通知
• renew ... Server -> ClientJS : トークン更新

の 5 つです。説明の順番とソースコードの記述順が一致しませんけど… まあ読み替えてください。

mtype は Promela 固有のデータ型の宣言で、他言語でいう enum のことです。

各プロセスは無限ループ（do から od）の中で通信をやりとりしています。

通信は ! が送信、? が受信です。Promela 言語ではインデントは意味を持ちません。人間の都合で字下げしています。

りりろじさんの説明では、ClientJS は Server に旧トークンを送って新トークンをもらっているんですけど、このモデルではなにがあろうと常にトークンを更新しています。 現実に即そうと思えばトークンの生き死にみたいな管理をしなきゃいけないんですが、そういうことをすると状態が爆発しかねないのでここでは抽象化しました。

まとめ

プロセスが複数非同期に走っていて通信のあれやこれやをする状況でまずいアレは避けたいです。 で、まずいアレが起きるんじゃ！ということを説明したいですがシミュレートは面倒ですね… Spin と Promela 言語はシミュレートの土台をあらかじめ用意してくれるので、人間は各プロセスの記述に焦点をあてて作業することができます。

今回の例ではシミュレートするだけで assertion failed がでる例でしたが、Spin には他の種類のシミュレートもできるので気になる人は調べてみてはいかがでしょうか。以下、本家 http://spinroot.com/spin/what.html から抜粋：

• マルチスレッドの検査
• C 言語ソースコードの検査
• 検査をマルチコアでやる
• 検査の背景の隠蔽（Kripke 構造とかなんとかをユーザの目から隠して書かなくてもよいようにする）
• 時相論理式 LTL を用いた検査（将来やばいアレが起きちゃダメ、みたいなことを検査）
• かしこい（以下省略、本家参照）

ぼくが Promela のことを覚えていないというのもあり、こんな簡単なモデルを書くのに３時間くらいかけてしまいましたが（この説明にはもっと時間を費やして書いてる）、こういう目的のためには軽量なツールだと思います。

protocol.jpg

protocol.pml

mtype = { INITIAL_TOKEN, NEXT_TOKEN };

chan judge = [1] of { bool };
chan update = [1] of { mtype };
chan notice = [1] of { mtype };
chan submit = [1] of { mtype };
chan renew = [1] of { mtype };

active proctype Server () {
  mtype current_token = INITIAL_TOKEN;
  mtype token;

  do
    :: submit ? token ->
       if 
         :: (token == current_token) ->
            judge ! true;
         :: else ->
            judge ! false;
       fi
    :: update ? token ->
         current_token = NEXT_TOKEN;
         renew ! current_token;
  od
}

active proctype ClientFlash () {
  mtype current_token = INITIAL_TOKEN;
  mtype token;
  bool q;

  do
    :: submit ! current_token ->
         judge ? q ->
           if
           :: (q) -> skip;
           :: else -> assert(false);
           fi
    :: notice ? token ->
         current_token = token;
  od
}

active proctype ClientJS () {
  mtype current_token = INITIAL_TOKEN;
  mtype token;

  do
    :: update ! current_token ->
         renew ? token ->
           current_token = token;
           notice ! current_token;
  od
}