backend/native 设计

设计目标

backend/native 是 luna_thread 真正并行运行代码的地方。它有两项工作：在不复制 MoonBit 数组的前提下对其运行数据并行的整数内核，以及在真实线程上运行工作流图的同步协议。两者都用 C 实现，隐藏在由整数和借用数组构成的窄接口之后，以便同一个运行时将来也能服务于 JavaScript 插件。

本页描述 native/src/runtime.c 和桥接层 ffi_runtime_bridge.c 中实际实现的线程模型、内存模型以及内核背后的数学。

数学背景

分块求值

设输入为 $x = (x_0, \dots, x_{n-1})$ ，工作线程数为 $w$ ，块大小为 $c$ ，且 $0 < w \le n$ 、 $0 < c \le n$ 。运行时要求满足覆盖条件

w \ge k, \qquad k = \left\lceil \frac{n}{c} \right\rceil ,

这样每个块都能分到一个工作线程；然后把 $[0, n)$ 分成 $k$ 个连续的块 $[s_j, s_{j+1})$ ，其中

s_0 = 0, \qquad s_{j+1} = s_j + \left\lceil \frac{n - s_j}{k - j} \right\rceil .

块大小。 每个块有 $\lfloor n/k \rfloor$ 或 $\lceil n/k \rceil$ 个元素，因此至多 $c$ 个：

\begin{aligned} k \ge \frac{n}{c} &\;\Longrightarrow\; \frac{n}{k} \le c \;\Longrightarrow\; \left\lceil \frac{n}{k} \right\rceil \le c && \text{since } c \in \mathbb{Z}. \end{aligned}

第一个结论是常见的均衡划分论证：若剩余的 $r = n - s_j$ 个元素和 $m = k - j$ 个块满足 $m \lfloor n/k \rfloor \le r \le m \lceil n/k \rceil$ ，则 $\lceil r/m \rceil$ 介于 $\lfloor n/k \rfloor$ 与 $\lceil n/k \rceil$ 之间，并且对 $r - \lceil r/m \rceil$ 和 $m - 1$ 该不等式再次成立。在 $j = 0$ 时， $r = n$ 、 $m = k$ ，不等式成立。¹1 代码把块数计算为 $\min(k, w)$ ，在覆盖条件下它等于 $k$ 。若没有该条件，块会大于 $c$ ，因此运行时直接拒绝。

作为幺半群折叠的归约

归约用一个满足结合律的运算 $\oplus$ 合并各元素：

\operatorname{reduce}(x) = x_0 \oplus x_1 \oplus \dots \oplus x_{n-1}.

整数上的求和、最小值和最大值都满足结合律和交换律。正是结合律保证了分块的正确性：设各块的结果为 $P_j = x_{s_j} \oplus \dots \oplus x_{s_{j+1}-1}$ ，

P_0 \oplus P_1 \oplus \dots \oplus P_{k-1} = x_0 \oplus x_1 \oplus \dots \oplus x_{n-1}

这由广义结合律保证，与 $w$ 和 $c$ 无关。最小值和最大值以每个块的第一个元素作为初值，因此只需要半群；这也是运行时要求 $n > 0$ 的原因之一。

分块前缀和

扫描分三个阶段计算包含式前缀和 $y_i = \sum_{t=0}^{i} x_t$ 。记 $S_j$ 为块 $j$ 的和：

并行地，每个块计算其局部前缀和 $L_j(i) = \sum_{t=s_j}^{i} x_t$ （ $s_j \le i < s_{j+1}$ ）并写入输出，同时得到块总和 $S_j = L_j(s_{j+1} - 1)$ 。
顺序地计算进位 $C_0 = 0$ 和 $C_j = C_{j-1} + S_{j-1}$ 。
并行地，每个块加上自己的进位： $y_i = C_j + L_j(i)$ 。

第 3 阶段之所以正确，是因为对 $j$ 归纳可得 $C_j = \sum_{t=0}^{s_j - 1} x_t$ ：

\begin{aligned} C_{j+1} = C_j + S_j &= \sum_{t=0}^{s_j - 1} x_t + \sum_{t=s_j}^{s_{j+1} - 1} x_t = \sum_{t=0}^{s_{j+1} - 1} x_t, \\ C_j + L_j(i) &= \sum_{t=0}^{s_j - 1} x_t + \sum_{t=s_j}^{i} x_t = \sum_{t=0}^{i} x_t = y_i . \end{aligned}

扫描共做 $2n + k$ 次加法；使用 $k$ 个工作线程时，其关键路径为 $O(n/k + k)$ ，而顺序循环为 $O(n)$ 。

设计决策

带检查的整数运算

