入出力オートマトン

入出力オートマトンでは、ほとんどの種類の非同期並行システムの記述に適用できる形式モデルが提供されます。入出力オートマトン モデルは、それ自体で、さまざまなタイプの 分散システムをモデル化できる非常に基本的な構造を備えています。特定の種類の非同期システムを記述するには、この基本モデルに追加の構造を追加する必要があります。このモデルは、任意の相対速度で動作し、相互に作用するプロセスやメッセージ チャネルなどのシステム コンポーネントを記述および推論するための明示的な方法を提供します。^[1]入出力オートマトンが初めて導入されたのは、 1987 年のNancy A. Lynchと Mark R. Tuttle による「分散アルゴリズムの階層的正しさの証明」です。^[2]

「I/O オートマトンとは、他のシステム コンポーネントと対話できる分散システムコンポーネントをモデル化したものです。これは、遷移が名前付きアクションに関連付けられている単純なタイプのステート マシンです。」^{[1]アクションには、}入力、出力、内部アクション の 3 種類があります。オートマトンでは、入力アクションと出力アクションを使用して環境と通信しますが、内部アクションはオートマトン自体にのみ表示されます。オートマトンによって選択および実行される内部アクションと出力アクションとは異なり、環境から単純に到着する入力アクションは、オートマトンの制御下にありません。^[1]

I/O オートマトンを使用すると、プロセス、メッセージ パッシングシステムのメッセージ チャネル、共有メモリシステムの共有データ構造など、分散システムの個々のコンポーネントをモデル化できます。

図 1 は、非同期メッセージ パッシング分散システムにおけるプロセスの I/O オートマトンの例を示しています。この設定では、プロセス P _{i はメッセージ パッシング システムを使用して他のプロセスと通信します。出力アクションは send(m) i,j} の形式で、プロセス P _{i が内容 m のメッセージをプロセス P j}に送信することを表します。入力アクションは、receive(m) _{k,iの形式で、プロセス P i}がプロセス P _kから内容 m のメッセージを受信することを表します。(プロセスが実行しているアルゴリズムに対応する P _iの内部アクションは示されていません。)

メッセージ チャネルは、I/O オートマトンによってモデル化することもできます。図 2 は、C _{i,jという典型的な単方向}FIFOチャネル オートマトンを示しています。このオートマトンには、 send(m) _i,jという形式の入力アクションと、 received(m) _i,jという形式の出力アクションがあります。各メッセージ m には、0 または 1 (m ∈ {0,1}) が含まれます。オートマトンの状態には、送信されたがまだ受信されていないすべてのメッセージの FIFO キューが格納されます。

プロセスオートマトンと通信チャネルオートマトンの両方が存在する一般的な分散システムでは、一方のオートマトンの出力アクションがもう一方のオートマトンと同じ名前の入力アクションと一致して実行されるように構成されます。たとえば、2 つのプロセス P _iと P _{j 、およびプロセス P i}からプロセス P _jへの通信チャネル C _i,jで構成されたシステムを考えます。この設定では、チャネル C _{i,jも send(m) i,j}入力アクションを実行する場合にのみ、プロセス P _{i は}出力アクション send (m) _{i,j を}実行します。

_{図 3 は、 2 つのプロセス P 1}と P ₂を持つ共有メモリ システム内のアトミックなレジスタ読み取り/書き込み I/O オートマトンを示しています。レジスタに格納されている値 V は、整数型(V ∈ Z ) です。オートマトンの状態はこの値を格納します。入力アクションは、プロセス P _{i が}レジスタに値 V を書き込むことを要求するwrite _{i (V) (ここで i ∈ {1,2} かつ V ∈} Z ) と、プロセス P _{i が}現在レジスタに格納されている値の読み取りを要求するread _{iで構成されます。出力アクション ack i は、プロセス P i に}書き込み要求が正常に完了したことを通知するために使用されます。出力アクション V _{i は、プロセス P i}による読み取り要求への応答として返される値 V を表します。

オートマトンは、内部アクション perform_Write(V) も含みます。これは、オートマトンのステートを更新することによって、レジスタに値 V を書き込みます。また、perform_Read は、ステートに格納されている値 V を読み取るために使用されます。(これらの内部アクションは、図 3 には示されていません。)

I/O オートマトン A、または単にオートマトンは次の 5 つのコンポーネントで構成されます。

• 署名(A)
• 州(A)
• スタート(A)
• トランス(A)
• タスク(A) ^{[1] [3]}

