Saturn: a library of verified concurrent data structures for OCaml 5
summary
Saturn is an OCaml 5 library on opam providing stack, queue, skiplist, hash table and work‑stealing deque implementations, benchmarked and partly formally verified. Concrete surprises include a reproduced negative size bug (size reaching -1 about 10–20% in a naive atomic counter test). Verification uses Iris mechanized in Coq; testing combines STM-style systematic stress tests and a model checker to exhaust interleavings. There's a separate sat_lo_free package for lock‑free variants, and benchmarks contrast mutex‑wrapped, Obj‑optimized, and standard implementations.
AI-written summary · about
chapters (12)
- 0:00Saturn and concurrent data structures
- 1:07Why concurrent structures are hard
- 3:57Concurrent stacks: literature and performance
- 5:19Saturn's data structure collection
- 7:28Testing and verification tools
- 9:35Optimizing data structures
- 11:00Benchmarking Saturn's queues
- 13:10Formal verification of structures
- 16:46Concurrency protocols in Iris
- 18:16Saturn versus other ecosystems
- 20:05Debugging OCaml performance
- 21:50Q&A
related talks
22mBuilding a lock-free STM for OCaml
21mAutomated Robustness Verification of Concurrent Data Structure Libraries Against(…)
18mMulticoretests - Parallel Testing Libraries for OCaml 5.0
15mCosmo: A Concurrent Separation Logic for Multicore Ocaml
30mMonadic interpreters for concurrent memory models: Executable semantics of a concurrent(…)
23mParallel Sequences in Multicore OCaml
19mEfficient Linearizability Monitoring
14mVerifying Concurrent Multicopy Search Structures