内核在 $\mathbb{Z}/2^{32}$ 和 $\mathbb{Z}/2^{64}$ 上工作，其中 + 会回绕。运行时却把它们当作整数对待，拒绝返回回绕后的值：每次加法 $a + b$ 在执行前都会检查，

b > 0 \wedge a > \mathrm{MAX} - b \quad\text{or}\quad b < 0 \wedge a < \mathrm{MIN} - b \;\Longrightarrow\; \text{overflow},

而这些检查本身不会溢出。映射内核（ $x \mapsto 2x$ ）先用一次并行扫描检查所有元素，只有在没有溢出时才写入，因此失败时输出保持不变。

其结果是成功的结果都是精确的：每一次执行过的机器加法，其真实结果都在范围内，因此等于整数加法；归纳可知，返回的和或前缀等于 $\mathbb{Z}$ 中的 $\sum x_t$ 。

代价是带检查的加法是一个部分运算，并且不满足结合律：某个部分和是否越界取决于括号方式。取 $x = (-1, 0, \mathrm{MAX}, 1)$ ：

\begin{aligned} k = 1:&\quad ((-1 + 0) + \mathrm{MAX}) + 1 = \mathrm{MAX} && \text{succeeds}, \\ k = 2:&\quad (-1 + 0) + (\mathrm{MAX} + 1) && \text{fails in the second chunk}. \end{aligned}

因此结果的值与 $w$ 和 $c$ 无关，但被接受的输入集合与它们有关。另一种选择是回绕运算，它会让每个结果都有定义且与分块无关，但作为整数却是悄无声息的错误；运行时选择了精确性。

C 中的固定内核

计划可以指定 Map 和归约内核，但 MoonBit 闭包无法跨越 C 接口在 C 线程上运行。因此运行时在 C 中实现了一组固定的内核：针对 32 位和 64 位整数的翻倍、求和、最小值、最大值和前缀和。门面包装了 32 位的翻倍、求和与前缀和；其余的可通过 ffi_* 声明使用。

借用数组，调用方分配输出

MoonBit 一侧以 #borrow 把 FixedArray 的数据传给 C：C 就地读取输入、写入输出，不获取所有权，因此不复制数据，也不改变引用计数。带类型的包装在调用前用 FixedArray::make 分配输出。归约直接返回值；桥接层传入一个栈变量作为单元素输出。

工作流使用单一调度锁

工作流运行时把所有调度状态（就绪队列、依赖计数器、通道槽位、互斥标志和屏障计数器）放在同一个 pthread_mutex_t 之下，工作线程在持有该锁时执行每个节点。这样无需按能力加锁，每个节点步骤相对于其他步骤都是原子的；代价是非计算节点永远不会同时运行，不过它们都是常数时间的簿记步骤。

线程模型

内核

当运行时以 OpenMP 编译时，每个内核把块循环作为带 num_threads(w) 的 OpenMP parallel for 运行，每个块一次迭代。没有 OpenMP 时这些 pragma 被忽略，select_thread_count 返回 $1$ ，于是同样的块在调用线程上依次运行。moon 构建在编译原生桩时不带 OpenMP 选项，因此从 MoonBit 调用时内核目前是顺序运行的；native/ 的 CMake 构建会启用 OpenMP。由于两种构建的分块相同，结果和溢出行为也相同。

工作流

submit_workflow_async 启动 $w + 1$ 个 POSIX 线程： $w$ 个工作线程和一个计算通道。调度就是由线程池执行的 Kahn 拓扑排序：

每个节点 $v$ 有一个未完成前驱的计数器，初值为其入度。计数器为 $0$ 的节点进入容量为 $|V|$ 的 FIFO 环形缓冲区。
工作线程在调度器的条件变量上等待，直到队列非空，然后取出一个节点并执行它。完成一个节点会使其后继的计数器减一，并把减到 $0$ 的后继放入队列。
计算节点被交给计算通道，工作线程等待它完成。在 v1 中，计算通道只检查节点种类并报告成功；计划并不会被执行。
所有 $|V|$ 个节点完成后状态变为 Completed；第一个失败的节点设置 Failed、其状态码和 failed_node_id。两种情况都会唤醒所有等待的线程，使线程池关闭。

没有每线程队列，也没有工作窃取：所有工作线程共享一个队列，FIFO 顺序加上持锁执行，使就绪节点的运行顺序就是它们就绪的顺序。

节点语义

节点	执行时的效果
`Spawn`, `Join`, `ReadShared`, `WriteShared`	立即完成；不移动任何数据。
`Send`	若通道槽位已满则阻塞，否则填满它。
`Recv`	若槽位为空则阻塞，否则清空它。
`Lock`	若互斥标志已设置则阻塞，否则设置它。
`Unlock`	若标志未设置则以状态码 12 失败，否则清除它。
`Wait`	阻塞，直到同一条件变量上的某个 `Signal` 唤醒它。
`Signal`	唤醒一个阻塞的 `Wait`（如果有的话）；否则该信号丢失。
`Barrier`	阻塞，直到其组内的所有屏障节点都已到达。

