Data Race Freedom à la Mode

Data Race Freedom à la Mode

---

연구 분야: Verification

---

---

학회: Proceedings of the ACM on Programming Languages, Volume 9, Issue POPL

---

초록

We present DRFcaml, an extension of OCaml's type system that guarantees data race freedom for multi-threaded 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.

---