レオ調整言語

Reo回路：オルタネーター

Reo ^{[ 1 ] [ 2 ]}は、個々のプロセスを広い意味で完全なシステムに構成する調整プロトコルのプログラミングと分析を行うドメイン固有言語です。Reo で構成できるシステムのクラスの例としては、コンポーネントベースシステム、サービス指向システム、マルチスレッドシステム、生物学的システム、暗号化プロトコルなどがあります。Reo はグラフィカル構文を持ち、コネクタまたは回路と呼ばれるすべての Reo プログラムは、ラベル付きの有向ハイパーグラフです。このようなグラフは、システム内のプロセス間のデータフローを表します。Reo には形式意味論があり、これはさまざまな形式検証手法とコンパイルツールの基礎となっています。

定義

Reo では、並行システムは、コンポーネント間のデータフローを可能にする回路によって相互に接続された複数のコンポーネントで構成されます。コンポーネントは、接続されている回路の境界ノードに対して I/O 操作を実行できます。I/O 操作には 2 種類あります。put 要求はノードにデータ項目をディスパッチし、get 要求はノードからデータ項目を取得します。すべての I/O 操作はブロッキングです。つまり、コンポーネントは、保留中の I/O 操作が正常に処理された後にのみ処理を続行できます。

右上の図は、3つのコンポーネント（左側に2つの生産者、右側に1つの消費者）で構成される生産者・消費者システムの例を示しています。中央の回路はプロトコルを定義しており、生産者はデータを同期的に送信し、消費者はそれらのデータを交互に受信します。

正式には、回路の構造は次のように定義されます。

定義 1.回路は次の三つ組から成ります。 ${\displaystyle R=(N,B,C,t)}$

1. Nはノードの集合です。
2. ${\displaystyle B\subseteq N}$ 境界ノードの集合です。
3. ${\displaystyle C\subseteq 2^{N}\times 2^{N}}$ チャネルのセットです。
4. ${\displaystyle t:C\rightarrow T}$ 各チャネルにタイプを割り当てます。

となる。 がチャネルである場合、Iはcの入力ノードの集合と呼ばれ、Oはcの出力ノードの集合と呼ばれる 。 ${\displaystyle |I\cup O|=2}$ ${\displaystyle (I,O)\in C}$ ${\displaystyle c=(I,O)\in C}$

回路のダイナミクスは、電子回路を通る信号の流れに似ています。

ノードは固定のマージャー・レプリケータ動作を持つ。つまり、入力チャネルの1つからのデータは、データの保存や変更なしに、すべての出力チャネルに伝播される（レプリケータ動作）。複数の入力チャネルからデータが提供される場合、ノードはそれらの中から非決定論的に選択を行う（マージャー動作）。入力チャネルのみ、または出力チャネルのみを持つノードは、それぞれシンクノードまたはソースノードと呼ばれる。入力チャネルと出力チャネルの両方を持つノードは、混合ノードと呼ばれる。

ノードとは対照的に、チャネルはタイプによって表現されるユーザー定義の動作を持ちます。つまり、チャネルはそこを通過するデータ項目を保存したり変更したりできます。すべてのチャネルは正確に2つのノードを接続しますが、これらのノードは必ずしも入力と出力である必要はありません。例えば、右上の図の縦方向のチャネルには2つの入力があり、出力はありません。チャネルのタイプは、データに対するチャネルの動作を定義します。以下に一般的なタイプを示します。

• 同期: 入力ノードからデータをアトミックに取得し、出力ノードに伝播します。
• LossySync : Sync と同じですが、出力ノードがデータを受け取る準備ができていない場合にデータが失われる可能性があります。
• Fifo ⟨ n ⟩ : 入力ノードからデータを取得し、サイズnの内部バッファに一時的に格納し、出力ノードに伝播します（この出力ノードがデータを受け取る準備ができたとき）。
• SyncDrain : 両方の入力ノードからデータをアトミックに取得し、それを失います。
• フィルター⟨ c ⟩ : フィルター条件cが満たされる場合は、入力ノードからデータをアトミックに取得し、出力ノードに伝播します。それ以外の場合は、データを失います。

ソフトウェアエンジニアリングの特性

外生性

調整言語を分類する方法の 1 つは、その場所によって分類することです。調整の場所とは、調整活動が行われる場所を指し、調整モデルと言語を内生的または外生的として分類します。^{[ 3 ]} Linda などの内生的モデルと言語は、計算の調整のために組み込む必要があるプリミティブを提供します。このようなモデルを使用するアプリケーションでは、各モジュールの調整に影響するプリミティブは、モジュール自体の中にあります。対照的に、Reo は、エンティティの調整を外部からサポートするプリミティブを提供する外生的言語です。外生的モデルを使用するアプリケーションでは、各モジュールの調整に影響するプリミティブは、モジュール自体の外部にあります。

特定のアプリケーションにおいては、内生的モデルの方が自然な場合もあります。しかし、内生的モデルは一般的に、調整プリミティブと計算コードの混在を招き、計算のセマンティクスと調整プロトコルが絡み合うことになります。この混在により、通信／調整プリミティブがソースコード全体に散在し、アプリケーションの協力モデルと調整プロトコルが曖昧で暗黙的なものになります。一般的に、アプリケーションの協力モデルまたは調整プロトコルとして識別可能なソースコードは存在せず、アプリケーションコードの他の部分から独立して設計、開発、デバッグ、保守、再利用することはできません。一方、外生的モデルは、調整対象の計算モジュールとは独立して、調整モジュールの開発を促進します。その結果、アプリケーションの調整コンポーネントの設計と開発に多大な労力が費やされた結果、より理解しやすく、他のアプリケーションでも再利用できる、具体的な「純粋なコーディネーターモジュール」が生まれる可能性があります。

