一句话：扩展 OCaml 类型系统，以 mode 保证多线程数据竞争自由并兼容顺序代码。
该论文提出 DRFCaml，扩展 OCaml 类型系统，在保持既有顺序代码向后兼容的同时，保证多线程程序的数据竞争自由。作者在 Lorenzen 等人引入的 locality、uniqueness 和 affinity 等 mode 基础上，新增 contention 与 portability 两个 mode 轴，用于记录数据是否已被共享或可在线程间共享。虽然基础类型与 mode 系统表达力有限，但通过胶囊（由唯一幽灵密钥控制访问的内存区域）和读写锁 API，可安全地在线程间共享带别名和可变状态的复杂数据结构。论文形式化了完整系统，并在 Rocq 证明助手中基于 Iris 程序逻辑建立语义模型，证明了系统可靠性。
We present DRFCaml, an extension of OCaml’s type system that guarantees data race freedom for multithreaded OCaml programs while retaining backward compatibility with existing sequential OCaml code. We build on recent work of Lorenzen et al., who extend OCaml with modes that keep track of locality, uniqueness, and affinity. We introduce two new mode axes, contention and portability , which record whether data has been shared or can be shared between multiple threads. Although this basic type-and-mode system has limited expressive power by itself, it does let us express APIs for capsules , regions of memory whose access is controlled by a unique ghost key, and reader-writer locks , which allow a thread to safely acquire partial or full ownership of a key. We show that this allows complex data structures (which may involve aliasing and mutable state) to be safely shared between threads. We formalize the complete system and establish its soundness by building a semantic model of it in the Iris program logic on top of the Rocq proof assistant.
@article{GeorgesPEWDECPD25,
title = {Data Race Freedom à la Mode},
author = {Aïna Linn Georges and Benjamin Peters and Laila Elbeheiry and Leo White and Stephen Dolan and Richard A. Eisenberg and Chris Casinghino and François Pottier and Derek Dreyer},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {POPL},
year = {2025},
doi = {10.1145/3704859}
}