Think Stitch
PRINCIPIA  最近の更新


活性(liveness)の検査

公平なミューテックス(スタベーション問題)他で、ミューテックスの公平性を検査しました。 そこで調べたのは「ミューテックスのロック獲得システムコール lock(p) を呼び出したら、いずれ必ずロックが獲得できる。」という条件でした。 つまり飢餓状態は起こらないという条件です。 これは一般的に「あるイベント x が発生したら、そのあとで、いずれ必ずイベント y が発生する」という形をしています。 このような条件のことを活性(liveness)といいます。 応答性という用語を使っている文献もあります。

前に行った検査では、有限の長さ L を設定して、イベント x が発生してから L ステップ以内に y が発生するという仕様を作成し、正当性を比較することで検査を行いました。 ここでは、活性を検査するための、もう1つの方法をご紹介します。

安全性・活性・公平性

同じ問題に対して公平性と活性という2つの概念が出てきて、ちょっとややこしいと思いますので、整理をしたいと思います。 まず活性は安全性と並べられる性質で、一般に並行システムが持つべき重要な性質の種類になります。

安全性(safety)
仕様に書かれていること以外のこと(つまり何か悪いこと)が起こらないという性質。
活性(liveness):
仕様に書かれていること(つまりやらなければいけないこと)が必ず起こるという性質。

これに対して公平性というのは、特に遷移に関する次のような性質のことでした。

公平性(liveness):
ある遷移について、プロセスがその遷移の遷移元状態に訪れる機会が無限にあって、しかも発生する可能性のある場合も無限にあるならば、いつかは必ず発生するという性質。

「発生する可能性がある」というのは、その遷移が tau 遷移またはtick 遷移であるか、あるいは一般のイベントが付随する遷移ならば、相互作用を行う対向のプロセスもイベントを提示しているという意味です。

ミューテックスのロックについての文脈では、「ロックを要求したらいつかは獲得できる」というように相対的に俯瞰的な立場から表現をすると活性で、「ロックを獲得しようとして競合しているプロセスには等しくチャンスがあるので、いずれは必ずロックが得られる」というようにミクロな視点でいえば公平性ということになります。 後者では、最終的にロックを獲得することに対応する遷移が公平であるということです。 やや日常的な意味でいえば、そこで競合しているプロセスに対応する各遷移が選択肢として並んでいて、そこからの選択が公平であるという意味です。

イベントが必ず発生するという条件

活性のもっともシンプルな形は「次にイベント e が必ず発生する」というものです。 これは拒否を使って表すことができるのでした(ご存じない方は SyncStitch ユーザガイドをごらんください。) これについて簡単に復習することにします。

イベント e が発生して停止するプロセスは次のとおりです。 これを仕様と考えることができます(小さな○も普通の状態です。単に名前を省略しているだけです)。

例えば次のようなプロセスがあった場合、必ずイベント e が発生するとはいえません。

これに対して、次のような場合、tau 遷移は観測にかからないし、かならず発生するので、最終的にはイベント e が必ず発生することになります。

以上のことは仕様 P0 と正当性検査を行えば、確認することができます。 トレースによる比較だけでは「かならず発生する」ということがいえないという点も確認しておきます。

他にも次のような可能性があります。非決定的選択の一方が発散している場合です。

この状態遷移図は発散を含んでいるのでコンパイルできません。 代わりにプロセス式を使って次のように定義します。

(define-process P3
  (ndc
    (! e STOP)
    DIV))
(define-process DIV
  (hide (list x) DIV0))

(define-process DIV0
  (! x DIV0))

計算木を見ると、確かに上の状態遷移図と同じプロセスであることがわかります。

この場合、正当性検査をパスしてしまうので、それとは別に発散の検査を行う必要があります。 この点についてはユーザガイドでも述べました。

まとめると、次にイベント e が必ず発生するということを確認するには、正当性検査と発散検査の両方を行う必要があるということです。 こうすれば、例えばイベント e に至るパスの途中に発散がある場合も排除することができます。

最後の2つの検査項目を作って、プロセス P3 と DIV をそれぞれトレースモードで観ると次のようになります。

まず発散するだけで他に何もしないプロセス DIV は、拒否を全く持っていない(空集合もない)ことがわかります。

一方、プロセス P3 は発散しているにもかかわらず拒否(表示はもちろん極小受理)を持っています。 非決定的選択の拒否は、各分岐の拒否の和集合になるので、1つが発散していても、他の分岐が拒否を持っていれば空にはならないのでした。 拒否があるから発散していないとはいえない、ということを再度強調しておきます。 かならず別に発散検査が必要です。

「イベントが必ず発生する条件」の復習は以上です。

いつかは必ずイベント e が発生するという条件

