Data Race Freedom à la Mode
summary
DRFcaml extends OCaml's type system with new mode axes (contention and portability) to statically guarantee data-race freedom for multi-threaded OCaml while remaining backward-compatible with sequential code. The design builds on Lorenzen et al.'s locality/uniqueness/affinity modes, exposes APIs for capsules (memory regions guarded by a unique ghost key) and reader-writer locks to transfer partial/full ownership safely, and is formalized and proved sound via an Iris semantic model encoded in the Rocq proof assistant.
AI-written summary · about
chapters (5)
- 0:00Introduction to OXCaml
- 3:55DRFCaml design overview
- 7:55Enforcing data race freedom
- 10:03Capsule and Mutex APIs
- 15:17Conclusion and Q&A
related talks
35m"Memory Safety is Merely Table Stakes [...]"
28mData Race Detection by Digest-Driven Abstract Interpretation
21mSeparation Logics for Probability, Concurrency, and Security
15mSafeRace: Assessing and Addressing WebGPU Memory Safety in the Presence of Data Races
14mSecRSL: Security Separation Logic for C11 Release-Acquire Concurrency
33mData-Dependent Confidentiality in DCR Graphs
21mScaling Data Analytics Via Confidential Computing on RISC-V
21mSecurely Compiling F* Programs With IO and Then Linking Them Against Weakly-Typ...