アルゴリズムの標準モデル

【 アルゴリズムの標準モデル 】

分散・並列アルゴリズムに、「時間」の概念が必要であることは、ある意味わかりやすいことかもしれない。

計算アルゴリズムの標準的なモデルは、Turing マシンである。多くの人は、分散・並列アルゴリズムのモデルには、Turingマシンは使えないと感じると思う。確かに、Turingマシンには「時間」の概念はない。また、ローカルな「プロセス」という概念もない。そこでの「状態」の概念は、Turing マシン全体にとってグローバルなものだ。

ただ、そうではないと、ランポートは言う。

なぜなら、グローバルなシステムのある不変量という概念は、意味のある概念である。それは、すべての可能なグローバルな状態についての述語であり、特定のグローバルな状態には依存しない。分散システムを実装すると言う問題は、異なるプロセスを通じて、システム全体の不変量を維持することと見ることができる。

ランポートは、並列・分散システムも Turing マシンの標準モデルで記述できると言う。

それでは、前回見たような分散・並列アルゴリズムの記述に必要な「時間」概念は、どうなってしまうのだろうか? 今回 紹介した論文 " The temporal logic of actions "は、まさに、こうした疑問に応えるものだ。

分散・並列アルゴリズムで、ある状態 s が状態 t に変化したとする。これを、s -> t と表すことにしよう。状態 s で利用されている変数を x, y, z, ... とした時、状態 s から変化した状態 t で利用される変数を、状態 s で利用されている変数名にプライム(ダッシュ)を付けて、x', y', z', ... と表すことにする。ここで、状態というのは、変数への値の割り当てであることに留意しよう。

この時、プライムなしの変数とプライム付きの変数から構成される式を、状態の変化 s -> t の「アクション」と呼ぶ。次の式は、アクションの例である。

  x' = x + 1

この式は、x  の値は、s -> t である状態 t では、状態 s での変数の値 xを使えば、x + 1に変わることを表している。( s -> t  で変数xの値は、1 増えるということである。)

逆に、s -> t 上で定義された アクション式 A が真であるなら、状態 s から状態 t への状態変化は可能である。

ランポートは、アクション式を対象とした論理は、Turingマシンを用いた標準モデルで表現できることを示す。

この標準モデルには、実は、時間の概念(物理的な時間ではなく「論理敵時間」なのだが)がしっかりと組み込まれている。なぜなら、アクションは、状態変化 s -> t  の上で定義されるのだが、そこでは、「論理的時間」のステップが、一つ確実に進んだと考えることができるからである。

後日、ランポートが実装を完成するシステムでは、論理的時間のステップを通じて到達可能な状態をすべて生成する状態マシンを通じて、分散・並列アルゴリズムをモデル化して、それをシミレートすることになる。

1990年のこの論文で、その理論的準備は、ほぼ出揃っている。


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

セッションの動画のURL 状態とアクションと時制論理式 https://youtu.be/5bV4UxhPpZM?list=PLQIrJ0f9gMcOeqlB09PdBddfXLv2QjG-F

スライドのpdf https://drive.google.com/file/d/15UXnhuhTHJI6-nQaJ4PwPoETrwhblGbo/view?usp=sharing

関連blog 「アルゴリズムの標準モデル」 https://maruyama097.blogspot.com/2022/07/blog-post_27.html

参考資料

Leslie Lamport. The temporal logic of actions. Technical Report 79, Digital Equipment Corporation, Systems Research Center, December 1991. http://lamport.azurewebsites.net/pubs/old-tla-src.pdf

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

セミナーのまとめページ

https://www.marulabo.net/docs/concurrent/

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

コメント

このブログの人気の投稿

マルレク・ネット「エントロピーと情報理論」公開しました。

初めにことばありき

宇宙の終わりと黒色矮星