次にもう少し一般的な「いつかは必ずイベント e が発生する」という条件を考えます。 イベント e が発生するまでの間に、他の任意のイベントが発生してもかまわないということです。 e 以外のイベントが永久に続いたり、途中で発散したりするのはだめです。

例えば、もっとも単純なのは次のような場合です。

基本的なアイデアは、イベント e 以外のイベントを隠蔽してしまうというものです。 そのために、次のようなプロセスを定義します(高階プロセスであることは内緒です)。

(define-process (HEE P)
  (hide (remq e Events) P))

すると、イベント e がいつか必ず起こることを、次のように検査を行うことができます。

次のような場合は、下の分岐が選ばれる可能性があるので、必ず e が発生するとはいえません。

これも確かに検査することができます。

循環がある場合 1

問題は次のようにイベントの循環がある場合です。 この場合、プロセスが永久に循環を回る可能性があるので(公平性はないので)、必ずイベント e が発生するとはいえません。

このことは発散検査で知ることができます。循環を形成するイベントをすべて隠蔽すると発散するからです。

循環がある場合 2

次のように、イベント e が発生したあとに循環がある場合は問題です。 循環は e 発生のあとですから、活性の条件は満たしています。 しかし発散してしまうので、発散検査にひっかかってしまうからです。

これを避けるために、注目しているイベント e が発生したら、その後のことは無視することにします。 これは次のように制約プロセスを使って実現することができます。

(define-process (HEECA P)
  (hide (remq e Events)
    (par Events
      P
      (CUTAFTER (list e)))))

ここでプロセス (CUTAFTER A) はイベントのリスト A に含まれるイベントが発生したら停止するプロセスです。 それ以外のイベントは何が何回起こってもかまいません。

(define-process (CUTAFTER A)
  (let ((B (lset-difference eq? Events A)))
    (CUTAFTER-HUNT A B)))

(define-process (CUTAFTER-HUNT A B)
  (alt
    (xalt e A (! e STOP))
    (xalt e B (! e (CUTAFTER-HUNT A B)))))

これによってプロセス P8 "切り取った" 残りを見てみましょう。 まず次のようにプロセスを定義します。

(define-process P8HEECA (HEECA P8))

これをプロセスエクスプローラで表示し、さらにプロセス木から隠蔽されていないサブプロセスを開きます。

すると下図のように、イベント e の後ろが切り取られていることが確認できます。

これで活性の検査が可能になりました。

トリガとなるイベントがある場合

次に、より一般的な場合「イベント b が発生したら、そのあと、いずれ必ずイベント e が発生する」という条件の場合を考えます。 例えば次のようなプロセスの場合です。

この場合、イベント c から始まる下の分岐先にイベント e はありませんが、イベント b から始まる上の分岐には e がありますから条件を満たします。

これを検査するには、イベント e の後ろを切り捨てたように、b ではないイベントから始まる分岐を切り捨ててしまえばよいのです。 ここでは簡単に、次のようにしました。

(define-process (HEECAB P)
  (hide (remq e Events)
    (par Events
      P
      (! b (CUTAFTER (list e))))))

先ほどと同じように、隠蔽の中のサブプロセスを見ると、イベント c の分岐が切り取られていることがわかります。

検査は次のようになります。

最後に、一般的な場合を検査してみました。

補足

計算あるいは状態遷移のモデルにはいくつものバリエーションがあるので、公平性の定義もそれに応じて定義が異なる場合があるようです。 また公平性自体にも複数の細かい分類があるようです。詳しくは専門書を見ていただく方がよいと思います。

ミューテックスの公平性を確認するために使った手法を有限ステップ法とでも呼ぶことにします。 これに対してここで紹介した方法を隠蔽法とでもいいましょうか。 どちらももちろんここだけの用語です。家の外では恥ずかしくていえません。 有限ステップ法は長さを指定しなければならないという欠点があります。 検査自体にある程度の試行錯誤が必要ですし、検査に通らないからといって活性がないとはいえませんでした。

これに対して隠蔽法ではステップ指定も試行錯誤も必要なく、結果は白黒はっきりします。 少し欠点があるとすれば、イベントが隠蔽されているので違反があったときの分析がやや面倒ということくらいでしょうか。 もっともこれも方法の問題ではなく、SyncStitch の問題なんですけどね。

同じくこれも SyncStitch の課題なのですが、隠蔽法の方が、ちょっとだけ少ないメモリで検査できるはずなのですが、いまはあまり差がありません。 いずれ改善したいと思っています。

尚、活性の検査は時間論理(時相論理)を扱うことのできるツールの方がはるかに簡単に実行できます。

2013/09/12
© 2013,2014,2015 PRINCIPIA Limited