構成性/再利用性

Reo回路は合成可能です。つまり、より単純な回路を再利用することで複雑な回路を構築できます。より具体的には、2つの回路を境界ノードで結合して、新しいジョイント回路を形成できます。他の多くの並行性モデル（例えば、π計算）とは異なり、Reo回路は合成時に同期性が維持されます。つまり、ノードAとBの間に同期フローを持つ回路と、ノードBとCの間に同期フローを持つ別の回路を合成すると、ジョイント回路はノードAとCの間に同期フローを持つことになります。言い換えれば、2つの同期回路を合成すると、同期回路が生​​成されます。

セマンティクス

Reo回路のセマンティクスは、その動作の形式的な記述である。Reoには様々なセマンティクスが存在する。^{[ 4 ]}

歴史的に、Reoの最初のセマンティクスは、コジェネリックなストリーム（すなわち無限シーケンス）の概念に基づいていました。^{[ 5 ]}このセマンティクスは、時間付きデータストリーム の概念に基づいています。これは、データ項目のストリームと単調に増加するタイムスタンプ（実数）のストリームからなるペアです。すべてのノードをこのような時間付きデータストリームに関連付けることで、チャネルの振る舞いを、接続されたノード上のストリームの関係としてモデル化できます。

その後、オートマトンベースの意味論が開発され、制約オートマトンと呼ばれるようになりました。^{[ 6 ]} 制約オートマトンとは、ラベル付きの遷移システムであり、遷移ラベルは同期制約とデータ制約で構成されます。同期制約は、遷移によってモデル化された実行ステップでどのノードが同期するかを指定し、データ制約は、これらのノードにどのデータ項目が流れるかを指定します。

制約オートマトン（および時間指定データストリーム）の限界の一つは、チャネルの挙動が保留中のI/O操作の可用性（または非可用性）に依存するような、コンテキスト依存の挙動を直接モデル化できないことです。例えば、制約オートマトンでは、出力ノードに保留中のget要求がない場合にのみデータを失うはずのLossySyncの挙動を直接モデル化することはできません。この問題を解決するために、Reoの別のセマンティクスであるコネクタカラーリングが開発されました。^{[ 7 ]}

^{Reoの他のセマンティクスにより、時間[ 8 ]}または確率^{[ 9 ]}の動作をモデル化することが可能になります。

実装

Extensible Coordination Tools (ECT) は、Reo の統合開発環境(IDE)を構成するEclipseのプラグイン セットです。ECT は、回路を描画するためのグラフィカル エディターと、回路内のデータフローをアニメーション化するアニメーション エンジンで構成されています。コード生成用に、ECT には Reo から Java へのコンパイラーが含まれており、制約オートマトンの意味に基づいて回路のコードを生成します。特に、Reo 回路を入力すると、回路をモデル化する制約オートマトンをシミュレートする Java クラスが生成されます。検証用に、ECT には Reo 回路をmCRL2のプロセス定義に変換するツールが含まれています。ユーザーはその後、mCRL2 を使用して、μ 計算プロパティ仕様に対するモデル チェックを行うことができます。(あるいは、Vereofy モデル チェッカーも Reo 回路の検証をサポートしています。)

Reoの別の実装はScalaプログラミング言語で開発されており、分散形式で回路を実行します。^{[ 10 ]}

参考文献

1. Farhad Arbab: Reo: コンポーネント構成のためのチャネルベースの調整モデル. コンピュータサイエンスにおける数学的構造 14(3):329--366, 2004.
2. Farhad Arbab: Puff, The Magic Protocol . Gul Agha, Olivier Danvy, Jose Meseguer編, Talcott Festschrift, LNCS第7000巻, 169-206ページ. Springer, 2011.
3. Farhad Arbab:相互作用計算の構成. Dina Goldin、Scott Smolka、Peter Wegner編『Interactive Computation』277-321ページ. Springer、2006年.
4. Sung-Shik JongmansとFarhad Arbab：「 Reoのための30の意味形式主義の概要」。Scientific Annals of Computer Science 22(1):201-251, 2012。
5. Farhad ArbabとJan Rutten：「成分コネクタの共帰的計算」。Martin Wirsing、Dirk Pattinson、Rolf Hennicker編、『WADT 2002 Proceedings of WADT 2002』、LNCS第2755巻、34～55ページ。Springer、2003年。
6. Christel Baier、Marjan Sirjani、Farhad Arbab、Jan Rutten：「制約オートマトンによるReoのコンポーネントコネクタのモデリング」『コンピュータプログラミングの科学』61(2):75-113、2006年。
7. Dave Clarke、David Costa、Farhad Arbab：「コネクタカラーリングI：同期とコンテキスト依存性」『コンピュータプログラミングの科学』66(3):205-225、2007年。
8. Farhad Arbab, Christel Baier , Frank de Boer, Jan Rutten: Timed Component Connectors のモデルと時間的論理仕様. Software and Systems Modeling 6(1):59-82, 2007.
9. Christel Baier：「Reoコネクタ回路の確率モデル」Journal of Universal Computer Science 11(10):1718-1748, 2005年。
10. José Proença:分散コンポーネントの同期調整。ライデン大学博士論文、2011年。

外部リンク

• レオのウェブサイト