これら 5 つのコンポーネントについては、以下で説明します。

I/O オートマトン A の形式化の最初のステップは、そのシグネチャsig(A) の定義です。シグネチャ S は、3 つの互いに素なアクション セットを使用して I/O オートマトンの動作を記述します。

1. in(S): 入力アクション、
2. out(S): 出力アクション、および
3. int(S): 内部アクション。

上記の入力、出力、内部アクションの形式化に基づいて、次のオブジェクトを定義することができます。

• ext(S):外部アクション、in(S) ∪ out(S) として定義される
• local(S):ローカルに制御されるアクション。out(S) ∪ int(S) として定義される。
• extsig(S):外部署名。(in(S), out(S), ø) として定義される。
• 行為(S)は署名Sのすべての行為の集合として定義される。^{[1] [3]}

オートマトンAの状態集合（states(A)と表記）は有限である必要はありません。これは、カウンタや無制限の長さのキューなどの無制限のデータ構造を持つシステムをモデル化できるため、通常の有限オートマトンの概念を大幅に一般化したものです。開始状態（初期状態とも呼ばれる）の集合は、状態の空でないサブセットです。複数の開始状態が許可されているため、開始状態にいくつかの入力情報を含めることができます。^{[1] [3]}

オートマトン A の状態遷移関係は、trans(A) ⊆ states(A) × act(sig(A)) × states(A) と表されます。これは、「すべての状態 s とすべての入力アクション π に対して、遷移 (s, π, s') ∈ trans(A) が存在する」という特性を満たします。

遷移は、I/O オートマトン A のステップとも呼ばれ、trans(A) の要素 (s, π, s') として定義されます。π が入力アクションの場合、入力遷移は遷移 (s, π, s') を指し、π が出力アクションの場合、出力遷移は遷移 (s, π, s') を指します。任意の状態 s とアクション π について、I/O オートマトン A に形式 (s, π, s') の遷移がある場合、π はs で有効であると言われます。I/O オートマトンはすべての入力アクションがどの状態でも有効である必要があるため、入力有効と呼ばれます。静止状態 s は、入力アクションのみが有効である状態として定義されます。^{[1] [3]}

I/O オートマトン A の 5 番目のコンポーネントであるタスク (A) は、A のローカルに制御されるアクションの同値関係として定義されるタスク パーティションであり、同値クラスの数は最大で可算数です。非公式には、タスク パーティション タスク (A) は、A 内の「タスク」または「制御スレッド」の抽象的な説明を表します。

このパーティションは、オートマトンの実行における公平性条件を定義するために使用されます。これらの条件では、オートマトンが実行中に各タスクに公平な順番を与え続けることが求められます。これは、複数のジョブを実行するシステム コンポーネントをモデル化する場合、特に役立ちます。たとえば、進行中のアルゴリズムに参加しながら、同時にその環境に定期的にステータス情報を報告するコンポーネントには、2 つのタスクがあります。このパーティションは、複数のオートマトンが合成され (より大きなシステム オートマトンを生成するため)、合成されたすべてのオートマトンが合成されたシステムで引き続きステップを実行するように指定する場合にも役立ちます。^{[1] [3]}

上で説明したように、C _{i,j はプロセス P i}からプロセス P _jへの一方向 FIFO チャネルを表す I/O オートマトンの例です。m をバイナリ メッセージとします: m ∈ {0,1}。オートマトン C _{i,j は}次のように正式に定義できます。

サイン：

sig(C _i,j ) は、オートマトンの2種類のアクションを指定します。

• _{(C i,j} )の入力アクションはsend(m) _i,jの形式をとり、ここでm∈{0,1}である。
• _{(C i,j} )の出力アクションはreceive(m) _i,jの形式をとります。ここでm∈{0,1}です。

直感的には、アクションsend(m) _{i,jは、メッセージmがプロセスP i}によって送信されたときにチャネルに入ったことを示し、アクションreceive(m) _{i,jは、メッセージmがプロセスP j}に配信されたときにチャネルから出たことを示します。^[1]

州:

states(C _i,j ) は、要素 m ∈ {0,1} のすべての有限シーケンスの集合です。直感的に言えば、状態は、送信者プロセス P _iから受信者プロセス P _jへ現在送信中のメッセージのシーケンスを、送信順に表します。

キューの初期状態を表すstart(C _i,j )には空のシーケンスのみが含まれます。^[1]

トランジション

遷移関係は、前提条件効果スタイルでモデル化できます。このスタイルでは、特定の種類のアクションを含むすべての遷移が 1 つのコードにグループ化されます。このコードでは、アクションが発生する前に満たす必要がある条件が、アクションが発生する前の状態である事前状態 s の述語として形式化されます。アクションの実行によって生じる状態の変更は、単純なプログラムの形式でコード化されます。このプログラムは、単一の遷移として分割せずに実行されます。このプログラムを状態 s に適用すると、新しい状態 s の結果になります。

_{C i,j}の遷移は次のように記述されます。

send(m) _i,jの場合:

• 前提条件: なし
• 効果: 状態に格納されているシーケンスの末尾に m が追加されます (m ∈ {1,0})

受信(m) _i,jの場合:

• 前提条件: mは状態に格納されているシーケンスの最初の要素です（ただし、m∈{1,0}）
• 効果: 状態に格納されているシーケンスの最初の要素を削除します

直感的に言えば、送信アクションはいつでも実行でき、チャネル内のメッセージキューの末尾にメッセージmを追加します。受信アクションはキューの最初の要素を削除して返します。^[1]

タスク

タスク(C _i,j )は、受信フォームのすべてのアクションを1つのタスクにグループ化するタスクパーティションを表します。直感的には、プロセスP _jにメッセージを渡すことは、1つのタスクと見なされます。

{receive(m)i,j : m ∈ {0,1}}^[1 ]

オートマトンの実行では、オートマトンがモデル化するコンポーネントの動作を記述する文字列が生成される。 ^[3]「I/OオートマトンAの実行フラグメントは、

• 有限シーケンス、 s ₀、 π ₁、 s ₁、 π ₂、...、 π _r、 s _r、または
• 無限シーケンス、s ₀、π ₁、s ₁、π ₂、...、π _r、s _r、...、

A の交互の状態と動作の集合であり、(s _k、π _k+1、s _k+1 ) は任意の k ≥ 0 に対して A の遷移である。

有限シーケンスは、必ず状態で終了する必要があります。実行は、開始状態から始まる実行フラグメントとして定義されます。A の実行セットは、execs(A)で表されます。I /O オートマトン A の到達可能な状態は、A の有限実行の最終状態です。

_{α は状態 s f}で終わる A の有限実行フラグメントであると仮定する。さらに、 α' はα の最後の状態s _{fで始まる A の任意の実行フラグメントであると仮定する。この場合、 α と α'}を連結し、 α の最後の状態 s _fの重複を排除することによって生成されるシーケンスは、 α.α' で表される。このシーケンスも I/O オートマトン A の実行フラグメントである。^[1]

