アルゴリズムの不変量

【 アルゴリズムの不変量 】

並列アルゴリズムを、状態の遷移として記述するアプローチを「状態モデル」と呼びます。

このアプローチとは別に、イベントの継起として並列アルゴリズムを記述するモデル「イベント・モデル」があるのですが、それについては後で述べます。

状態モデルでは、
　● 状態は、変数への値の割り当てです。
　● 状態の遷移の系列を「振る舞い Behavior」と呼びます。
　● 状態の遷移を引き起こすものを「アクション」と呼びます。

同一のFIFOアルゴリズムでも、可能なシステムの振る舞いは、多様です。それは無数に存在します。

ここでは状態の遷移を引き起こすアクションを並べて、振る舞いを記述してみます。先のセッションを参照ください。

システムの可能な振る舞いの例 1
　　P P P C P C P …

システムの可能な振る舞いの例 2
　　P C P C P C …

システムの可能な振る舞いの例 3
　　P P P C C C P …

このアルゴリズムに基づく振る舞いは無限個存在するのですが、重要なことは、この状態モデルで全てのアクションの実行の全てのステップで成り立つ、状態についての論理式が存在刷ることです。

こうした状態についての論理式を、アルゴリズムの「不変式」「不変量」と呼びます。

次に見るbounded FIFO queue のアルゴリズムの「不変量」の存在は、このアルゴリズムがN個の容量のバッファを持つbounded FIFO queue の正しい仕様であることを示唆しています。

N個の容量のバッファを持つ bounded FIFO queueアルゴリズムの「不変量」は次のものです。

　　( Len(buf) ≦ N ) ∧ ( Input = out◦buf◦in )

ここで、記号◦は、リストの結合を表しています。

最初の項( Len(buf) ≦ N ) が成り立つのは、バッファーの容量は、高々N個であるという仮定から明らかです。

第二項 ( Input = out◦buf◦in ) については、初期状態では、Input=in で out=buf=<.> で成り立っています。

ある状態 st でこの式が成り立っていると仮定して、その次の状態 st’ でもこの式が成り立っていることを示せば、帰納法でこの式が不変量であることを示すことができます。

スライドをご覧ください。

-------------------------------------------

セッションの動画のURL https://youtu.be/6Q5N9hDAe9o?list=PLQIrJ0f9gMcOeqlB09PdBddfXLv2QjG-F

スライドのpdf https://drive.google.com/file/d/14gN7smiesFPvO55033JsLB637UfLaU_j/view?usp=sharing 関連blog 「アルゴリズムの不変量」 https://maruyama097.blogspot.com/2022/07/blog-post_294.html 参考資料 Lamport, L. The Computer Science of Concurrency: The Early Years https://cacm.acm.org/magazines/2015/6/187316-turing-lecture-the-computer-science-of-concurrency/fulltext#R9

Ashcroft, E.A. Proving assertions about parallel programs. J. Comput. Syst. Sci. 10 (February 1975), 110135. https://www.sciencedirect.com/science/article/pii/S0022000075800183?via%3Dihub

セミナーのまとめページ https://www.marulabo.net/docs/concurrent/

セミナー告知・申込ページ https://concurrent.peatix.com/view -------------------------------------------