TLA+に再挑戦(2022.3)
英語のドキュメント を読んだけどあまり理解できてなかったので 日本語 で再挑戦する会。
今回
- 「6章 時相論理」を読んだり試したり
- 「7章 アルゴリズム」を読んでいちゃもん書いたり
第6章 時相論理 例 「デッカーのアルゴリズム」
最初: お試し
- 全てのスレッドのフラグが
FALSE
になるのを待つ、だと Deadlock するP2
で待っている間に、他のスレッドがP1
へ進入する(TRUE
になる)と、先へ進めなくなる
次: Deadlock を解消し、全てのスレッドが同時にクリティカルセクションへ進入しないことを保証する
いわゆる安全性検査をする。
P2
で、self 以外にTRUE
のスレッドがいる間、「self をFALSE
にする、self をTRUE
にする」を繰り返す- 運が良ければ self を
FALSE
にした次の時点で他のスレッドが先に進めるようになる
次: 全てのスレッドが確実にクリティカルセクションへ進入できることを保証する
今度は活性検査をする。
- 不変条件
Liveness == \A t \in Threads: <>(pc[t] = "CS")
を追加する<>
は「最終的に」を意味する演算子- 時相論理を含むので、 invariants ではなく properties へ追加する
- この時点では失敗する
- 例えば次のような系列は state=9 から state=2 へループしてしまうからダメらしい
- 全ての系列で、「全てのスレッドが確実にクリティカルセクションへ進入できること」を保証したいのに、そうならない系列があるからということだと思う
* state=1 - flag: `<<FALSE, FALSE>>` - pc: `<<"P1", "P1">>` * state=2 - flag: `<<TRUE, FALSE>>` - pc: `<<"P2", "P1">>` * state=3 - flag: `<<TRUE, TRUE>>` - pc: `<<"P2", "P2">>` * state=4 - flag: `<<TRUE, TRUE>>` - pc: `<<"P2_1", "P2">>` * state=5 - flag: `<<FALSE, TRUE>>` - pc: `<<"P2_2", "P2">>` * state=6 - flag: `<<FALSE, TRUE>>` - pc: `<<"P2_2", "CS">>` * state=7 - flag: `<<FALSE, TRUE>>` - pc: `<<"P2_2", "P3">>` * state=8 - flag: `<<FALSE, FALSE>>` - pc: `<<"P2_2", "P4">>` * state=9 - flag: `<<TRUE, FALSE>>` - pc: `<<"P2", "P4">>`
次: デッカーのアルゴリズムを活性検査する
実はここまでの例はただのナイーブな実装だった。
- セマフォを使わず、共有メモリだけでCSに進入できるスレッドを限定する
- 共有メモリにはCSに進入できるスレッドが排他的に設定される
- CSへ進入する前、自分の順番が来るまで繰り返し共有メモリをチェックする
- CSから退出した後、自分以外のスレッドを共有メモリに設定する
- スレッド数が2の場合しか検査を通過できない
- 3以上になるとリソーススタベーションが発生する
- うまく一般化するのは難しい
次: デッカーのアルゴリズムの回復力を確認する
- 2つのスレッドのうち、片方を
fair process
、もう一方をprocess
にする- 公平なプロセスはスタッタリングする
- (勝手な解釈)必ずpcを進めようとする
- そうでないプロセスはスタッタリングしない
- (勝手な解釈)pcを進めない
- 公平なプロセスはスタッタリングする
- 公平でないプロセスが
P2_1_1
で止まると、プロセスがクラッシュして存在しなくなったかのような状態になる - 公平なプロセスは無限に
P2
でスタッタリングする
第7章 アルゴリズム
シングルプロセスアルゴリズムの仕様
- ほとんど決まりきった形式になる
- 例えば
add
というアルゴリズム- 入力 a の値域は -5 以上 5 以下の整数
- 入力 b の値域は -5 以上 5 以下の整数
- 入力 a, b に対する期待結果は
a + b
- アルゴリズムと期待結果を同じ実装で求めているのはよくない
---- MODULE add ---- EXTENDS Integers, TLC Expected(a, b) == a + b (*--algorithm add variables in a \in -5..5, in b \in -5..5, output; begin output := in a + in b; assert output = Expected(in a, in b); end algorithm; *)
- 集合から最大値を求めるイディオム
CHOOSE x \in set: \A y \in set: y <= x
Int
は整数の無限集合だけど、TLCは無限を処理できない- 「定義のオーバーライド」という機能がある
Int = 1..5
みたいにできる
- モデルの設定
Definition Override
に記述する - 仕様を十分に検査できる定義へ書き換えるとよい
- 「定義のオーバーライド」という機能がある
leftpad
- 入力
- 文字c
- 長さn
- 文字列s
- 出力
- 長さnの文字列
- 文字列sの長さがnより小さいなら、sの前に不足分のcを補う
------------------------------ MODULE leftpad ------------------------------ EXTENDS Integers, Sequences, TLC PT == INSTANCE PT Leftpad(c, n, s) == IF n < 0 THEN s ELSE LET outputLength == PT!Max(Len(s), n) paddingLength == CHOOSE length \in 0..n: length + Len(s) = outputLength IN [x \in 1..paddingLength |-> c] \o s CharSet == {"a", "b", "c"} (*--algorithm leftpad variables in_c \in CharSet \union {" "}, in_n \in -1..6, in_s \in PT!SeqOf(CharSet, 6), output; begin output := in_s; while Len(output) < in_n do output := <<in_c>> \o output; end while; assert output = Leftpad(in_c, in_n, in_s); end algorithm; *)
アルゴリズムの特性
- 「順序を持つ全数列の集合とはこうです」と、いきなりこういう式を出してくるところはよくないと思う
- 引数
set
整数のセットn
出力する数列の長さ
- 定義
- PT!SeqOf(set, n)
- 整数のセットの要素より、長さが n になる全組み合わせのシーケンスを返す?
\A x \in 2..Len(seq): seq[x] >= seq[x-1]
位置x-1の数値<=位置xの数値
となるシーケンスを返す?
- PT!SeqOf(set, n)
- 引数
OrderedSeqOf(set, n) == { seq \in PT!SeqOf(set, n): \A x \in 2..Len(seq): seq[x] >= seq[x-1] }
次回
参考リンク
- Practical TLA+ | SpringerLink
- 原著
- 実践TLA+ 電子書籍|翔泳社の本
- 翻訳
- The TLA+ Home Page
- TLA+ の総本山的なWebページ