I/OオートマトンAのトレースは、Aの実行αで発生する外部アクションのシーケンスです。Aのすべてのトレースの集合はtraces(A)として表されます。^[1]

実行 a、b、c は、チャネル I/O オートマトン (メッセージ m ∈ {0, 1}) の正式な定義で説明されているオートマトン C _i,jの 3 つの実行です。この例では、キュー内のメッセージのシーケンスを括弧で囲むことで状態が示され、空のシーケンスは λ で表されます。

(a) [λ]、送信(1) _i,j、[1]、受信(1) _i,j、[λ]、送信(0) _i,j、[0]、受信(0) _i,j、[λ]

(b) [λ]、送信(1) _i,j、[1]、受信(1) _i,j、[λ]、送信(0) _i,j、[0]

(c) [λ]、送信(1) _i,j、[1]、送信(1) _i,j、[11]、送信(0) _i,j、[110].... ^[1]

それぞれが個別のシステム コンポーネントを記述する複数のオートマトンを合成して、より大規模で複雑なシステムを表すオートマトンを生成することができます。この場合、各構成オートマトンで同じ名前を持つアクションはまとめて識別されます。したがって、コンポーネント オートマトンがアクション π を含むステップを実行すると、署名に π が含まれる他のすべてのコンポーネント オートマトンもそのアクションを実行します。次に、オートマトン A と A' の合成が許可される条件を示します。

1. A の内部アクションは、A' のアクションとは分離されている必要があります。これにより、A' のアクションと同じ名前を持つ A の内部アクションが実行されたときに、A' のステップが実行されることが防止されます。
2. A と A' の出力アクションは互いに独立している必要があります。この条件により、出力アクションのパフォーマンスを制御する構成オートマトンが 1 つだけであることが保証されます。

