workflow の設計

設計の目標

データ並列のプランが扱うのは一度に 1 つの操作です。実際のプログラムはタスクをスポーンしてジョインし、チャネルで作業を受け渡し、ロックで共有状態を守ります。workflow パッケージはこれらを 1 つの記述にまとめます。ノードは型付きのステップ、資源は明示的なケイパビリティ、エッジは実行順序を決めるタスクグラフです。グラフはデータなので、ランタイムが実行する前に、どのターゲットでも MoonBit で検証できます。

数学的背景

ワークフローはケイパビリティ、ノード、エッジの 3 つ組 $W = (C, V, E)$ です。

• 各ケイパビリティ $\kappa \in C$ は id、種類 $k(\kappa) \in K$、アクセスモード $a(\kappa) \in M$ を持ちます。
• 各ノード $v \in V$ は id、種類 $t(v) \in T$、省略可能なケイパビリティ $\operatorname{cap}(v)$ を持ちます。
• 各エッジ $(u, v) \in E$ は、$v$ が $u$ の完了後にしか開始できないことを表します。

2 つの関係がグラフに型を与えます。$\mathrm{Acc} \subseteq K \times M$ は各ケイパビリティ種類の有効なアクセスモードを、$\mathrm{Use} \subseteq T \times K$ は各ノード種類が使えるケイパビリティ種類を挙げます（どちらの表も workflow API にあります）。id が一意で、エッジが存在する異なるノードを結び、さらに次が成り立つとき、ワークフローは整形式です。

$$\forall \kappa \in C:\ (k(\kappa), a(\kappa)) \in \mathrm{Acc}, \qquad \forall v \in V \text{ that needs one}:\ (t(v), k(\operatorname{cap}(v))) \in \mathrm{Use}.$$

エッジは関係 $u \prec v$、すなわち「$u$ から $v$ への経路がある」を定めます。実行順序とは、$u \prec v$ のときは必ず $u$ が $v$ より前に来るようなすべてのノードの列で、トポロジカル順序と呼びます。そのような順序が存在するのは $(V, E)$ に有向閉路がないときに限ります。閉路 $v_0 \to \dots \to v_m = v_0$ があれば $v_0$ が自分より前に来る必要があり、逆に Kahn のアルゴリズムは入ってくるエッジのないノードを繰り返し取り除くことで、どの非巡回グラフにも順序を作ります。

設計上の決定

ケイパビリティは宣言し、ノードは id で参照する

同期のための資源は、それを使うステップとは独立に存在します。送信するノードと受信するノードは同じチャネルについて合意しなければなりません。ケイパビリティを一度だけ宣言して id で参照すれば、その合意は明示的で検査可能になり、ランタイムには確保すべき資源の詰まった表が手に入ります。アクセスモードは、チャネルの MoveOnly や共有ビューの ReadOnly のように宣言の意図を記録するので、validate は読み取り専用バッファに対する WriteShared ノードを拒否できます。

どの種類のエッジも同じように順序付ける

DataDependency、ControlDependency、OwnershipTransfer、SynchronizationDependency はいずれも、$v$ が始まる前に $u$ が完了することを意味します。種類はエッジが存在する理由を記録し、仕様は所有権の移転にさらに意味を与えていますが、v1 はすべてのエッジを同じように検査しスケジュールするので、順序関係 $\prec$ は種類によりません。

ビルダーはその場で変更する

Workflow はケイパビリティ、ノード、エッジを Array に保持し、add_capability、add_node、add_edge はそこに追加して同じワークフローを返します。これで連鎖的な構築は 1 ステップあたり償却 $O(1)$ と安価になりますが、永続的なビルダーではありません。let b = a.add_node(n) の後、a と b は同じ値で、どちらも n を含みます。2 つの版が必要なコードは 2 つのワークフローを作らなければなりません。

検証は階層的

