アクターモデル理論

理論計算機科学において、アクターモデル理論はアクターモデルに関する理論的問題を扱います。

アクターは、同時デジタル計算のアクター モデルの基礎を形成するプリミティブです。アクターは、受信したメッセージに応じて、ローカルな決定を下し、より多くのアクターを作成し、より多くのメッセージを送信し、次に受信したメッセージに応答する方法を指定できます。アクター モデル理論には、アクター計算のイベントと構造の理論、その証明理論、および表示モデルが組み込まれています。

アクターの定義から、ローカル決定、アクターの作成、メッセージの送信、メッセージの受信、次に受信したメッセージへの応答方法の指定など、多数のイベントが発生することがわかります。

ただし、この記事では、Actor に送信されたメッセージの到着というイベントのみに焦点を当てます。

この記事はHewitt [2006]に掲載された結果を報告しています。

可算性の法則: 最大で可算な数のイベントが存在します。

活性化順序付け ( -≈→) は、あるイベントが別のイベントを活性化することをモデル化する基本的な順序付けです (あるイベントから、それが活性化するイベントに渡されるメッセージにはエネルギーの流れがなければなりません)。

• エネルギーの伝達のため、活性化順序は相対論的に 不変です。つまり、すべてのイベントに対して です。の場合、すべての観測者の相対論的参照フレームにおいて、の時間は の時間よりも先行します 。e1e2e1 -≈→ e2e1e2
• 活性化順序付けに関する厳密な因果律: いかなるイベントも活性化順序付けを行わないe -≈→ e。
• 活性化順序における有限先行法則: すべてのイベントに対して、集合は有限です。e1{e|e -≈→ e1}

アクターx( -x→ ) の到着順序は、メッセージが に到着するイベントの (全体の) 順序をモデル化しますx。到着順序は、メッセージ処理の調停によって決定されます (多くの場合、アービターと呼ばれるデジタル回路が使用されます)。アクターの到着イベントは、その世界線上にあります。到着順序は、アクター モデルが本質的に不確定性を持つことを意味します (並行計算における不確定性を参照)。

• アクターの到着順序のすべてのイベントはxの世界線上で発生するためx、アクターの到着順序は相対論的に不変です。つまり、すべてのアクターxとイベントに対して、の場合、すべての観測者の相対論的参照フレームでは、の時間は の時間よりも先行します。e1e2e1 -x→ e2e1e2
• 到着順序における有限先行法則: すべてのイベントとアクターの 集合は有限です。e1x{e|e -x→ e1}

結合された順序付け ( で示される) は、すべてのアクターのアクティブ化順序付けと到着順序付けの 推移閉包→として定義されます。

• 結合された順序付けは、相対論的に不変な順序付けの推移的閉包であるため、相対論的に不変です。つまり、すべてのイベントについて、の場合、 の時間は、すべての観測者の相対論的参照フレームでの時間よりも前になります。e1e2e1→e2e1e2
• 複合順序付けに対する厳密な因果律: いかなるイベントも を行ないませんe→e。

結合された順序は、定義により明らかに推移的です。

[Baker and Hewitt 197?]では、上記の法則から次の法則が導かれるのではないかと推測されました。

複合順序付けにおけるイベント間の有限連鎖の法則:複合順序付けにおける 2 つのイベント間には、イベントの無限連鎖 (つまり、線形順序付けされた集合) は存在しません →。

しかし、[Clinger 1981]は驚くべきことに、複合順序付けにおけるイベント間の有限連鎖の法則が以前の法則とは独立していることを証明しました。 つまり、

定理。 複合順序付けにおけるイベント間の有限連鎖の法則は、前述の法則からは導き出されません。

証明。前述の法則を満たすが、複合順序付けにおけるイベント間の有限連鎖の法則に違反するアクター計算が存在することを示すだけで十分です。

アクターInitialにメッセージが送信されStart、次のアクションを実行する 計算を考えてみましょう。

1. Greeter ₁のアドレスでメッセージを送信する新しいアクターGreeter _{1を作成します。}SayHelloTo
2. Greeter ₁のアドレスを記載したメッセージをInitialに送信するAgain

その後、アドレスGreeter _iのメッセージを受信すると、 Initialの動作は次のようになります(これをイベントと呼びます)。 AgainAgaini

1. アドレスGreeter _iのメッセージを送信する新しいアクターGreeter _{i+1を作成します。}SayHelloTo
2. Greeter _i+1のアドレスを含むメッセージをInitialに送信するAgain

明らかに、 Initialが自分自身にメッセージを送信する計算はAgain決して終了しません。

各 Actor Greeter _iの動作は次のとおりです。

• Greeter _i-1のSayHelloToアドレスを持つメッセージ（これをイベントと呼ぶ）を受信すると、Greeter _i-1にメッセージを送信する。SayHelloToiHello
• Helloメッセージ (イベントと呼びます)を受信して​​も、何も実行されません。Helloi

今では毎回、したがって、が可能です。Helloi -Greeteri→ SayHelloToiHelloi→SayHelloToi

また毎回、したがって。Againi -≈→ Againi+1Againi → Againi+1

さらに、複合順序付けの厳密な因果律の前に述べられたすべての法則が満たされます。

ただし、 と の間の組み合わせ順序には、次のように無限の数のイベントが存在する可能性があります。Again1SayHelloTo1

Again1→...→Againi→...${\displaystyle \infty }$...→Helloi→SayHelloToi→...→Hello1→SayHelloTo1