構成が可算無限のオートマトンから構成される場合、追加の制約があります。各アクションは、構成するオートマトンのうち有限個のアクションのみである必要があります。オートマトンを無限に構成することで、多くの論理コンポーネントから構成される論理システムをモデル化できます。論理システムは、多くの場合、より少ないコンポーネントを含む物理システム上に実装されます。^[1]

_{図 4 は、 2 つのプロセス P i}と P _j、および FIFO メッセージ チャネル C _i,jの構成を示しており、1 つのオートマトンの出力アクションが他のオートマトンと同じ名前の入力アクションと一致しています。したがって、プロセス P _iによって実行されるsend(m) _{i,j出力は、チャネル C i,jによって実行される send(m) i,j}入力と一致して実行されます。

プロセス P _{i は、チャネル C i,j}を介してプロセス P _jにメッセージ m (m ∈{1,0}) を送信します。プロセス P _{j は、}内部アクションの反転(図には示されていません) を使用して、 P _iから受信したメッセージ m のビットを反転し、そのメッセージをシステムの他の部分に転送します。

I/O オートマトンの出力アクションを「内部アクションとして再分類する」ことで非表示にすることができます。これにより、システムの他の部分との通信から出力アクションが除外されます。正式には、署名の非表示操作は次のように説明されます。

Sを署名とし、Φ⊆out(S)とする。hideΦ (S)_は新しい署名S'であり、ここで