MoonBit の validate は、すべてのターゲットでデータモデル全体を検査します。ポリシー、ケイパビリティの種類とアクセスモード、ノードとケイパビリティの参照、エッジの端点、計算ノードのプラン、そして閉路です。ネイティブランタイムは、ワークフローの投入時に自分が依存するものを再び検査します。2 つの層はほとんどの規則で一致しますが、すべてではありません。

規則	validate	ネイティブランタイム
RwLock、Semaphore のケイパビリティ	受け付ける	拒否（ステータス 8）
RwLock に対する Lock と Unlock	受け付ける	拒否
アクセスモード、重複 id、計算プラン	検査する	検査しない
閉路	部分的（下記）	完全（ステータス 9）

MoonBit の層はすべての問題を報告するので、ユーザーは問題を一度に見られます。ネイティブの層は開始するかどうかを決めるだけなので、最初の問題で止まります。

MoonBit の閉路検査は部分的

validate が CyclicDependency を報告するのは、(a) グラフにノードがあるのに入ってくるエッジのないノードが 1 つもないとき、または (b) 同じ 2 ノードの間に逆向きのエッジが 2 本あるときです。どのエッジも存在するノードを結ぶなら、どちらの条件も閉路があることを意味します。

• (b) は長さ 2 の閉路です。
• (a) では、任意のノードから入ってくるエッジを逆向きにたどります。どのノードにも入ってくるエッジがあるのでたどりは止まらず、ノードは $|V|$ 個なので $|V| + 1$ ステップ以内に同じノードを再び通り、その繰り返し部分が閉路になります。

逆は成り立ちません。$1 \to 2 \to 3 \to 4 \to 2$ では、ノード $1$ に入ってくるエッジがなく、逆向きのエッジの組もないので、$2 \to 3 \to 4 \to 2$ が閉路であるにもかかわらず validate は何も報告しません。ネイティブランタイムは Kahn のアルゴリズムを実行し、$1$ を取り除いた後 $\{2, 3, 4\}$ から取り除けるノードが見つからず、グラフを拒否します。また、未知のノードからのエッジも (a) では入ってくるエッジに数えられるので、入ってくるエッジがすべて未知の id から来るグラフには、InvalidNodeReference の問題と並んで CyclicDependency が報告されます。

正しさ / 不変条件

• 受理の健全性。 validate が問題を返さなければ、ワークフローは上の意味で整形式です。ただし、ソースから到達できる長さ 3 以上の閉路がある可能性は残ります。
• 拒否の健全性。 どの問題も実際の違反を示します。例外は、未知のノードからのエッジによる CyclicDependency だけです。
• 投入。 submit(w, backend) が受理されるのは、validate(w) が空で backend が Native のときに限ります。completed は決して設定しません。
• 計算量。 validate の実行時間は $O(|V|^2 + |C|^2 + |E|^2 + |V| \cdot |C| + |V| \cdot |E|)$ です。重複の検出は要素ごとに配列全体を絞り込み、端点と入次数の検索はノードとエッジの配列を走査し、逆向きエッジの判定はエッジのすべての組を比べます。

採用しなかった案

• ケイパビリティをノードに埋め込む。 各 Send ノードの中に置いたチャネルは、対応する Recv と共有できません。
• スケジューリングの異なる型付きエッジ。 エッジの種類ごとに独自のスケジューリング規則を与えると、順序関係がランタイムのポリシーに依存してしまいます。v1 は規則を 1 つに保っています。
• 永続的なビルダー。 add_* のたびに配列をコピーすると、古い版を残せる便利さと引き換えに構築が 2 乗の計算量になります。
• MoonBit で閉路を完全に検出する。 validate でトポロジカルソートを行えば上で述べた穴はふさがります。現在の検査のほうが安価で、残りの場合はネイティブランタイムが捕まえます。この穴は修正の候補です。

境界

このパッケージはワークフローをスケジュールも実行もせず、ノード間でデータを移動せず、ブロックするノードが対になっているか（Recv の前に実行される Send があるか）を検査せず、デッドロックを検出せず、エッジの種類ごとに異なる意味を与えません。