TLA+ と PlusCal
概要
TLA+ (temporal logic of actions plus; 1999年) と PlusCal (2009年) は共に並行処理と分散システム向けに設計された仕様記述言語 (高レベルモデリング言語)。システム設計やアルゴリズムなどの重要で危険度の高い部分のエラーを定性的に検出することを目的としている。
先に発表された TLA+ は振る舞いの時相理論、つまり有限状態機械 (finite state machine) の状態遷移を観点とした仕様記述向けに設計されている。しかし一般的なプログラミング言語の逐次処理や並行処理の構造を TLA+ で記述すると多くのボイラープレートが必要となる。PlusCal はそのようなボイラープレートを宣言化して省略し、より逐次処理の観点で記述できるようにした DSL である (最終的に TLA+ にトランスパイルされ TLC で検証される)。
このため並行システムの仕様記述を目的とするのであれば PlusCal が向いているが、モデル検証時のトラブルを解消するためには基本的な TLA+ の知識も必要となる (言い換えれば、トランスパイル結果の TLA+ は頻出のボイラープレートばかりであるため PlusCal を主軸に修習していても基本的な TLA+ の作法は覚えられるだろう)。
TLA+ も PlusCal も論文の理論説明に使う擬似コードのような十分に抽象化された設計を記述することを意図している。TLA+ の背後ではシステムを有限状態機械として検証していることから、UML の状態遷移図 (state diagram) と表現の親和性がよく、したがって TLA+ や PlusCal はシステムが想定する状態遷移を検証する道具と考えても良い。一方で、用意されている制御構造は非力でオブジェクト指向や関数型言語といった一般的なパラダイムも持たず (これらを導入すると状態遷移の全数テストがさらに複雑化するためだろう)、現実的で詳細なプログラムフローを記述することは難しい。
TLA+ や PlusCal は設計を抽象化する過程で設計者の主観や感覚の影響を大きく受けやすい。「TLA+ で証明済み」といった主張を盲信せず、どのような前提の下にどのようなケースが適用または省略されたか (省略した部分はどう実装することを想定しているか) を十分にレビューすべきである。
Table of Contents
TLA+
TLA+ はシステムやアルゴリズムを有限状態機械とみなし離散ベントの連続として抽象化する。TLA+ ではある状態から次の状態へのアトミックな変化を一つのステップとし、状態の変化の連続を振る舞い (behaviour) とする。どのような振る舞いが許可されるかは不変式やプロパティ、またはアサーションで検証される。全ての振る舞いとチェックを記述することは仕様化 (specify) である。
TLA+ の難しい点は機能要件をステートマシンに抽象化することと言われている。ステートマシンの振る舞いは 1) 取りうる初期状態と 2) 各状態が取りうる次の状態の 2 点で抽象化することができる (取りうる次の状態が存在しないときシステムは halt する)。TLA+ ではシステムの状態を表すために必要な変数とその初期状態、各変数間の関連と次の状態への遷移を定義することでその仕様を記述する。そして、システムがステップを進行するごとに "正しい状態" の要件を満たしているかをチェックして "正しく動く" ことを検証する。
TLA+入門1: TickTack
このページでは最初の TLA+ の例として、システム状態に 0 と 1 を交互にとる TickTack システムについて考える。
TLA+入門2: 独立した 2 変数のシステム
このページでは TLA+ の例として時相論理演算子を扱う。
翻訳: Summary of TLA+
PlusCal
PlusCal は逐次処理をモデル化することを目的に設計された仕様記述言語である。TLA+ の逐次処理向け DSL と言ったところで TLA+ から多くの構文や演算子を流用している。TLA+ と比較してより現実的なプログラミングに近い記述となっているが、背後では有限状態機械の挙動を探索し検査する点は同じである。
PlusCal の仕様は TLA+ のブロックコメント部分に記述する。PlusCal で記述された仕様は最終的に TLA+ にトランスパイルされて TLC でモデルチェックが行われる。
PlusCal の記述は JUnit のような単体テストフレームワークとよく似ていることから、一般的なプログラミング言語での単体テストに慣れているプログラマであればまず制御構文とアサーションを使った単体テストを作成するつもりで、背後でどのような状態遷移グラフが構築されているかを意識しながら取り掛かるのが近道だろう。その後にケース分岐を考慮して仕様を網羅する方法や、マルチプロセス間の非同期メッセージを検証する方法に進めば良い。
PlusCal入門1: hello, world
このページでは最初の PlusCal の例として hello, world と表示するプログラムをレビューし、その基本的な記述構造について考える。PlusCal での仕様記述や TLC 実行のための環境設定は環境設定と検証の実行を参照。…
PlusCal: データ構造と演算子
PlusCal: 制御構造
このページではいくつかの例を使って PlusCal の基本的な制御構造を説明する。実行環境のセットアップは PlusCal を参照。
PlusCal: 並行システムと非同期処理
このページでは PlusCal を使ってマルチプロセスやマルチスレッド、それらに伴う非同期処理といった並行処理を記述する方法について説明する。サンプルを実行するための環境セットアップは環境設定と検証の実行を参照。…
PlusCal: 証明アプローチ
このページでは PlusCal を使って記述したシステムが正しいことをどのように証明するかについて説明する。サンプルを実行するための環境セットアップは環境設定と検証の実行を参照。
翻訳: A PlusCal User's Manual
翻訳: The PlusCal Algorithm Language
翻訳: PlusCal/TLA+: An Annotated Cheat Sheet
PlusCal と TLA+ のリファレンスとして有用なチートシート。
TLC モデルチェッカーの動作
TLC は TLA+ (PlusCal からトランスパイルされた TLA+ を含む) の仕様記述を検証するプログラムである。スクリプト言語のようにインタープリターとして実行される。
変数定義域×組み合わせケースの自動化
TLC は VARIABLES
で宣言された状態変数の定義域やプロセス進行状況、非決定論的な分岐など、システムが取りうるすべての組み合わせを自動で探索して検証する。
状態変数の定義域をどのように定義するかは TLC 検査のパフォーマンスに大きく影響する。例えば以下の例を実行すると 2G×2G=\(4.6\times 10^{18}\) のケース全てに対して \(x+y \ge 0\) の検証を試みるが、当然ながら計算量の爆発によって今世紀中に TLC 検査が終わることはないだろう。
---- MODULE CombinationalExplosion ----
EXTENDS Integers, TLC
(* --algorithm CombinationalExplosion
variables x \in 0..2147483647;
y \in 0..2147483647;
begin
A: assert x + y >= 0;
end algorithm; *)
====
このような整数型の全値を定義域とするような検査の方法は TLC では現実的ではない。設計をより抽象化して本当に意味のある状態の定義のみとなるよう見直すか (実際 2,147,483,647 個もの状態が個別に意味を持つことは稀である)、全数テストを諦めてコーナーケースといくつかの代表値のみを検査対象とするように修正する必要がある。
状態変数の記憶による実行最適化と停止
TLC はステップごとに状態変数を記録していて、ある過程を終えた後の状態変数が過去に検証済みであればそれ以上の実行を省略する。例えば以下の例では \(x \in \{0,\ldots,99\}\) の定義域で開始するが、ステップ A
を終えた時点で \(x \in \{0,1\}\) の状態に収束することから、ステップ B
以降は \(x=0\) と \(x=1\) の 2 通りの検証が行われれば十分である。
---- MODULE OmitExec ----
EXTENDS Integers, TLC
(* --algorithm OmitExec
variables x \in 0..99
begin
A: x := x % 2;
B: print x;
end algorithm; *)
====
A
が 100 ケース実行されているのに対して、ステップ B
は 2 回しか実行されていないことが分かる。この最適化をうまく使うと状態変数の数や取りうる状態の数を減らして TLC 検証の実行効率を改善することができる。やりすぎは逆効果だが、考慮すべき状態を削減することは設計をよりシンプルにするだろう。
この特性により、実装上は停止条件が存在しない仕様だとしても TLC の検査は停止することができる。実際のこの挙動は PlusCal の while 構文を参照。
状態変数はハッシュ値として記録されており、検証成功時に表示される Fingerprint collision probability とはその状態ハッシュが衝突している確率を示している。
状態変数の記憶によるバックトレース
単純な逐次処理を TLA+ や PlusCal を使って仕様を記述することは Python などの言語で unit-test を記述しているのとそれほど大きく変わることはない。むしろ形式仕様言語で記述できる程度に目的の仕様を過不足なく抽象化する過程が難しい点であって、その検証をどのような手段で行うかはそれほど重要な点ではないという考えもある。
しかし、一般的な言語のテストフレームワークが失敗条件と stack trace 程度しか報告しないのに対して、TLA+ や PlusCal がどのような状態遷移を経て失敗したかを報告するという点は設計者やプログラマにとって明らかに有用な機能の一つだろう。
例として機内食に提供するメニューの仕様について考える。ここでベジタリアンには野菜のみのメニュー、アレルギーを持つ人にはアレルギー食材を除いたメニューを提供しようとしている。この仕様は一見して正しく条件分岐しているように見えるが TLC 検査は失敗する。
---- MODULE InFlightMeal ----
EXTENDS TLC
(* --algorithm InFlightMeal
variables
allergy \in BOOLEAN;
vegetalian \in BOOLEAN;
menu = {}
define
VEGETABLES == {"beans", "carrot", "tomato", "potato"}
MEATS == {"beef", "poke"}
ALLERGIC_INGREDIENTS == {"beans"}
end define;
begin
Select:
if vegetalian then
menu := VEGETABLES;
elsif allergy then
menu := (MEATS \union VEGETABLES) \ ALLERGIC_INGREDIENTS;
else
menu := MEATS \union VEGETABLES;
end if;
Verify:
assert ~vegetalian \/ \A meal \in menu: meal \in VEGETABLES;
assert ~allergy \/ \A meal \in menu: meal \notin ALLERGIC_INGREDIENTS;
assert menu /= {};
end algorithm; *)
====
Fig 2 の Error Trace にはラベル付けされた過程とその状態変数の推移が出力される。この例ではベジタリアンかつアレルギーありのケースでアレルギー食材である "beans" がメニューに含まれてしまっていることが分かる。
デッドロックの検出
TLC はすべてのプロセスが終了していないにもかかわらず進行可能なステップがなくなった状況をデッドロックとする。
環境設定と検証の実行
実際の TLA+, PlusCal を記述する前に、まず Visual Studio Code (vscode) の TLA+ 拡張機能を使用した TLA+ の記述と検証方法について説明する。TLA+ 拡張機能の詳細については公式サイトの Wiki を参照。この拡張機能は PlusCal にも対応している。
vscode 拡張機能のインストール
Visual Studio Code のサイトから vscode をダウンロードしてインストールし、拡張機能のマーケットプレイスから TLA+ の拡張機能を追加する。

