ライブネスのソースを表示

'''ライブネス'''とは、並行システムの特性の1つで、同時実行されるコンポーネント（[[プロセス]]）が[[クリティカルセクション]]（複数のプロセスが同時に実行できないプログラムの部分）で「交代」しなければならないにもかかわらず、システムが進行することを意味する<ref>{{Cite journal | last1 = Lamport | first1 = L. | doi = 10.1109/TSE.1977.229904 | title = Proving the Correctness of Multiprocess Programs | journal = IEEE Transactions on Software Engineering | issue = 2 | pages = 125–143 | year = 1977 | citeseerx = 10.1.1.137.9454 }}</ref>。ライブネスの保証は、[[オペレーティングシステム]]や[[分散システム]]において重要な特性である<ref>{{cite book|last=Luís Rodrigues|first=Christian Cachin; Rachid Guerraoui|title=Introduction to reliable and secure distributed programming|year=2010|publisher=Springer Berlin|location=Berlin|isbn=978-3-642-15259-7|pages=22–24|edition=2.}}</ref>。

より一般的には「'''何か良いことが最終的に起こる'''」ことを示すのがライブネス特性であり、「'''何か悪いことが起こらない'''」ことを示すのが安全性特性である。安全特性に違反した場合、その違反（「悪い」イベントの発生）を示す有限実行が必ず存在するが、ライブネス特性は、分散システムの有限実行では、「良い」イベントが後になっても発生する可能性があるため、違反できない。最終的な[[一貫性モデル (ソフトウェア)|一貫性]]はライブネス特性の一例である。すべての線形時間特性は、安全性特性とライブネス特性の交点として表すことができる。与えられた安全性特性の違反が有限の目撃者を認めるのに対し、ライブネス特性の違反は、証明として使用できる有限の目撃者がいないため、立証が困難な場合がある。

== ライブネスの形態==
ライブネスにはいくつかの形態があります。以下のものは、ある[[相互排除]]（[[ミューテックス]]）装置で保護されたクリティカル・セクションを持つマルチプロセス・システムの観点から定義されています。すべてのプロセスがミューテックスを正しく使用していると仮定し、[[クリティカルセクション]]の実行が終了することを進捗と定義する。

* [[デッドロック]]からの解放は、弱いながらもライブネスの一形態である。複数のプロセスと、相互排除装置で保護された1つのクリティカルセクションを持つシステムを考える。このようなシステムは、ある時点であるプロセス群がクリティカルセクションへのアクセスをめぐって競合しているときに、後の時点であるプロセスが最終的に前進する場合、デッドロックフリーであると言われます。そのプロセスは前述のグループに属する必要はなく、それ以前あるいはそれ以降にアクセスを得たかもしれない。
* [[リソーススタベーション|スタベーション]]からの自由（または「有限のバイパス」）は、デッドロックの自由よりも強力なライブ性保証です。これは、臨界領域へのアクセスを争うすべてのプロセスが、最終的に進歩することを意味する。スタベーションのないシステムは、デッドロックのないシステムでもある。
*さらに強力なのが bounded bypass の要件である。これは、n個のプロセスが臨界領域へのアクセスを競っている場合、ある関数fについて他のプロセスから最大f(n)回バイパスされた後、各プロセスが進展することを意味している。

==ライブネスと安全性==
B. Alpernによれば、デッドロックフリーは安全性の性質である。Alpernは、システムの状態が、デッドロックがある状態（赤の状態）と、デッドロックがない状態（緑の状態）に分けられることを前提としている。システムが永遠に緑の状態にとどまる（あるいは、赤の状態にならない）という性質は、安全性の性質である。しかし、緑の状態と赤の状態の区別がつかない場合、最終的にシステム内のいずれかのプロセスが進化するという性質をライブネス性質という。

==形式上の区別==
安全性と有効性の区別は、<math>P(t)</math>という述語によって形式的に確立することができる。 
ここで、<math>t</math>は時間を意味する。<math>t_0</math>をlivenessとsafetyの特性が評価される出発点となる瞬間とする。以下の例では、<math>x</math>をデッドロックフリーであることを保証したいプロセス（またはスレッド）とする。

安全性: <math>\forall t \ge t_0: P(t) = \textrm{False}. </math>

事例: <math>P(t)</math> は "<math>x</math> が時間 <math>t</math>でデッドロックの状態にある"ことを意味する。

ライブネス:  <math>\forall t_1 \ge t_0, \exists t \ge t_1, t < \infty: P(t) = \textrm{True}. </math>
 
事例: <math>P(t)</math> は "<math>x</math> が時間 <math>t</math> で待機、停止する"ことを意味する。

== 境界付きバイパスと境界付き追い越し== 
境界付き追い越し（bounded overtaking）とは、タグ付けされたプロセスがクリティカルセクションに入りたいと宣言した後、タグ付けされたプロセスがクリティカルセクションに入るまでに、他の各プロセスが制限された回数だけタグ付けされたプロセスを追い越すことを意味する。なお、タグ付けされたプロセスがそのクリティカルセクションに入る許可を得られない場合でも、有界追い越しは成立する可能性がある。したがって「境界のある追い越し」はそれだけではライブネス特性とは言えない。デッドロック状態のシステムでは、どのプロセスも他のプロセスを追い越さないため、「境界のある追い越し」は自明に成立するが、境界線付きバイパスは成立しない。

プロセスP1がクリティカルセクションに入ろうとするときはいつでも、プロセスP2はプロセスP1が入ろうとする前に最大で一回だけ入ろうとすることは境界付き追い越し（bounded overtaking）の一例である。

境界付きバイパス（境界付き待機、bounded bypass）とは、あるプロセスがクリティカルセクションに入りたいという意思表示をした後に、他のプロセスによってバイパスされる回数が、システム内のプロセス数の関数によって制限されることを意味する。

境界線付きバイパスの有効性と境界線付き追い越しの安全性の区別は微妙であることにも注目したい。スタベーションフリーダムと「境界付き追い越し」の組み合わせは境界付きバイパスを意味する（つまり境界付きバイパスはライブネス特性に分類されているが、実際にはライブネス特性と安全性特性の混合物である）<ref>{{Cite book | last1 = Fang | first1 = Y. |title = Liveness by invisible invariants | doi=10.1007/11888116_26 | journal = International Conference on Formal Techniques for Networked and Distributed Systems | volume = 4229 | issue = 1 | pages = 356–371 | year = 2006 | series = Lecture Notes in Computer Science | isbn = 978-3-540-46219-4 }}</ref>。

==脚注==
{{reflist|2}}

{{DEFAULTSORT:らいふねす}}
[[Category:並行性]]
[[Category:トランザクション処理]]
[[Category:並列コンピューティング]]