• in(S')= in(S)
• アウト(S')= アウト(S) - Φ
• int(S') =int(S) ∪ Φ

したがって、「Aがオートマトンであり、Φ⊆out(A)である場合、hideΦ _{( A)は、Aからsig(A)をsig(A') = hideΦ} (sig(A))に置き換えることによって得られるオートマトンA'である。」^[1]

タスク パーティションは、I/O オートマトンがローカルに制御するアクションの同値関係として定義され、最大で可算数の同値クラスを含むことを思い出してください。この設定では、公平性は各タスクにアクションを実行する機会を継続的に提供することとして定義できます。

I/O オートマトン A において、C がタスクのクラス (A) を表すものとします。正式には、A の実行フラグメント α は、すべてのクラス C に対して以下の基準が満たされている場合に 公平であるとみなされます。

1. 「α が有限の場合、α の最終状態では C は有効になりません。」
2. 「α が無限の場合、α には C からのイベントが無限に含まれ、または C が有効になっていない状態の発生が無限に含まれます。」

イベントは、「実行やトレースなどのシーケンス内でのアクションの発生」として定義されます。公平性の定義「無限に頻繁に」に基づいて、各タスク (または同値クラス C) はアクションを実行する機会を得ます。タスク (または同値クラス) C がアクションを実行する機会を得た場合、2 つのケースが考えられます。C のアクションが現在の状態で有効になっており、実行できる場合と、C のアクションが現在の状態で有効になっていないため実行できない場合です。したがって、最終状態 S _fでの有限公平な実行は、オートマトンがラウンドロビン方式ですべてのタスクに継続的に順番を与えるが、 S _fで有効になっているアクションがないため、アクションは実行されない実行として定義できます。

I/O オートマトン A の公正な実行の集合はfairexecs(A)で表されます。 β を A の公正な実行のトレースとすると、 β はA の公正なトレースになります。 A の公正なトレースの集合はfairtraces(A)で表されます。

実行例では、実行 (a) は最終状態で受信アクションが有効になっていないため公平です。実行 (b) は有限ですが、最終状態では受信アクションが有効になっています。したがって、実行 (b) は公平ではありません。実行 (c) は無限で、受信イベントが含まれず、最初のステップ以降のすべての時点で受信アクションが有効になっています。したがって、これは公平な実行ではありません。^{[1] [3]}公平性の定義には重要な特性があります。「構成の公平な実行は、コンポーネントの公平な実行の構成です」つまり、Fair(Π _i A _i )= Π _i Fair(A _i ) です。^[2]

I/O オートマトンでは、非同期システムを正確に記述できます。また、システムは何ができるかという「正確な主張」を形式化して証明するためにも使用されます。このセクションでは、いくつかの重要な特性について説明します。これらと、その他の特性および証明方法については、分散アルゴリズムで説明されています。^[1]

入力有効化プロパティは、オートマトンが入力アクションの発生をブロックできないことを示します。このプロパティを持つことの 2 つの重要な利点は次のとおりです。

1. モデルは任意の入力に対応するように設計されているため、予期しない入力の処理の失敗によるシステム エラーの主な原因が排除されます。
2. 入力を可能にするプロパティは、「外部アクションのシーケンスに基づいた、オートマトンに対する外部動作の単純な概念」を利用します。このプロパティを前提としないと、モデル内の特定の定理の証明が失敗する可能性があります。

I/O オートマトンの内部アクションはユーザーには見えません。I/O オートマトンがブラック ボックスのように見え、ユーザーには「オートマトンの実行のトレース (または公正な実行)」のみが見えます。I/O オートマトンとその証明の特定のプロパティは、通常、「トレースのプロパティまたは公正なトレース」として形式化されます。

P をトレース プロパティとします。P には次のコンポーネントがあります。

• sig(P)は内部アクションのない署名を表す
• traces(P) は、「acts(sig(P)) 内のアクションのシーケンス」のセットに対応します。このセットは無限である可能性があります。

トレース プロパティは、外部シグネチャと、そのインターフェイスで表示されるシーケンスのセット (またはプロパティ) を記述します。acts(sig(P)) は、省略表記の acts(P) で表されることがあります。I/O オートマトン A がトレース プロパティ P を満たすと述べられている場合、(少なくとも) 2 つの異なる意味が意図されている可能性があります。

1. 「extsig(A) = sig(P) かつ traces(A) ⊆ traces(P)」
2. 「extsig(A) = sig(P) かつ fairtraces(A) ⊆ traces(P)」

直感的には、A が外部動作を生成する場合、それはプロパティ P によって許可されることを意味します。ただし、A が実際に P のすべてのトレースを表す必要はありません。A は入力対応であるため、入力アクションのすべての可能なシーケンスに対して、fairtraces(A) (および traces(A)) には A による応答が含まれます。fairtraces(A) ⊆ traces (P) が成り立つ場合、プロパティ P には生成されたシーケンスがすべて含まれている必要があります。

直感的には、安全性プロパティは、何も「悪い」ことが起こらないという事実を表します。より正式には、P をトレース プロパティとします。次の基準が traces(P) に当てはまる場合、P はトレース安全性プロパティ、または安全性プロパティです。

• traces(P) は空ではありません: イベントの発生前に何か悪いことが起こることはありません。したがって、空でないことは traces(P) の合理的な条件です。
• traces(P) は「プレフィックスが閉じている」 : β ∈ traces(P) とし、β' は β の有限プレフィックスを表します。この場合、β' ∈ traces(P) です。詳しくは、何も悪いことが起こらないトレースがあると仮定します。したがって、そのトレースのどのプレフィックスでも悪いことは起こりません。したがって、プレフィックスが閉じていることは traces(P) の合理的な条件です。
• traces(P) は「極限閉」です。β 1 _、 β ₂、… が traces(P) 内の有限シーケンスの無限シーケンスを表すものとします。また、各 i について、β _{i はβ i+1} のプレフィックスであると仮定します。この場合、一意のシーケンス β、つまり「連続拡張順序付けによる β _iの極限」も traces(P) に存在します。したがって、トレース内で何か悪いことが起こった場合、それはトレース内の特定のイベントの結果です。この場合、極限閉を持つことは、traces(P) の合理的な条件です。

非公式には、活性特性は、最終的に何か「良い」ことが起こると解釈できます。したがって、ある時点までに何が起こったかに関係なく、将来のある時点で何か良いことが起こる可能性があります。より正式には、P をトレース特性とします。P はトレース活性特性、または「acts(P) 上のすべての有限シーケンスが traces(P) に何らかの拡張を持つ場合」の活性特性です。

• 時間制限付き I/O オートマトン: Merritt, Michael、Modugno, Francesmary、Tuttle, Mark R. (1991 年 8 月)。「時間制限付きオートマトン (拡張要約)」。第 2 回国際並行性理論会議の議事録。CONCUR '91。第 527 巻。408 ～ 423 ページ。
• 確率的 I/O オートマトン: Wu, Sue-Hwey; Smolka, Scott A.; Stark, Eugene W. (1997 年 4 月). 「確率的 I/O オートマトンの構成と動作」(PDF) .理論計算機科学. 176 (1–2): 1–38. doi : 10.1016/s0304-3975(97)00056-x .
• 安全性プロパティと活性プロパティ全般については、「安全性プロパティと活性プロパティ」を参照してください。

• 連続プロセスの伝達
• 俳優モデル
• 関係変換器
• 有限状態トランスデューサ