『実践TLA+』を読んだ
ざっくりというならば、モデル検査とは、仕様を（様相）論理式に落とし込んで、その仕様がモデルを満たしているかを検査するための方法論である。TLA+はモデル検査用のツールであり、仕様や実装の正しさを検証することができる。
自分はモデル検査ツールはNuSMVとAlloyを使ったことがあるのだが、TLA+は使ったことがなかった。というのも、使おうとしたことはあるが、論理式はわかるもののGUIの使い方がわからなかったため放置していた。
最近、『実践TLA+』という書籍が出版されたため、TLA+に再挑戦してみることにした。実践TLA+では、GUIの使い方もきちんと説明されているために、すんなりと利用することができたと思う。
TLA+は時相論理という論理をベースにしているのだが、これは一般のプログラマにはとっつきにくい。そこで、TLA+では、手続き型言語に近い記述であるPlusCalを導入していて、比較的書きやすくなっている。実際にいくつかのコードを動かしてみたが、PlusCalから時相論理での記述を自動的に生成してくれるため大変便利である。また、公平性やデッドロックなどの検査も自動で行えるのがよいと感じた。
『実践TLA+』を読んで、全然わからなかったという人は、おそらく、論理式やモデル検査の知識が乏しいか、並行プログラミングの知識が乏しいかのどちらかか、もしくはその両方であると思われる。時相論理を使ったモデル検査の入門としては、『モデル検査 初級編―基礎から実践まで4日で学べる―』でNuSMVをやってみるとよいと思う（この本ではSPINというツールでも説明しているのでそちらでもよい）。これを読めば、時相論理、モデル検査の基本がわかるので、TLA+への足がかりになるはずである。
並行プログラミングがわからない場合は、宣伝になってしまうが、私の書いた『並行プログラミング入門』がよいと思う。たとえば、『並行プログラミング入門』の3.9でパン屋のアルゴリズムが、『実践TLA+』の6.4でデッカーのアルゴリズムがある。これらアルゴリズムはアトミック命令を使わない同期処理方法である。また、『並行プログラミング入門』の6.1.1と『実践TLA+』の6.1.2で、弱い公平性と強い公平性について説明がある。このように、内容が重なる部分が多く、両方を読むとより知識が確かなものになる。『実践TAL+』で得た知見を用いると『並行プログラミング入門』にあるアルゴリズムを検証できるはずなので、挑戦してみるのも面白そうだ。
理論的なところを知りたい場合は、論理学の教科書で様相論理や時相論理を勉強すればよいが、使う分にはそこまでは必要ないだろう。
個人的には、『実践TLA+』の最後の11章で説明している、分散コンピューティングMapReduceでのLivenessなども検証しているのが面白いと感じた。分散処理なプログラミングをしているときに、ノード故障に対応するために、ハートビートを送ったりと小手先のテクニックを駆使しても、いざ故障が発生した場合に全く動かないという事はざらにある。そういう小手先のテクニックを確かにテストできるのは大変有意義に思う。
