package saturn_lockfree
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=7c7bec95a27055b41aa83540fcc1c6a87c9b7ad61bc511a532b8605ea33788fb
sha512=5a95888ec9d8979ceca9b57589109f9c7df6d72e51482a3cbc99988863d0b95cc8cf7592f433efd840475e79394eacf761e3e8503c8b3bfdd1bd74d8485c584e
Description
Published: 12 Jul 2023
README
Saturn
— parallelism-safe data structures for Multicore OCaml
This repository is a collection of parallelism-safe data structures for OCaml 5. They are contained in two packages:
Saturn
that includes every data structures and should be used by default if you just want parallelism-safe data structures..Saturn_lockfree
that includes only lock-free data structures.
The available data structures are :
Names | Names in Saturn (in Saturn_lockfree ) |
What is it ? | Sources |
---|---|---|---|
Treiber stack | Stack (same) |
A classic multi-producer multi-consumer stack, robust and flexible. Recommended starting point when needing a LIFO structure | |
Michael-Scott queue | Queue (same) |
A classic multi-producer multi-consumer queue, robust and flexible. Recommended starting point when needing a FIFO structure. | Simple, Fast, and Practical Non-Blocking and Blocking Concurrent Queue Algorithms |
Chase-Lev Work-Stealing Dequeue | Work_stealing_deque (same) |
Single-producer, multi-consumer dynamic-size double-ended queue (deque). Ideal for throughput-focused scheduling using per-core work distribution. Note, pop and steal follow different ordering (respectively LIFO and FIFO) and have different linearization contraints. |
Dynamic circular work-stealing deque and Correct and efficient work-stealing for weak memory models) |
SPSC Queue | Single_prod_single_ cons_queue (same) |
Simple single-producer single-consumer fixed-size queue. Thread-safe as long as at most one thread acts as producer and at most one as consumer at any single point in time. | |
MPMC bounded relaxed queue | Relaxed queue (same) |
Multi-producer, multi-consumer, fixed-size relaxed queue. Optimised for high number of threads. Not strictly FIFO. Note, it exposes two interfaces: a lockfree and a non-lockfree (albeit more practical) one. See the mli for details. | |
MPSC Queue | Single_consumer_queue (same) |
A multi-producer, single-consumer, thread-safe queue without support for cancellation. This makes a gooddata structure for a scheduler's run queue. It is used in Eio. | It is a single consumer version of the queue described in Implementing lock-free queues. |
Usage
Saturn
can be installed from opam
: opam install saturn
. Sample usage of Work_stealing_deque
is illustrated below.
module Ws_deque = Work_stealing_deque.M
let q = Ws_deque.create ()
let () = Ws_deque.push q 100
let () = assert (Ws_deque.pop q = 100)
Tests
Several kind of tests are provided for each data structure:
unitary tests and
qcheck
tests: check semantics and expected behaviors with one and more domains;STM
tests: check linearizability for two domains (see multicoretests library);dscheck
: checks non-blocking property for as many domains as wanted (for two domains most of the time). See dscheck.
See test/README.md for more details.
Benchmarks
There is a number of benchmarks in bench
directory. You can run them with make bench
. See bench/README.md for more details.
Contributing
Contributions are appreciated! If you intend to add a new data structure, please read this before.
Dependencies (3)
-
domain_shims
>= "0.1.0"
-
dune
>= "3.0"
-
ocaml
>= "4.12"
Dev Dependencies (6)
-
dscheck
with-test & >= "0.1.0"
-
yojson
with-test & >= "2.0.2"
-
alcotest
with-test & >= "1.6.0"
-
qcheck-alcotest
with-test & >= "0.18.1"
-
qcheck-stm
with-test & >= "0.2"
-
qcheck
with-test & >= "0.18.1"
Used by (1)
-
saturn
< "0.4.1"
Conflicts
None