package saturn_lockfree

  1. Overview
  2. Docs
Lock-free data structures for multicore OCaml

Install

Dune Dependency

github.com Readme Changelog ISC License Edit opam file Versions (2)

Authors

  1. K
    KC Sivaramakrishnan <sk826@cl.cam.ac.uk>

Maintainers

  1. K
    KC Sivaramakrishnan <sk826@cl.cam.ac.uk>

Sources

saturn-0.4.0.tbz
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)

  1. domain_shims >= "0.1.0"
  2. dune >= "3.0"
  3. ocaml >= "4.12"

Dev Dependencies (6)

  1. dscheck with-test & >= "0.1.0"
  2. yojson with-test & >= "2.0.2"
  3. alcotest with-test & >= "1.6.0"
  4. qcheck-alcotest with-test & >= "0.18.1"
  5. qcheck-stm with-test & >= "0.2"
  6. qcheck with-test & >= "0.18.1"

Used by (1)

  1. saturn < "0.4.1"

Conflicts

None