しかし、物理学では、無限のエネルギーを有限の軌道に沿って消費することはできないことが分かっています。したがって、アクター モデルは物理学に基づいているため、複合順序付けにおけるイベント間の有限チェーンの法則がアクター モデルの公理として採用されました。

複合順序付けにおけるイベント間の有限連鎖の法則は、次の法則と密接に関連しています。

離散性の法則: すべてのイベントおよびに対して、集合は有限です。e1e2{e|e1→e→e2}

実際、前の 2 つの法則は同等であることが示されています。

定理 [Clinger 1981]。 離散性の法則は、複合順序付けにおけるイベント間の有限連鎖の法則と同等です(選択公理は使用しません)。

離散性の法則はゼノマシンを排除し、ペトリネットの結果に関連しています[Best et al. 1984, 1987]。

離散性の法則は、無制限の非決定性の性質を意味します。結合された順序付けは、[Clinger 1981] によってアクターの表示的モデルの構築に使用されます (表示的意味論を参照)。

Clinger [1981]は、上記のアクターイベントモデルを使用して、パワードメインを使用するアクターの表示的モデルを構築しました。その後、Hewitt [2006]は、到着時間で図を拡張し、技術的に単純で理解しやすい 表示的モデルを構築しました。

• 俳優モデルの初期の歴史
• アクターモデルとプロセス計算
• アクターモデルの実装

• Carl Hewitt他 「アクター誘導とメタ評価」ACM プログラミング言語の原理に関するシンポジウム会議記録、1974 年 1 月。
• アイリーン・グレイフ。 並列プロセスの通信の意味論、 MIT EECS 博士論文。1975 年 8 月。
• Edsger Dijkstra.プログラミングの規律Prentice Hall. 1976 年。
• Carl Hewitt とHenry Baker の 「アクターと連続関数」、 プログラミング概念の形式的記述に関する IFIP ワーキング カンファレンスの議事録。1977 年 8 月 1 ～ 5 日。
• Henry Bakerと Carl Hewittプロセスの増分ガベージ コレクション、人工知能プログラミング言語に関するシンポジウムの議事録。SIGPLAN 通知 12、1977 年 8 月。
• Carl Hewitt とHenry Bakerによる 並列プロセスの通信の法則IFIP-77、1977 年 8 月。
• 米澤明 「メッセージ パッシング セマンティクスに基づく並列プログラムの仕様と検証手法」 MIT EECS 博士論文。1977 年 12 月。
• Peter Bishop超大規模アドレス空間モジュール拡張可能コンピュータ システムMIT EECS 博士論文。1977 年 6 月。
• カール・ヒューイット。制御構造をメッセージ受け渡しのパターンとして見る、人工知能ジャーナル、1977 年 6 月。
• ヘンリー・ベイカー。リアルタイム計算のためのアクターシステム、 MIT EECS 博士論文。1978 年 1 月。
• Carl Hewitt と Russ Atkinson。 シリアライザの仕様と証明手法、 IEEE Journal on Software Engineering、1979 年 1 月。
• Carl Hewitt、Beppe Attardi、Henry Lieberman。 メッセージ パッシングの代表団、第 1 回国際分散システム会議議事録、アラバマ州ハンツビル。1979 年 10 月。
• Russ Atkinson. シリアライザの自動検証MIT 博士論文。1980 年 6 月。
• ビル・コーンフェルドとカール・ヒューイット。 科学コミュニティのメタファー、 IEEE Transactions on Systems, Man, and Cyber​​netics。1981 年 1 月。
• ジェリー・バーバー。 知識オフィス システムの変化に関する推論MIT EECS 博士論文。1981 年 8 月。
• ビル・コーンフェルド。 問題解決における並列性、 MIT EECS 博士論文。1981 年 8 月。
• ウィル・クリンガー。 アクターセマンティクスの基礎、MIT 数学博士論文。1981 年 6 月。
• Eike Best .並行動作: シーケンス、プロセス、公理コンピュータサイエンス講義ノート Vol.197 1984 年。
• Gul Agha. アクター: 分散システムにおける並行計算のモデル、博士論文。1986 年。
• Eike Best と R.Devillers。ペトリネット理論における順次動作と並行動作、理論計算機科学 Vol.55/1。1987 年。
• Gul Agha、Ian Mason、Scott Smith、Carolyn Talcott。 「アクター計算の基礎」 Journal of Functional Programming、1993 年 1 月。
• 松岡 聡、米沢 明徳. オブジェクト指向並行プログラミング言語における継承異常の分析、並行オブジェクト指向プログラミングの研究方向、1993年。
• Jayadev Misra. 並行プログラミングのロジック: Safety Journal of Computer Software Engineering. 1995 年。
• ルカ・デ・アルファロ、ゾハル・マナ、ヘンリー・シプマ、トマス・ウリベ。 リアクティブ システムの視覚的検証TACAS 1997。
• Thati、Prasanna、Carolyn Talcott、Gul Agha。仕様図の実行と推論のテクニック、代数的方法論とソフトウェア技術に関する国際会議 (AMAST)、2004 年。
• Giuseppe Milicia と Vladimiro Sassone。 継承の異常: 2004 ACM 応用コンピューティングシンポジウム (SAC) の 10 年後の議事録、ニコシア、キプロス、2004 年 3 月 14 ～ 17 日。
• ペトラス・ポティエター。ゼノマシンとハイパーコンピューティング 2005
• カール・ヒューイット「コミットメントとは何か? 物理的、組織的、社会的 COINS@AAMAS」2006 年。