マルチスレッド
CSP
SyncStitch
排他制御
モデル検査


排他制御をするときにチェックする2つのポイント

排他制御をするときにチェックすべきポイントは2つあります.


  1. 2つ以上のプロセスが同時にクリティカルセクションに入らないこと(安全性 safety)

  2. プロセスがロックを要求したら,いつかはロックが獲れること(活性 liveness)


ミューテックスの公平性

ミューテックスを用意して lock/unlock を正しく配置すれば安全性は保証されます.

しかし活性を保証してくれるとは限りません.たとえば POSIX の pthread_mutex_lock/unlock を見ると,複数のスレッドがミューテックスを待っているとき,次に獲得するスレッドはスケジューリングポリシーで決まるとあり,スケジューリングポリシーの項を見ると SCHED_FIFO のようなものがありますが optional であると書いてあります.つまり,実装によってはロックを要求しても永久にもらえない可能性があります.

これはいわゆる公平性の問題です.実際に問題になるかどうかは対象によるでしょうけれど,時間的な制約も加わって対処が必要ということはあるかもしれません.


モデル検査での問題

排他制御が正しくできているかどうかをモデル検査で調べる場合にも公平性は問題になります.物理的な世界で実装されるシステムではありえないようなケースについても,モデル検査は反例として見つけてしまうからです.

実際に例を見てみます.


ミューテックスのモデル

N 個のプロセスがそれぞれ自分の仕事をしているとします.1つ共有資源があって,これを使うときだけミューテックスで排他制御します.


定数とプロセスID型

定数 N と,プロセスIDの型 I を定義します.ID は整数です.

(def N 3)

(deftypename I (int 0 N))


ミューテックスのインターフェイス

ミューテックスのインターフェイスをチャネルとして定義します.ロックを要求するチャネルを (lock i) とします.獲得できると (ret i) を返してくれるものとします.システムコールっぽくしているわけです.アンロックは (unlock i) とします.こちらは応答を必要としないので,同期が発生した瞬間アンロックされると考えます.

(defch lock I)

(defch ret I)
(defch unlock I)


プロセスの仕事開始・終了を表すイベント

各プロセスが共有資源を使うアクションを表すイベント (a i), (b i) を定義します.(a i) が使用開始,(b i) が終了を表します.瞬間的に発生するイベントを2つ使って時間的区間を表します.

(defch a I)

(defch b I)


仕事をするプロセスの定義

仕事をするプロセスは次のようになります.ロックを要求 (lock i) し,獲得 (ret i) できたら仕事を開始 (a i),終了 (b i) したらアンロックする (unlock i),これを繰り返します.

(def (P (i I))

(! (lock i) (ret i) (a i) (b i) (unlock i) (P i)))


ミューテックスプロセス

次はミューテックスです.ミューテックスも1つの(理論的)プロセスと考えます.オペレーティングシステムのカーネルと考えてもいいかもしれません.

ミューテックスの状態は,いずれかのプロセス i に所有されている (Locked i) か,または誰も所有していない Unlocked かのいずれかです.これを代数的データ型 t で表します.

(deftype t Unlocked (Locked I))

ミューテックスを定義します.変数 s はミューテックスを待っているプロセス ID の集合です.

(def (M (m t) (s (set I)))

(alt
(? lock (i)
(M m (adjoin s i)))
(? unlock (i)
(= m (Locked i))
(M Unlocked s))
(if (and (= m Unlocked)
(not (empty? s)))
(xamb i s
(! (ret i)
(M (Locked i) (remove s i))))
STOP)))


  1. ロックの要求 (lock i) が来たら,待ち集合 s に加える.

  2. アンロックの要求 (unlock i) が来たら,所有者であることを確認したのち,ミューテックスの状態を Unlocked に変える.

  3. もしミューテックスの状態が Unlocked で,かつ待っているプロセスがいる場合,その中から非決定的に(無作為に)1つ選んで与える.

実現の詳細を隠蔽し変数の初期値を設定するプロセスも定義しておきます.

(def MUTEX (M Unlocked (set)))


システムの定義(並行合成)

仕事をするプロセスとミューテックスを合成して,システム全体を定義します.まず直接には相互作用のない N 個のプロセスを合成し,それから合成系とミューテックスを合成します.プロセスの合成系とミューテックスの間では lock ret unlock の通信が行われるので,これを指定します.

(def SYSTEM

(par (chset lock ret unlock)
(xpar i I (set) (P i))
MUTEX))


シミュレーション

モデルができたのでシミュレーションしてみます.一番上のパスはプロセス0がロックを獲得して仕事をし,アンロックして初期状態に戻るシナリオです.

下はプロセス0とプロセス2がロックを要求し,非決定的な選択の結果いずれかが獲得する,というシナリオです.

m3.png

次は競合の例です.プロセス0がロック中にプロセス1がロックを要求をしていますが,ロックは与えられません.(ret 1) による遷移がないことからわかります.

m4.png


安全性の検査

目視によるシミュレーションでだいたいうまくいっているようなので,網羅的な検査をしてみます.まずは安全性です.2つのプロセスが同時に共有資源を使うことはない,ということを検査します.

