TLA+ / PlusCal

Leslie Lamport による形式仕様記述言語。並行・分散システムの設計を時相論理で記述し、モデル検査器で網羅的に状態空間を探索して不変条件・活性を検証する。Hillel Wayne 『実践TLA+』を通して学習した。

モデル検査の基本

• Init/アクションの全状態に対して不変条件(例: NoOverdrafts 残高が負にならない)が保たれるかを網羅検証する。
• ラベルが原子性の粒度を決め、ラベル内処理は1ステップ(アクション)で実行される。pc(プログラムカウンタ)が現在のラベルを指す。
• 並行プロセスは reader-writer パターンなどで記述し、await で条件成立を待ち、either/with で非決定性を表現する。デッドロックも検出できる。

時相特性(活性)

• []P(常に)、<>P(最終的に)、P ~> Q(P が成り立てばいずれ Q)、<>[]P(最終的には常に)。
• 公平性: fair(弱い公平性)/fair+(強い公平性)を付けないとスタッタリング(何もしない)で停止性が破れる。Dekker のアルゴリズムでライブロックを観察する例も。

PlusCal の道具立て

• 集合内包(filter/map)、タプル <<...>>、構造体 [a |-> 1]、関数 [x \in S |-> expr]、CHOOSE(宣言的に連立方程式や最大値を解く)、LET-IN、プロシージャ。
• 状態機械、ゴーストデータ、TypeInvariant パターンで図書館システムや MapReduce、Two-Phase Commit をモデル化する。

定理証明系 とは異なり「網羅的テスト」に近い立ち位置で、設計の曖昧さを早期に炙り出す。関連: distributed-consensus-raft / database-transaction-theory / _moc-book-notes