仕様記述
vscode 上でプロジェクトを作成して HelloWorld.tla
というファイルに TLA+ または PlusCal で仕様を記述する。ここで MODULE
とファイル名は同じ名前にすることに注意。
---- MODULE HelloWorld ----
EXTENDS TLC
VARIABLES pc
Init == pc = "greeting"
Greeting == /\ pc = "greeting"
/\ PrintT("hello, world")
/\ pc' = "finish"
Termination == /\ pc = "finish"
/\ UNCHANGED pc
Next == Greeting \/ Termination
====
---- MODULE HelloWorld ----
EXTENDS TLC
(* --algorithm HelloWorld
begin
Greeting:
print "hello, world";
end algorithm; *)
====
トランスパイル
PlusCal で記述した場合は [View]-[Command Palette...] メニューか CTRL+Shift+P を押して "TLA+: Parse module" を選択すると Example 5 のような TLA+ のコードにトランスパイルされる。同時にモデルファイルの HelloWorld.cfg
も生成され、翻訳前の内容は HelloWorld.old
に保存されてる。
TLC 検証
次に EXPLORER ペインで HelloWorld.tla
ファイルを右クリックして "Check model with TLC" を選択すと TLC によるモデルチェックが実行されて結果が表示される (Fig 6)。
ここで TLA+ の例でまだモデル HelloWorld.cfg
が存在しない場合は Fig 7 のように誘導される。モデルファイルでは HelloWorld モジュールで使用する定数やデッドロック時の挙動などを指定できるが、ひとまずこの例では INIT
(取りうる初期状態) と NEXT
(各状態が取りうる次の状態) の定義とのマッピングのみを指定する。
TLC は TLA+ で記述された仕様に対して状態モデルのチェックを行うプログラムである (TLC は Java で実装されているためコマンドラインから Java を起動できるようにしておく必要があるかもしれない)。結果 Status 右上の "Full output" をクリックすると以下のような TLC 出力の詳細が表示される。
ここでは Success と表示されていることから HelloWorld システムが取りうる全ての状態で仕様を満たしていることがわかる。ただしこの hello, world の例は意味のある状態変数もアサーションも持たないため TLC での実行は単に hello, world を逐次実行したのと変わらない。PlusCal や TLA+ の一般的な記述では仕様の最後または処理の途中でアサーションを記述し、システムの状態変数が正しいことを検証する。
LaTeX 出力
TLA+ で記述した場合は [View]-[Command Palette...] メニューまたは CTRL+Shift+P ショートカットを使って LaTeX または PDF に出力することができる。PDF 化には latex
コマンドを求められるが、ローカルに LaTeX をインストールしていない場合は overleaf などのサイトにファイルの内容をコピーして生成することもできる。
コマンドライン実行
vscode ディレクトリの tla2tools.jar
を使って java コマンドから直接 TLC を起動することができる。最新版では簡易的な REPL も用意されているようなので将来的に使えるようになるかもしれない。
参照
- Leslie Lamport (2002), Specifying Systems.
- Leslie Lamport (2020), A PlusCal User’s Manual P-Syntax Version 1.8.
- LEARN TLA+