プロセス i が共有資源を使っているという状態は,イベント (a i) の発生からイベント (b i) の発生までの時間的区間として表すことができます.これを fluent を使って命題にします.fluent (p i) は (a i) が発生すると true になり,(b i) が発生すると false になります.

(fluent (p (i I)) (set (a i)) (set (b i)) false)

対称性があるので (p 0) と (p 1) が同時に成り立つことがないことを確認すれば十分でしょう.

(check (LTL SYSTEM (F (and (p 0) (p 1)))))

検査を実行すると,確かにそのようなパスは存在しないことがわかります.

余談ですが,検査が成功しても,実は検査式が間違っているのではないかと不安を感じるときがあります.そういうときは故意にモデルを壊して(mutation)検査で反例が出ることを確認します.テストを失敗させるのと同じ考え方です.

たとえばプロセスがロックをしないようにすれば確かに反例が出ます.

(def (P (i I)) (! (a i) (b i) (P i)))

m5.png


活性の検査

いよいよ活性の検査をします.活性のイディオムは $\mathsf{GF}\phi$ で,「$\phi$ は無限に何度も(infinitely often)成り立つ」という論理式です.いいかえれば,「『あるとき以降 $\phi$ は成り立たない』なんてことはない」ということです.むしろややこしい?

今の場合,無限に何度もなりたって欲しいのは (p i) です.あるとき以降,あるプロセスだけ共有資源がもらえなくなる,なんてことはない,ということです.「そういうことはない」という検査なので,いつものように否定の形にします.これで反例が見つかれば「いや,そういうときがある」ということになるからです.ややこしいですね...

対称性から (p 0) だけ調べれば十分でしょう.

(check (LTL SYSTEM (not (G (F (p 0))))))

検査をすると反例が見つかります.念のため全体を示しましたが,問題になるのは黒い状態で挟まれた繰り返しの部分です.

m1.png

これを見るとプロセス0はロックを要求しているのに永久に与えられません.このミューテックスのモデルは公平性を持っていないのでこうなります.たとえ現実の実装では起こらなくても,モデル検査は理論的な解を見つけてしまいます.


公平性の仮定を導入する

実装として公平性を保証する必要があるのであれば,モデルとしても公平性を実現することになるわけですが,そうではなく「現実にはまず起こらないし問題にならない」というケースの場合,モデルはそのままでなんとかレアケースを排除したいということもあります.

そういうときは検査式の方に公平性の仮定を入れます.今の場合,「ロックを要求したらいつかは必ず与えられる」という条件を追加します.このイディオムは $\mathsf{GF}\phi \rightarrow\mathsf{GF}\psi$ です.$\phi$ が無限に何度も成り立つならば,$\psi$ も無限に何度も成り立つ,ということです.いまの場合


  • $\phi$ = ロックを要求している

  • $\psi$ = ロックを獲得している

とすればよいことになります.

「ロックを要求している」という状態は (lock i) の発生から (ret i) までの区間で,「ロックを獲得している」という状態は (ret i) の発生から (unlock i) までの区間です.これを fluent として定義すればいいのですが,もっと簡便な方法があるのでここではそれを使います.

イベント e について @e と書くと「イベント e が発生した直後の状態である」という fluent になります.executed(e) と呼ばれることもあります.これを使うと,公平性の仮定を入れた検査式は次のようになります.

(check (LTL SYSTEM

(not
(imp
(imp (G (F @(lock 0))) (G (F @(ret 0))))
(G (F (p 0)))))))

これで検査を行うと,また反例が見つかります.

m2.png

パスを見ると,プロセス0はロックの要求 (lock 0) を出していません.ミューテックスの公平性と同じように,モデル検査はスケジュールの公平性についてもレアなケースを見つけてしまいます.


スケジュールにも公平性の仮定を入れる

スケジュールの公平性が問題にならない場合は,ミューテックスのときと同様に公平性の仮定を入れることでレアケースを避けることができます.

今の場合,「(lock i) がまったく発生しなくなることはない」という条件を入れます.

(check (LTL SYSTEM

(not
(imp
(and (G (F @(lock 0)))
(imp (G (F @(lock 0))) (G (F @(ret 0)))))
(G (F (p 0)))))))

これで検査が通るようになりました.


まとめと注意


  1. 公平性が保証されないミューテックスの実装がある.

  2. 実際には問題にならないケースもモデル検査は見つけてしまう.

  3. それを抑制するには公平性の仮定を検査式に入れる.

問題を無視するように条件を入れて,それでなくなってよかったよかったといっているだけのようにも見えますし,実際そういう側面はあるのですが,それでも意義はあります.なぜかというと,問題にならないレアケースを抑制したいのは,それが他の問題を隠しているかもしれないからです.先に発見されてしまう公平性の問題を抑制しないと,それ以外の問題が見えないからです(すべての問題を発見するツールならば話は別です).

モデルに手を加えずに,検査式に公平性の仮定を入れるのは非破壊検査のように見えるのですが,実はそうではない場合があります.結果として本来ある問題を消してしまうことがあります.機会があったらそれについても書きます.