レオ調整言語

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}$すべてのチャネルにタイプを割り当てます。

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

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

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

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

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

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

歴史的に、Reo の最初の意味論は、ストリーム (つまり、無限シーケンス) の共​​代数的概念に基づいていました。 ^{[ 5 ]}この意味論は、データ項目のストリームと単調増加するタイムスタンプ (実数) のストリームからなるペアである、時間付きデータ ストリーム の概念に基づいています。すべてのノードをこのような時間付きデータ ストリームに関連付けることで、チャネルの動作を、接続されたノード上のストリームの関係としてモデル化できます。

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

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

^{Reoの他の意味論では、時間付き[ 8 ]}または確率的^{[ 9 ]}動作をモデル化することが可能になります。

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

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

• Reoウェブサイト