workflow 设计

设计目标

数据并行计划一次只覆盖一个操作。真实的程序还会派生和汇合任务、通过通道传递工作、用锁保护共享状态。workflow 包为这些提供统一的描述：一个任务图，其节点是有类型的步骤，资源是显式的能力，边决定执行顺序。图是数据，因此可以在运行时执行它之前，在任何目标上用 MoonBit 验证。

数学背景

工作流是由能力、节点和边组成的三元组 $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$ 完成后开始。

两个关系为图赋予类型。 $\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 都表示 $u$ 在 $v$ 开始前完成。种类说明边存在的原因，规范还赋予所有权转移更多含义，但 v1 对所有边一视同仁地检查和调度，因此顺序关系 $\prec$ 与种类无关。

构建方法就地修改

Workflow 把能力、节点和边存放在 Array 中，add_capability、add_node 和 add_edge 向其中追加并返回同一个工作流。这使链式构建很廉价，每步均摊 $O(1)$ ，但它不是持久化的构建器：执行 let b = a.add_node(n) 之后，a 和 b 是同一个值，都包含 n。需要两个变体的代码必须构建两个工作流。

验证是分层的

MoonBit 中的 validate 在所有目标上检查完整的数据模型：策略、能力种类和访问模式、节点和能力的引用、边的端点、计算节点的计划，以及环。原生运行时在提交工作流时会再次检查它所依赖的内容。两层在大多数规则上一致，但并非全部：

规则	`validate`	原生运行时
`RwLock`、`Semaphore` 能力	接受	拒绝（状态码 8）
作用于 `RwLock` 的 `Lock` 和 `Unlock`	接受	拒绝
访问模式、重复 id、计算计划	检查	不检查
环	部分（见下文）	完整（状态码 9）

MoonBit 层报告每个问题，让用户一次看到所有问题；原生层在遇到第一个问题时就停止，因为它只需决定是否启动。

MoonBit 的环检查是部分的

在以下情况下 validate 报告 CyclicDependency：(a) 图中有节点，但没有一个节点没有入边；或 (b) 同一对节点之间有两条方向相反的边。当每条边都连接存在的节点时，这两个条件都意味着存在环：

(b) 是长度为二的环。
对于 (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 没有返回问题，则工作流在上述意义下是良构的，只可能存在一个从源节点可达、长度为三或以上的环。
拒绝的可靠性。 每个问题都指出一个真实的违规，唯一的例外是来自未知节点的边所引起的 CyclicDependency。
提交。 当且仅当 validate(w) 为空且 backend 为 Native 时，submit(w, backend) 被接受；它从不设置 completed。
复杂度。 validate 的运行时间为 $O(|V|^2 + |C|^2 + |E|^2 + |V| \cdot |C| + |V| \cdot |E|)$ ：重复检测对每个元素过滤整个数组，端点和入度查找会扫描节点和边数组，反向边测试比较所有边对。

被否决的方案

把能力嵌入节点。 存放在每个 Send 节点内部的通道无法与对应的 Recv 共享。
调度方式各异的带类型边。 为每种边规定各自的调度规则，会让顺序关系依赖于运行时策略；v1 只保留一条规则。
持久化构建器。 每次 add_* 都复制数组，会为了保留旧版本的便利而让构建变成二次复杂度。
在 MoonBit 中完整检测环。 在 validate 中做拓扑排序可以弥补上述缺口；当前的检查更廉价，剩下的情形由原生运行时捕获。这个缺口是一个待修复的候选项。

边界

这个包不调度或执行工作流，不在节点之间移动数据，不检查阻塞节点是否配对（即某个 Recv 是否有先运行的 Send），不检测死锁，也不赋予不同种类的边不同的含义。