山火事問題

前回２フェーズコミットを試した後、他の例として出てくるPaxosと、もう一つの問題（本件）がありました。PaxosはPlusCALで書かれていて記述自体はシンプルなものの、アルゴリズム自体が難しい点、pdf上にざっくりと載っているだけで、動くスペックにするのが大変な予感がしたことから、ひとまずこっちを試してみようかと。

こちらの問題は、もとのWebページに「ネット上でこの文字列で検索したときにこのページのみ出てくるようにするため、決してこの文字列をお前のウェブページやその他ネット上に書き込んではならぬ」と、２０年前ならではの俺俺っぷりで「名前を言ってはいけないあの問題」的な状態を作り出していて、今ならGoogle先生に任せろよ、の一言ですが、ランポート先生を怒らせても何もいいことありません。幸い日本人には日本語が使えるため、ここでは山火事問題と呼ぶことにします。

Alphaプロセッサのキャッシュの同期アルゴリズムをTLA+で表したものにバグを入れてあるので、それを探しましょう、というお題です。どうやら１５年経った今も問題としては生きているようで、多分答えをみつけてチューリング賞受賞者にメールすると答え合わせをしてくれるというすごい状況（なはず）。

さて、今日はまだ問題をダウンロードしただけなので、本題にははいれませんが、ひとつ、「ほう」と思った記述を。

Data == [0..(DataLen - 1) -> {0,1}]

DataLenが正の整数だとすると、これは長さがDataLenの任意のバイナリ列を表します。確かに。現実のシステムをTLA+に落とす参考になりますね。実際にこれをモデルチェックかけようとすると、たぶんDataLenをとても小さくしないと計算量が膨大すぎて無理だと思うけど。