通道是容量为一的槽位，能力不携带任何负载：运行时强制执行的是协议，而不是数据的传递。

屏障的组是具有相同能力和相同深度 $d(v)$ 的 Barrier 节点集合，其中 $d(v)$ 是从某个源节点到 $v$ 的最长路径长度：

d(v) = \max\bigl(\{0\} \cup \{\, d(u) + 1 \mid (u, v) \in E \,\}\bigr).

运行时对所有边做 $|V|$ 轮松弛来计算 $d$ ；这已足够，因为无环图中的最长路径至多有 $|V| - 1$ 条边。少于两个节点的组以状态码 14（BARRIER_BROKEN）失败。

内存模型

对内核而言，各块划分了 $[0, n)$ ，在每个并行阶段中，迭代 $j$ 只写 $[s_j, s_{j+1})$ 内的输出下标以及它自己的 partials[j] 或 summaries[j] 单元。因此不同迭代写入互不相交的位置，不存在数据竞争。OpenMP parallel for 的结尾是一个屏障，所以顺序的进位阶段能看到第一阶段的所有写入，第三阶段能看到进位。MoonBit 调用方在整个调用期间被阻塞，因此 C 线程运行时没有 MoonBit 代码接触这些数组；而且由于调用方仍持有借用的数组，它们会一直存活。

对工作流而言，所有对共享调度状态的访问都在调度器互斥锁之下进行，条件变量等待返回时会重新获取该锁，因此所有这类访问都是有序的。poll_workflow 获取同一个互斥锁来复制一致的快照。

正确性 / 不变量

内核结果。 内核成功时，翻倍后的值、和以及前缀和都等于它们在 $\mathbb{Z}$ 中的值，与 $w$ 和 $c$ 无关，如上文所推导。
先验证再工作。 每个内核在分配或计算之前都会检查空指针、正的大小、 $w \le n$ 、 $c \le n$ 、缓冲区长度以及覆盖条件，否则返回状态码 1（空指针时为 7）。
工作流准入。 在启动线程之前，运行时要求：工作线程数和节点数为正；需要能力的节点有种类匹配的能力；没有 RwLock、Semaphore 或 Opaque 能力；没有自环边；边的端点存在；并且图无环。无环性用 Kahn 算法完整检查：有限图无环，当且仅当反复删除没有入边的节点能删掉全部节点。
终止性。 若没有任何 Send、Recv 或 Lock 节点阻塞，每个 Wait 在阻塞后都会被唤醒，且每个屏障组至少有两个节点，则每个节点恰好完成一次，工作流到达 Completed 或 Failed。

已知缺陷

当前分支的这些行为与代码的意图相悖，已记录待修复：

请求的生命周期。 luna_mbt_workflow_submit_async 在自己的栈上构建请求，并在运行时启动后立即释放能力、节点和边数组，但工作线程仍保留着指向该请求的指针。运行工作流时会读取已释放的内存，并间歇性崩溃。
丢失的唤醒。 只有 Signal 和完成的屏障会把阻塞的节点重新放入队列。阻塞的 Send、Recv 或 Lock 永远不会被重试，因此工作流永远无法完成，wait_workflow 也不会返回。
没有错误通道。 被拒绝的工作流变成一个以 Ok 报告的空句柄，execute_reduce_sum_i32 把失败报告为 0。
运行时标识。 supports_openmp() 是常量 true，而 moon 构建并没有 OpenMP。

被否决的方案

工作窃取双端队列。 当任务数量多且不均匀时，每个工作线程一个双端队列才划算。这里的工作流节点是在同一把锁下执行的常数时间协议步骤，因此共享的 FIFO 更简单也足够；数据并行则交给每个内核内部的 OpenMP。
在 C 线程上执行 MoonBit 闭包。 MoonBit 运行时并不保证其对象可以在外部线程中使用，因此内核改为固定的 C 函数。
跨接口复制数组。 复制会让内存模型变得平凡，但会使每个内核的内存流量翻倍；借用加上互不相交的写入能提供同样的安全性。
回绕运算。 如上文所推导，为了得到精确结果而被否决。

边界

这个后端不执行计划、用户定义的内核、浮点数据或 Bytes；不通过通道或共享能力移动数据；不实现读写锁或信号量；不检测死锁，也不提供超时；并且只能在 native 目标上构建。

代码把块数计算为 $\min(k, w)$ ，在覆盖条件下它等于 $k$ 。若没有该条件，块会大于 $c$ ，因此运行时直接拒绝。 ↩