OxCaml 中的数据竞态自由

# OxCaml 中的数据竞争自由 · KC Sivaramakrishnan 来源：https://kcsrk.info/ocaml/oxcaml/x-ocaml/blogging/2026/05/07/data-race-freedom-in-oxcaml/ 2026年5月7日 不久前，我连上了 `x-ocaml`（https://kcsrk.info/ocaml/x-ocaml/blogging/2025/06/20/xocaml/），让这个博客可以嵌入实时、可编辑的 OCaml 笔记本。那篇文章使用的是普通的 OCaml 5 顶层环境。今天，你浏览器中运行的顶层环境是基于 OxCaml（https://oxcaml.org/）构建的，这是 Jane Street 对编译器的分支。这意味着我们可以交互式地证明一个小的并行程序是无数据竞争的，而无需启动任何线程。 下面的例子改编自 OxCaml 团队的优秀教程《并行入门（第 1 部分）》（https://oxcaml.org/documentation/tutorials/01-intro-to-parallelism-part-1/），并参考了我最近关于 OxCaml 的 CS6868（https://github.com/fplaunchpad/cs6868_s26）课程讲义（https://github.com/fplaunchpad/cs6868_s26/blob/main/lectures/11_oxcaml/handout.md）。该教程是权威参考，值得全文阅读；这篇文章试图以更易消化的小篇幅捕捉其精髓，重点放在共同在编译时排除数据竞争的两个新模式轴上，以及一个关于可移植性、容易误解的细微之处。 ## 快速说明：OCaml 中的数据竞争没那么可怕 在深入之前，值得暂停一下思考：我们为什么要在 OCaml 中排除数据竞争？在 C、C++ 或不安全的 Rust 中，数据竞争是灾难性的：标准允许编译器*做任何事*，包括静默的内存破坏，因为你的程序一开始就没有定义好的含义。OCaml 则温和得多。OCaml 的内存模型（https://ocaml.org/manual/5.4/memorymodel.html）保证即使是有竞争的程序也能保持类型安全和内存安全——一个有竞争的程序可能会观察到跨域的不一致值，但它不会崩溃，不会读取未初始化的内存，也不会违反类型系统的不变量。 因此，OCaml 中的数据竞争是一个逻辑错误，而不是运行时隐患。那为什么还要静态地捕捉它们呢？因为一旦程序是数据竞争自由的，你就能得到**顺序一致性**：任何可观察到的行为都可以解释为不同域操作的一种交错，且每个域自身的操作按程序顺序执行。这仍然是并发推理——存在许多可能的交错——但这是并发代码能拥有的最简单模型，并且等式推理、归纳法和通常的程序逻辑工具都可以迁移到每种交错上。放弃竞争自由，你就会失去这一点：可观察到的行为只能通过允许*线程内*重排来证明，即单一域的操作对其他域来说似乎以非程序顺序执行。顺序一致性才是真正的奖品。数据竞争自由是获得它的代价。 ## 你好，OxCaml 快速检查一下你的浏览器是否真的运行着 OxCaml 顶层环境。`@ local` 注解是 OxCaml 独有的语法；在标准的 OCaml 解析器上，它甚至无法解析。 let use_locally (x @ local) = x + 1 let () = Printf.printf "use_locally 42 = %d\n" (use_locally 42) ## 一个有竞争的 `gensym` 这是我们反复用到的例子：一个通过递增捕获的计数器来发放唯一 ID 的符号生成器。在顺序执行时它工作正常；单元格打印出两个 ID。最后一行试图将 `gensym` 发送到另一个域，这时类型检查器阻止了我们。 [@@@alert "-do_not_spawn_domains"] let gensym = let count = ref 0 in fun prefix -> count := !count + 1; prefix ^ "_" ^ string_of_int !count let () = Printf.printf "%s %s\n" (gensym "x") (gensym "x") let _ = Domain.Safe.spawn (fun () -> gensym "x") 在两个域中并行运行它，你就会打满数据竞争四要素清单上的每一项：两个域，共享的 `count`，两者都写，并且 `count` 是普通的 `ref`——不是原子的。在标准的 OCaml 5 上，编译器会乐于让你把这个闭包发送到另一个域。OxCaml 则在任何代码运行之前就拒绝了。错误信息提到了两个名字——*nonportable* 和 *portable*——它们在普通 OCaml 的词汇表中不存在。它们是什么意思？ ## 两个用于数据竞争自由的新模式 OxCaml 通过多种模式（https://oxcaml.org/jane/doc/extensions/modes/intro/）扩展了 OCaml 的类型系统——这些注解描述了值*如何*被使用，与它的类型正交。我已经在这个博客上写过其中两种：唯一性（https://kcsrk.info/ocaml/modes/oxcaml/2025/05/29/uniqueness_and_behavioural_types/），跟踪一个值是否至多有一个引用；以及线性（https://kcsrk.info/ocaml/modes/oxcaml/2025/06/04/linearity_and_uniqueness/），跟踪一个值可以被使用多少次。今天的文章是关于另一对——两个共同在编译时排除数据竞争的模式： - **争用（Contention）**——`uncontended` / `contended`：跟踪多个域是否可以同时访问某个值。一个 `contended` 的值可能此刻正在另一个域手中，因此类型系统限制了你对它所能做的事情。 - **可移植性（Portability）**——`portable` / `nonportable`：跟踪一个值是否可以安全地*跨越*域边界。发送到其他域的闭包必须是 `portable` 的。 这一对足以捕捉 `gensym` 的竞争。我们单独看每个限制，然后再回到闭包。 ### 争用拒绝可变写入 一个 `contended` 的值可能正在被另一个域修改。因此 OxCaml 拒绝让你读取或写入它的可变字段： type mood = Happy | Neutral | Sad type thing = { price : float; mutable mood : mood } (* 读取 contended 值的不可变字段是允许的。 *) let price_contended (t @ contended) = t.price (* 写入可变字段是不允许的。 *) let cheer_up_contended (t @ contended) = t.mood <- Happy 最后一行上的错误信息准确地指出了规则：*“这个值是 contended，但期望它是 uncontended，因为它的可变字段 mood 正在被写入。”* 甚至*读取*一个 `contended` 值的可变字段也会被拒绝——另一个域可能正在同一时刻进行写入。 ### 可移植性拒绝捕获的 ref 可移植性关乎闭包。一个 `@ portable` 的闭包是编译器已验证可以安全发送到另一个域的闭包，但有一个关键例外：闭包从其封闭作用域*捕获*的每个值，在闭包体内都被视为 `contended`。一个纯函数如果不修改任何东西，则是可移植的——争用规则没有反对它的理由： let test_portable () = let (f @ portable) = fun x y -> x + y in f 1 2 let () = Printf.printf "test_portable () = %d\n" (test_portable ()) 仅捕获一个 `ref` 是没问题的；但*修改*一个被捕获的 `ref` 才会违反规则： let test_nonportable () = let r = ref 0 in let (counter @ portable) () = incr r; !r in counter () 仔细阅读错误信息——它告诉你*确切原因*为何 `counter` 不可移植。闭包是 `@ portable` 的，所以捕获的 `r` 在闭包体内被视为 `contended`。但 `incr r` 是一个修改操作，而通过 ref 写入要求它是 `uncontended`。两个规则冲突了。那么原始的 `gensym` 拒绝也就说得通了：它做的正是同一件事——修改一个捕获的 `count`。 ## 陷阱与实际规则 把最后两个单元格放在一起看，很容易得出错误的结论：为了让一个函数可以安全地发送到另一个域，你必须放弃副作用。那就限制得太过了。 实际规则更窄，这个区别很重要。 可移植性约束的是闭包**从其封闭作用域捕获的内容**。捕获的值变成了 contended——这是规则，也是为什么 `gensym` 被拒绝的原因。但闭包的**参数**不是捕获物。它们在每次调用时被新鲜传入，因此可以按类型指定的任何模式传入——包括 `@ uncontended`。提供 uncontended 参数的义务转移到了调用者身上。这是一个比“无副作用”弱得多的要求。 ### 捕获 vs 参数：代码示例 下面是一个让区分更具体的例子。`loop` 是 `@ portable` 的，它的主体修改了一个 `int ref`。这可以工作，因为 ref 是一个注解为 `@ uncontended` 的*参数*，而不是捕获的东西： let (factorial_portable @ portable) n = let a = ref 1 in let rec (loop @ portable) (a @ uncontended) i = if i > 0 then begin a := !a * i; loop a (i - 1) end in loop a n; !a let () = Printf.printf "factorial_portable 10 = %d\n" (factorial_portable 10) 两个 `@ portable` 注解在这里起作用。内部那个说 `loop` 可以发送到另一个域——这是有趣的那个，它之所以可行是因为 `a` 是 `loop` 的*参数*，而不是捕获物：当 `loop` 最终从某个并行处被调用时，那个调用处必须证明它传入的 `a` 是无争用的。可移植性没有禁止修改；它把证明推给了调用点。外部注解说整个 `factorial_portable` 也是可移植的——每次调用它分配一个新的 `a`，并且不从外部捕获任何东西，所以我们可以把整个函数发送到另一个域。编译器在程序接收过程中验证这两个注解。 ## 形式化补充：默认值与子模式 到目前为止，我们把 `@ contended` 和 `@ portable` 当作有趣的模式来写，仿佛它们的缺席没什么特别的。实际上每个轴上有一个小格，有一个默认值和一个关于保证“多强”的方向。讲义总结如下： | 轴 | 模式 (`⊑`) | 默认值 | |------|-----------|-------| | 争用 | `uncontended` ⊑ `shared` ⊑ `contended` | `uncontended` | | 可移植性 | `portable` ⊑ `nonportable` | `nonportable` | 关系 `A ⊑ B` 是**子模式序**：模式 `A` 的值可以在期望模式 `B` 的地方使用，因为 `A` 带有更强的保证，而 `B` 是更宽松的期望。一个 `uncontended` 值满足一个 `@ contended` 参数（我们只是承诺被调用方可能让其他域接触它；如果其他域从未接触过，这个承诺是平凡兼容的）。一个 `portable` 闭包满足一个 `@ nonportable` 槽位。但反过来不成立——子模式是单向的。 默认值就是你写普通 OCaml 时得到的结果。每个值一开始是 `uncontended`——没有其他域拥有它，所以读写不受限制。每个闭包一开始是 `nonportable`——我们不做关于将其发送到别处的声明。这就是为什么在 OxCaml 下普通 OCaml 代码仍然通过类型检查的原因：默认值是每个轴最宽松的一端，只有当你（或一个并行 API）要求更强的保证时，你才会遇到新的限制。这篇文章只使用了争用链的两个端点——`uncontended` 和 `contended`——并跳过了 `shared`，它允许跨域的只读访问，对于 gensym 的故事不需要。 module Portable = struct module Atomic : sig type !'a t : value mod contended portable val make : 'a @ portable contended -> 'a t val fetch_and_add : int t @ local -> int -> int end = struct type !'a t : value mod contended portable = 'a Basement.Portable_atomic.t let make = Basement.Portable_atomic.make let fetch_and_add = Basement.Portable_atomic.fetch_and_add end end ## 回到 `gensym`：修复方案 捕获 vs 参数的区别足以修复简单的循环，但 `gensym` 的形状不同：有一个计数器必须跨调用共享。我们需要一个计数器类型，它*本身*是可移植的——一个值能同时跨越争用和可移植性两个模式，这样捕获它的闭包保持可移植。这正是 OxCaml 的 `portable`（https://github.com/oxcaml/oxcaml/tree/main/portable）库中的 `Portable.Atomic.t`：一个 `'a Portable.Atomic.t` 始终是可移植的且总是无争用的，无论它位于何处。 将计数器和 `gensym` 包装在一个模块中，这样顶层环境可以将整个包视为可移植的，然后实际执行一开始给我们带来麻烦的操作：将 `gensym` 发送到一个新生成的域。编译器接受了它（它已验证了 `Gen` 是可移植的），程序运行了： [@@@alert "-do_not_spawn_domains"] module Gen = struct open Portable let count = Atomic.make 0 let gensym prefix = let n = Atomic.fetch_and_add count 1 in prefix ^ "_" ^ string_of_int n end let d = Domain.Safe.spawn (fun () -> Gen.gensym "y") let s1 = Gen.gensym "x" let s2 = Domain.join d let () = Printf.printf "%s %s\n" s1 s2 顶层环境报告 `module Gen : sig ... end @@ portable`——模式推断注意到每个内部值都是可移植的，并使整个模块可移植，因此 `Gen.gensym` 在以可移植模式提取时能够存活。你可能想知道为什么我们不直接在顶层写 `let (gensym @ portable) prefix = ...`，就像上面 `factorial_portable` 那样的形式。这是顶层环境的一个特性：一个裸 `let` 会进入隐式顶层模块，而该模块本身处于默认的 `nonportable` 模式，因此当 `Domain.Safe.spawn` 之后读取 `gensym` 时，它看到一个不可移植的绑定并拒绝——尽管该闭包在它的绑定点已被验证为可移植。`factorial_portable` 单元格之所以能用更简单的形式，只是因为没有其他东西试图以可移植模式提取那个绑定。将其包装在 `module Gen` 中为闭包提供了自己的可移植之家，这才让它能够实际跨越域边界。在一个真实的 `.ml` 文件中，整个编译单元是一个模块，模式推断可以将其整体标记为可移植，因此不需要这种舞蹈。 （关于你在这里看到的 `Portable.Atomic`：在一个真实程序中，你会通过从 `portable`（https://github.com/oxcaml/oxcaml/tree/main/portable）opam 库中 `open Portable` 来获取它。为了保持页面大小合理，这个笔记本只包含了 `basement`（https://github.com/oxcaml/oxcaml/tree/main/basement）——提供实际原子操作的小型库——以及页面顶部的一个隐藏设置单元格，它用 kind 注解 `: value mod contended portable` 包装了它。这个 kind 告诉编译器这个类型跨了两个轴——捕获它的闭包保持可移植，并且任何域都可以接触它。）讲义（https://github.com/fplaunchpad/cs6868_s26/blob/main/lectures/11_oxcaml/handout.md）指出，对于比单个原子计数器更复杂的状态，正确的答案是**胶囊（capsules）**——一种结构化的方式，将可变状态及其访问协议打包在一起，从而使整个包是可移植的。 ## 剩余内容 这里的数据竞争自由保证与任何测试运行无关：上面的每次拒绝都发生在 OxCaml 二进制文件在磁盘上会经历的同一个编译步骤，在任何代码执行之前。最后的生成是一个演示，而不是证明——是编译器一开始就接受了程序，才告诉我们不可能有数据竞争。两个模式轴、一个 kind 注解以及关于“可移植”含义的清晰规则，足以使数据竞争自由成为类型检查器强制执行的性质。 这篇文章所依据的课程还深入探讨了胶囊（用于比原子更复杂的状态）和 `Parallel.fork_join2`（用于结构化并行）。这些是另一篇文章的素材。