TLA+
TLA+ はプログラムやシステムをモデル化するための言語。
特に並列システムや分散システムに対して用いられる。
プログラムの仕様を数学的な表記を用いて書き下し、その仕様の持つ性質を検査することができる。
→ モデル検査
TLA+ は産業界の事例が豊富
AWS が DynamoDB や S3 のデバッグに利用
Elastic が Elasticsearch の cluster coordination などの検査に利用
学習リソース
TLA+ Video Course https://lamport.azurewebsites.net/video/videos.html
かなり良い
入門するならこれ
Specifying Systems https://lamport.azurewebsites.net/tla/book.html?back-link=learning.html#book
PDF をダウンロードできる
初手でこの本を読むのはおすすめしない
TLA+ そのものに関しては詳しく説明されているが、TLA+ の処理系の使い方が全く書いてないので、自分で試してみることがほぼ無理
TLA+ Toolbox
TLA+ の IDE
必要なものが一式そろっているので便利
https://lamport.azurewebsites.net/tla/toolbox.html
他の選択肢としては VSCode に TLA+ の拡張があるが、世の中の学習リソースが基本的に TLA+ Toolbox 前提になっているため、最初は TLA+ Toolbox からはじめるのがよさそう
モデルはステートマシンを論理式を用いて書き下すような雰囲気で記述する
同じモデル検査のための言語である Spin はプログラミング言語のような見た目だったが、TLA+ は全く異なる
Lamport 先生曰く、この目的に対しては論理式を書き下す記法のほうが優れているらしい
ステートマシンに対して成り立つべき性質を普通の論理式や線形時相論理の式で表現し、検証することができる。
サンプルコード
code:Counter.tla
------------------------------ MODULE Counter ------------------------------
(* 複数のプロセスがグローバルなカウンタをインクリメントする状況をモデル化。
* このときロストアップデートが発生することを検出してみる。
*)
EXTENDS Integers, FiniteSets
(* プロセスの集合 *)
CONSTANT procs
(* 各プロセスの実行ステップ ("read", "write", "done") *)
VARIABLE pc
(* 各プロセスのメモリ *)
VARIABLE memory
(* カウンター (global) *)
VARIABLE count
Init ==
/\ pc = p \in procs |-> "read"
/\ memory = p \in procs |-> 0
/\ count = 0
(* カウンタの値をプロセスのメモリに読み込む *)
ReadStep(p) ==
/\ pcp = "read"
/\ memory' = [ memory EXCEPT !p = count ]
/\ pc' = [ pc EXCEPT !p = "write" ]
/\ UNCHANGED << count >>
(* メモリの値 + 1 をグローバルなカウンタに書き込む *)
WriteStep(p) ==
/\ pcp = "write"
/\ count' = memoryp + 1
/\ pc' = [ pc EXCEPT !p = "done" ]
/\ UNCHANGED << memory >>
(* 何もしない *)
DoNothing(p) ==
/\ pcp = "done"
/\ UNCHANGED << pc, memory, count >>
(* カウンタを非アトミックにインクリメントする *)
Increment(p) ==
\/ ReadStep(p)
\/ WriteStep(p)
\/ DoNothing(p)
Next ==
\E p \in procs : Increment(p)
-----------------------------------------------------------------------------
AllProcessIsDone ==
\A p \in procs : pcp = "done"
(* 事後条件: 全てのプロセスが終了しているとき、カウンタの値はプロセスの数に等しい *)
PostCondition ==
AllProcessIsDone => count = Cardinality(procs)
=============================================================================
code:Counter.cfg
\* SPECIFICATION
\* Uncomment the previous line and provide the specification name if it's declared
\* in the specification file. Comment INIT / NEXT parameters if you use SPECIFICATION.
CONSTANTS
procs = {1, 2}
INIT Init
NEXT Next
\* PROPERTY
\* Uncomment the previous line and add property names
INVARIANT PostCondition