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 的八个构造器，γ=\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。

设计决策

返回第一个策略错误，列出所有策略问题

构建策略是常见情形，一条错误信息就足以修正一次调用，因此 make_execution_policy 以 Result 返回第一个问题。重新检查已存储的策略发生在工作流验证中，它一次报告所有问题，因此 validate_policy 返回全部问题。两者按同样的顺序检查同样的四个条件。

让中止式的便捷函数保持精简

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 和三个请求记录复制了 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 中的测试检查了全部八个。
  • 没有依赖。 这个包只导入 MoonBit 核心库，因此模块的依赖图保持无环。

被否决的方案

  • 每个后端一个带类型的错误。 单一的 PolicyIssue 类型让策略与后端无关；问题以数据的形式指出不受支持的后端或模式。
  • 部分函数形式的 native_status_from_code。 返回 NativeStatus? 会迫使每个调用方处理运行时将来可能新增的编码；把它们映射为 InvalidArgument 则是偏向失败的稳妥做法。
  • 在每个后端中定义整数编码。 这些编码是 C 契约的一部分，因此放在所有后端共享的包中。

边界

这个包不运行任何东西，不探测系统，不验证整数编码的请求记录，也不把状态码 88 到 1414 描述为构造器；工作流运行时以原始整数报告它们。