Luna Flow
日本語

shared の設計

設計の目標

luna_thread のどのパッケージも、どのバックエンド、どのモード、何個のワーカー、どの順序を意味するかを表す必要があり、どのバックエンドも C ランタイムの整数コードを扱う必要があります。shared はそれらを定義する唯一の場所で、plan、workflow、各バックエンドが互いに依存せずに合意できるようにしています。自身は依存を持たず、すべてのターゲットでビルドできます。

数学的背景

細分化された直積としてのポリシー

実行ポリシーは次の直積の元です。

P=B×D×Z×Z×O,P = B \times D \times \mathbb{Z} \times \mathbb{Z} \times O ,

バックエンド、モード、ワーカー数、チャンクサイズ、順序です。v1 のランタイムが受け付けるのは次の部分集合です。

P1={ (b,d,w,c,o)∈P∣w>0, c>0, b=Native, d=Synchronous }.P_1 = \{\, (b, d, w, c, o) \in P \mid w > 0,\ c > 0,\ b = \mathrm{Native},\ d = \mathrm{Synchronous} \,\} .

make_execution_policy は部分的なコンストラクタ P⇀P1P \rightharpoonup P_1 です。引数が P1P_1 に属していればそれを返し、そうでなければ挙げた順序で最初に破られた条件を返します。validate_policy は破られたすべての条件のリストを返すので、

p∈P1  ⟺  validate_policy⁡(p)=[ ].p \in P_1 \iff \operatorname{validate\_policy}(p) = [\,] .

切断と引き込みとしてのステータスコード

SS を NativeStatus の 8 つのコンストラクタとし、γ=\gamma = native_status_code :S→Z: S \to \mathbb{Z} がそれらに 00 から 77 の番号を付けるとします。ρ=\rho = native_status_from_code :Z→S: \mathbb{Z} \to S は {0,…,7}\{0, \dots, 7\} 上で γ\gamma の逆になり、ほかの整数をすべて InvalidArgument に写すとします。すると

ρ∘γ=idS,\rho \circ \gamma = \mathrm{id}_S ,

なので γ\gamma は単射（切断）、ρ\rho は全射（引き込み）です。もう一方の合成は γ\gamma の像の上でだけ恒等写像になります。

(γ∘ρ)(m)={m0≤m≤7,1otherwise.(\gamma \circ \rho)(m) = \begin{cases} m & 0 \le m \le 7, \\ 1 & \text{otherwise.} \end{cases}

したがって C のステータスを NativeStatus に変換して戻すと、コード 00 から 77 は保たれ、ワークフローのステータス 88 から 1414 は 11 につぶれます。

設計上の決定

ポリシーのエラーは最初の 1 つを返し、問題はすべて列挙する

ポリシーを作るのはよくある場面で、呼び出しを直すにはエラーメッセージが 1 つあれば足りるので、make_execution_policy は最初の問題を Result で返します。保存されたポリシーの再検査はすべてを一度に報告するワークフロー検証の中で行われるので、validate_policy はすべての問題を返します。どちらも同じ 4 つの条件を同じ順序で検査します。

中断する便利関数は最小限に

ExecutionPolicy::new、native_policy、javascript_policy は make_execution_policy の結果を unwrap します。ネイティブの既定値では失敗しません。JavaScript バックエンドでは v1 では必ず失敗するので javascript_policy は中断します。これは計画中の JavaScript バックエンド向けに書いたコードが今でもコンパイルできるように存在しています。ユーザーからポリシーの引数を受け取るコードは make_execution_policy を呼んでください。

ケイパビリティは調べるのではなく宣言する

RuntimeCapabilities::for_backend は固定の表を返します。実行中のシステムを調べるにはネイティブバックエンドが必要ですが、shared はそれに依存してはならず、しかも結果は moon のビルドと CMake のビルドで異なります。表は各バックエンドが意図しているケイパビリティを述べ、現在の実装が実際に何をするかは各バックエンドのページに書かれています。

C 構造体の整数コードによる写し

NativeBuffer と 3 つのリクエストレコードは、luna_thread_runtime.h にある C 構造体のフィールド順と整数コードを写しており、バインディングは backend/native の型付きレコードを知らなくてもそれらを埋められます。仕様はこの対応を ABI レイアウト同型と呼んでいます。レコードは値を検査せずに保存し、検査はそれを送るバックエンドの役目です。

正しさ / 不変条件

  • ポリシーの部分集合。 make_execution_policy、ExecutionPolicy::new、native_policy が返すポリシーはすべて P1P_1 に属します。
  • ステータスの往復。 上で導いたとおり、すべての NativeStatus ss について ρ(γ(s))=s\rho(\gamma(s)) = s です。shared API のテストが 8 つすべてを検査しています。
  • 依存なし。 このパッケージは MoonBit のコアライブラリしかインポートしないので、モジュールの依存グラフは非巡回のままです。

採用しなかった案

  • バックエンドごとの型付きエラー。 1 つの PolicyIssue 型にすればポリシーはバックエンドに依存しません。問題は、サポートされないバックエンドやモードをデータとして示します。
  • 部分関数の native_status_from_code。 NativeStatus? を返すと、ランタイムが将来加えるかもしれないコードの処理をすべての呼び出し側に強いることになります。それらを InvalidArgument に写すのは、失敗の側に倒す安全策です。
  • 整数コードを各バックエンドで定義する。 コードは C の契約の一部なので、すべてのバックエンドが共有するパッケージに置きます。

境界

このパッケージは何も実行せず、システムを調べず、整数コードのリクエストレコードを検証せず、ステータス 88 から 1414 をコンストラクタとして記述しません。ワークフローランタイムはそれらを生の整数で報告します。