Cosmo: A Concurrent Separation Logic for Multicore Ocaml
summary
Cosmo provides a separation logic for Multicore OCaml that exposes the weak memory model yet lets you verify familiar locks: it instantiates Iris and is mechanized in Coq, models atomic vs non‑atomic locations, and isolates subjectivity into explicit views (sets of write events). Release/acquire on atomic accesses transfers subjective state; several lock implementations are formally verified so coarse‑grained programs using locks verify without reasoning about the weak memory details.
AI-written summary · about
chapters (11)
- 0:00Intro
- 0:35Multicore OCaml
- 1:08In traditional fine-grained concurrent separation logics...
- 2:07The challenge subjectivity
- 2:58Key idea: modeling subjectivity with views
- 5:10Key idea: decomposing subjective assertions
- 6:37Rules of atomic locations, simplified
- 7:19Rules of non-atomic locations
- 8:19Example: transferring an assertion through a spin lock
- 11:09The spin lock
- 12:45Methodology
related talks
24mSimuliris: A Separation Logic Framework for Verifying Concurrent Program Optimiz
30mMonadic interpreters for concurrent memory models: Executable semantics of a concurrent(…)
19mA Proof Recipe for Linearizability in Relaxed Memory Separation Logic
40mWhen magic meets multicore - OCaml and its elegant era of parallelism
21mCSL and relaxed memory
24mSaturn: a library of verified concurrent data structures for OCaml 5
22mBuilding a lock-free STM for OCaml
21mCommCSL: Proving Information Flow Security for Concurrent Programs using Abstract(…)