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の数値 となるシーケンスを返す？

OrderedSeqOf(set, n) ==
  { seq \in PT!SeqOf(set, n):
      \A x \in 2..Len(seq):
        seq[x] >= seq[x-1] }

次回

2022.4 実践TLA+もくもく会 - connpass

参考リンク

• Practical TLA+ | SpringerLink
  • 原著
• 実践TLA+ 電子書籍｜翔泳社の本
  • 翻訳
• The TLA+ Home Page
  • TLA+ の総本山的なWebページ