From 23c957da0225c50f0075d39f2e1f6f519a1e3507 Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Wed, 4 Dec 2024 19:23:21 +0100 Subject: [PATCH] Improve documentation. (#177) --- README.md | 8 +-- src/bounded_queue/bounded_queue.mli | 8 +++ src/bounded_queue/bounded_queue_intf.mli | 8 --- src/bounded_queue/bounded_queue_unsafe.mli | 8 +++ src/htbl/htbl.mli | 2 +- src/htbl/htbl_unsafe.mli | 2 +- .../michael_scott_queue.mli | 14 ++++ .../michael_scott_queue_intf.mli | 14 ---- .../michael_scott_queue_unsafe.mli | 15 ++++ src/mpsc_queue.mli | 68 +++++++++---------- src/saturn.mli | 66 +++++++++++++++--- src/skiplist.mli | 16 ++++- src/spsc_queue/spsc_queue.mli | 8 +++ src/spsc_queue/spsc_queue_intf.mli | 8 --- src/spsc_queue/spsc_queue_unsafe.mli | 8 +++ src/treiber_stack.mli | 2 +- 16 files changed, 173 insertions(+), 82 deletions(-) diff --git a/README.md b/README.md index 69a9cae8..f4259e02 100644 --- a/README.md +++ b/README.md @@ -42,8 +42,8 @@ You can learn more about the **motivation** behind `Saturn` through the implemen - [Lock-free Bag](#lock-free-bag) - [About the Unsafe Data Structures](#about-the-unsafe-data-structures) - [Usage](#usage) - - [Data Structures with Domain Roles](#data-structures-with-domain-roles) - - [Composability](#composability) + - [Data Structures with Domain Roles](#data-structures-with-domain-roles) + - [Composability](#composability) - [Testing](#testing) - [Benchmarks](#benchmarks) - [Contributing](#contributing) @@ -168,12 +168,12 @@ what not to do with them. Two main points are discussed: - some data structures have restrictions on what operations can be performed in a single domain or a set of domains - the currently provided data structures are non-composable -### Data Structures with Domain Roles +## Data Structures with Domain Roles Some provided data structures are designed to work with specific domain configurations. These restrictions optimize their implementation, but failing to respect them may compromise safety properties. These limitations are clearly indicated in the documentation and often reflected in the name of the data structure itself. For instance, a single-consumer queue must have only one domain performing `pop` operations at any given time. To learn more about it, see this [document](doc/domain-role.md). -### Composability +## Composability Composability refers to the ability to combine functions while preserving their properties. For Saturn data structures, the expected properties include atomic consistency (or linearizability) and progress guarantees, such as lock-freedom. Unfortunately, Saturn's data structures are not composable. diff --git a/src/bounded_queue/bounded_queue.mli b/src/bounded_queue/bounded_queue.mli index d64f6612..68324889 100644 --- a/src/bounded_queue/bounded_queue.mli +++ b/src/bounded_queue/bounded_queue.mli @@ -1 +1,9 @@ +(** Lock-free bounded Queue. + + This module implements a lock-free bounded queue based on Michael-Scott's queue + algorithm. Adding a capacity to this algorithm adds a general overhead to the + operations, and thus, it is recommended to use the unbounded queue + {!Saturn.Queue} if you don't need it. + *) + include Bounded_queue_intf.BOUNDED_QUEUE diff --git a/src/bounded_queue/bounded_queue_intf.mli b/src/bounded_queue/bounded_queue_intf.mli index 03f1cacd..d46cb3cf 100644 --- a/src/bounded_queue/bounded_queue_intf.mli +++ b/src/bounded_queue/bounded_queue_intf.mli @@ -14,14 +14,6 @@ PERFORMANCE OF THIS SOFTWARE. *) module type BOUNDED_QUEUE = sig - (** Lock-free bounded Queue. - - This module implements a lock-free bounded queue based on Michael-Scott's queue - algorithm. Adding a capacity to this algorithm adds a general overhead to the - operations, and thus, it is recommended to use the unbounded queue - {!Saturn.Queue} if you don't need it. - *) - (** {1 API} *) type 'a t diff --git a/src/bounded_queue/bounded_queue_unsafe.mli b/src/bounded_queue/bounded_queue_unsafe.mli index d64f6612..27d44ac3 100644 --- a/src/bounded_queue/bounded_queue_unsafe.mli +++ b/src/bounded_queue/bounded_queue_unsafe.mli @@ -1 +1,9 @@ +(** Optimized lock-free bounded Queue. + + This module implements a lock-free bounded queue based on Michael-Scott's queue + algorithm. Adding a capacity to this algorithm adds a general overhead to the + operations, and thus, it is recommended to use the unbounded queue + {!Saturn.Queue} if you don't need it. + *) + include Bounded_queue_intf.BOUNDED_QUEUE diff --git a/src/htbl/htbl.mli b/src/htbl/htbl.mli index dc6c2330..8a21bfd5 100644 --- a/src/htbl/htbl.mli +++ b/src/htbl/htbl.mli @@ -1,4 +1,4 @@ -(** Lock-free hash table. +(** Lock-free and resizable hash table. The operations provided by this hash table are designed to work as building blocks of non-blocking algorithms. Specifically, the operation signatures diff --git a/src/htbl/htbl_unsafe.mli b/src/htbl/htbl_unsafe.mli index dc6c2330..e785b652 100644 --- a/src/htbl/htbl_unsafe.mli +++ b/src/htbl/htbl_unsafe.mli @@ -1,4 +1,4 @@ -(** Lock-free hash table. +(** Optimized lock-free and resizable hash table. The operations provided by this hash table are designed to work as building blocks of non-blocking algorithms. Specifically, the operation signatures diff --git a/src/michael_scott_queue/michael_scott_queue.mli b/src/michael_scott_queue/michael_scott_queue.mli index c723f6f3..8b718185 100644 --- a/src/michael_scott_queue/michael_scott_queue.mli +++ b/src/michael_scott_queue/michael_scott_queue.mli @@ -1 +1,15 @@ +(** + Michael-Scott classic lock-free multi-producer multi-consumer queue. + + All functions are lockfree. It is the recommended starting point + when needing FIFO structure. It is inspired by {{: + https://www.cs.rochester.edu/~scott/papers/1996_PODC_queues.pdf} + Simple, Fast, and Practical Non-Blocking and Blocking Concurrent + Queue Algorithms}. + + If you need a [length] function, you can use the bounded queue + {!Saturn.Bounded_queue} instead with maximun capacity (default value). + However, this adds a general overhead to the operation. +*) + include Michael_scott_queue_intf.MS_QUEUE diff --git a/src/michael_scott_queue/michael_scott_queue_intf.mli b/src/michael_scott_queue/michael_scott_queue_intf.mli index 5c0acc8d..eccb56a4 100644 --- a/src/michael_scott_queue/michael_scott_queue_intf.mli +++ b/src/michael_scott_queue/michael_scott_queue_intf.mli @@ -16,20 +16,6 @@ *) module type MS_QUEUE = sig - (** - Michael-Scott classic multi-producer multi-consumer queue. - - All functions are lockfree. It is the recommended starting point - when needing FIFO structure. It is inspired by {{: - https://www.cs.rochester.edu/~scott/papers/1996_PODC_queues.pdf} - Simple, Fast, and Practical Non-Blocking and Blocking Concurrent - Queue Algorithms}. - - If you need a [length] function, you can use the bounded queue - {!Saturn.Bounded_queue} instead with maximun capacity (default value). - However, this adds a general overhead to the operation. -*) - (** {1 API} *) type 'a t diff --git a/src/michael_scott_queue/michael_scott_queue_unsafe.mli b/src/michael_scott_queue/michael_scott_queue_unsafe.mli index c723f6f3..19fdeddb 100644 --- a/src/michael_scott_queue/michael_scott_queue_unsafe.mli +++ b/src/michael_scott_queue/michael_scott_queue_unsafe.mli @@ -1 +1,16 @@ +(** + Optimized Michael-Scott lock-free multi-producer multi-consumer + queue. + + All functions are lockfree. It is the recommended starting point + when needing FIFO structure. It is inspired by {{: + https://www.cs.rochester.edu/~scott/papers/1996_PODC_queues.pdf} + Simple, Fast, and Practical Non-Blocking and Blocking Concurrent + Queue Algorithms}. + + If you need a [length] function, you can use the bounded queue + {!Saturn.Bounded_queue} instead with maximun capacity (default value). + However, this adds a general overhead to the operation. +*) + include Michael_scott_queue_intf.MS_QUEUE diff --git a/src/mpsc_queue.mli b/src/mpsc_queue.mli index 29e1bc99..4b453bda 100644 --- a/src/mpsc_queue.mli +++ b/src/mpsc_queue.mli @@ -1,12 +1,12 @@ -(** Lock-free multi-producer, single-consumer, domain-safe queue - without support for cancellation. +(** Lock-free multi-producer, single-consumer, domain-safe queue without support + for cancellation. This data structure is well-suited for use as a scheduler's run queue. - **Note**: This queue does not include safety mechanisms to prevent - misuse. If consumer-only functions are called concurrently by multiple - domains, the queue may enter an unexpected state, due to data races - and a lack of linearizability. + {b Warning}: This queue does not include safety mechanisms to prevent misuse. + If consumer-only functions are called concurrently by multiple domains, the + queue may enter an unexpected state, due to data races and a lack of + linearizability. *) (** {1 API} *) @@ -42,16 +42,16 @@ val of_list : 'a list -> 'a t (** {2 Producer-only functions} *) val push : 'a t -> 'a -> unit -(** [push q v] adds the element [v] at the end of the queue [q]. This - can be used safely by multiple producer domains, in parallel with - the other operations. +(** [push q v] adds the element [v] at the end of the queue [q]. This can be + used safely by multiple producer domains, in parallel with the other + operations. @raise Closed if [q] is closed. *) val push_all : 'a t -> 'a list -> unit -(** [push_all q vs] adds all the elements [vs] at the end of the queue [q]. - This can be used safely by multiple producer domains, in parallel with - the other operations. +(** [push_all q vs] adds all the elements [vs] at the end of the queue [q]. This + can be used safely by multiple producer domains, in parallel with the other + operations. @raise Closed if [q] is closed. @@ -79,38 +79,38 @@ val push_all : 'a t -> 'a list -> unit (** {2 Consumer-only functions} *) exception Empty -(** Raised when {!pop} or {!peek} is applied to an empty queue. *) +(** Raised when {!pop_exn} or {!peek_exn} is applied to an empty queue. *) val is_empty : 'a t -> bool -(** [is_empty q] is [true] if calling [pop] would return [None]. - This can only be used by the consumer. +(** [is_empty q] is [true] if calling [pop_exn] would return [None]. This can + only be used by the consumer. @raise Closed if [q] is closed and empty. *) val close : 'a t -> unit -(** [close q] marks [q] as closed, preventing any further items from - being pushed by the producers (i.e. with {!push}). This can only - be used by the consumer. +(** [close q] marks [q] as closed, preventing any further items from being + pushed by the producers (i.e. with {!push}). This can only be used by the + consumer. @raise Closed if [q] has already been closed. *) val pop_exn : 'a t -> 'a -(** [pop_exn q] removes and returns the first element in queue [q]. This - can only be used by the consumer. +(** [pop_exn q] removes and returns the first element in queue [q]. This can + only be used by the consumer. @raise Empty if [q] is empty. @raise Closed if [q] is closed and empty. *) val pop_opt : 'a t -> 'a option -(** [pop_opt q] removes and returns the first element in queue [q] or - returns [None] if the queue is empty. This can only be used by the - consumer. +(** [pop_opt q] removes and returns the first element in queue [q] or returns + [None] if the queue is empty. This can only be used by the consumer. @raise Closed if [q] is closed and empty. *) val drop_exn : 'a t -> unit -(** [drop_exn q] removes the first element in queue [q]. This can only be used by the consumer. +(** [drop_exn q] removes the first element in queue [q]. This can only be used + by the consumer. @raise Empty if [q] is empty. @@ -125,16 +125,15 @@ val peek_exn : 'a t -> 'a @raise Closed if [q] is closed and empty. *) val peek_opt : 'a t -> 'a option -(** [peek_opt q] returns the first element in queue [q] or returns - [None] if the queue is empty. This can only be used by the - consumer. +(** [peek_opt q] returns the first element in queue [q] or returns [None] if the + queue is empty. This can only be used by the consumer. @raise Closed if [q] is closed and empty. *) val push_head : 'a t -> 'a -> unit -(** [push_head q v] adds the element [v] at the head of the queue - [q]. This can only be used by the consumer (if run in parallel - with {!pop}, the item might be skipped). +(** [push_head q v] adds the element [v] at the head of the queue [q]. This can + only be used by the consumer (if run in parallel with {!pop_exn}, the item + might be skipped). @raise Closed if [q] is closed and empty. *) @@ -161,10 +160,11 @@ val push_head : 'a t -> 'a -> unit *) (** {2 Multicore example} - Note: The barrier is used in this example solely to make the results more - interesting by increasing the likelihood of parallelism. Spawning a domain is - a costly operation, especially compared to the relatively small amount of work - being performed here. In practice, using a barrier in this manner is unnecessary. + {b Note}: The barrier is used in this example solely to make the results more + interesting by increasing the likelihood of parallelism. Spawning a domain + is a costly operation, especially compared to the relatively small amount of + work being performed here. In practice, using a barrier in this manner is + unnecessary. {@ocaml non-deterministic=command[ # open Saturn.Single_consumer_queue diff --git a/src/saturn.mli b/src/saturn.mli index 55f63002..657630af 100644 --- a/src/saturn.mli +++ b/src/saturn.mli @@ -26,22 +26,70 @@ Copyright (c) 2017, Nicolas ASSOUAD ######## *) -(** Lock-free data structures for Multicore OCaml *) +(** Parallelism-safe data structures for Multicore OCaml *) + +(** {1 Useful Information} + + {2 Domain-Specific Data Structures} + Some data structures are optimized for specific domain configurations. These + restrictions enhance performance but must be adhered to for maintaining safety + properties. These limitations are documented and often reflected in the data + structure's name. For example, a single-consumer queue should only have one + domain performing `pop` operations at any time. + + For more details, refer to this + {{: https://github.com/ocaml-multicore/saturn/blob/main/doc/domain-role.md}{document}}. + + {2 Composability} + + Composability is the ability to combine functions while preserving their + properties, such as atomic consistency (linearizability) and progress + guarantees (e.g., lock-freedom). Saturn's data structures, however, are not + composable. + + For more details, refer to this + {{: https://github.com/ocaml-multicore/saturn/blob/main/doc/composability.md}{document}}. +*) + +(** {2 Unsafe Data Structures} + + Some data structures have both a normal and an {b unsafe} version. The + {b unsafe} version uses `Obj.magic`, which may be unsafe with flambda2 + optimizations. + + The unsafe version is provided because certain optimizations require features + not currently available in OCaml, such as arrays of atomics or atomic fields + in records. It is recommended to use the normal version unless performance + requirements necessitate the unsafe version. *) (** {1 Data structures} *) +(** {2 Collections} *) + +module Htbl = Htbl +module Htbl_unsafe = Htbl_unsafe +module Skiplist = Skiplist +module Bag = Bag + +(** {2 Queues} *) + module Queue = Michael_scott_queue module Queue_unsafe = Michael_scott_queue_unsafe -module Stack = Treiber_stack -module Bounded_stack = Bounded_stack module Bounded_queue = Bounded_queue module Bounded_queue_unsafe = Bounded_queue_unsafe -module Work_stealing_deque = Ws_deque +module Single_consumer_queue = Mpsc_queue module Single_prod_single_cons_queue = Spsc_queue module Single_prod_single_cons_queue_unsafe = Spsc_queue_unsafe -module Single_consumer_queue = Mpsc_queue -module Skiplist = Skiplist + +(** {2 Stacks} *) + +module Stack = Treiber_stack +module Bounded_stack = Bounded_stack + +(** {2 Work Stealing Deque }*) + +module Work_stealing_deque = Ws_deque + +(** {1 Other}*) + module Size = Size -module Htbl = Htbl -module Htbl_unsafe = Htbl_unsafe -module Bag = Bag diff --git a/src/skiplist.mli b/src/skiplist.mli index 2716ffdb..ae5da4a3 100644 --- a/src/skiplist.mli +++ b/src/skiplist.mli @@ -1,4 +1,16 @@ -(** A lock-free skiplist. *) +(** Lock-free non-resizable skiplist. + + A skiplist is a probabilistic data structure that has an average logarithmic + complexity for search and insertion operations. Like `Stdlib.Map`, it is an + ordered collection. + + {b Warning}: This skiplist is not resizable. It will, however, continue + to work once the limit capacity is reached, but performance will decrease as + the depth of the structure won't be enough to maintain logarithmic performance. + + {b Sources}: This implementation is inspired by the algorithm in chapter 14 of + {i The Art of Multiprocessor Programming} book. +*) (** {1 API}*) @@ -80,7 +92,7 @@ val try_remove : ('k, 'v) t -> 'k -> bool (** {2 Multicore example} - **Note**: The barrier is used in this example solely to make the results more + {b Note}: The barrier is used in this example solely to make the results more interesting by increasing the likelihood of parallelism. Spawning a domain is a costly operation, especially compared to the relatively small amount of work being performed here. In practice, using a barrier in this manner is unnecessary. diff --git a/src/spsc_queue/spsc_queue.mli b/src/spsc_queue/spsc_queue.mli index 776c6aa1..64ef149f 100644 --- a/src/spsc_queue/spsc_queue.mli +++ b/src/spsc_queue/spsc_queue.mli @@ -1 +1,9 @@ +(** Lock-free single-producer, single-consumer queue. + + {b Warning}: This queue does not include safety mechanisms to prevent + misuse. If consumer-only functions are called concurrently by multiple + domains, the queue may enter an unexpected state, due to data races + and a lack of linearizability. The same goes for producer-only functions. + *) + include Spsc_queue_intf.SPSC_queue diff --git a/src/spsc_queue/spsc_queue_intf.mli b/src/spsc_queue/spsc_queue_intf.mli index 1a4853dd..ad8ad5bb 100644 --- a/src/spsc_queue/spsc_queue_intf.mli +++ b/src/spsc_queue/spsc_queue_intf.mli @@ -1,12 +1,4 @@ module type SPSC_queue = sig - (** Single producer single consumer queue. - - **Note**: This queue does not include safety mechanisms to prevent - misuse. If consumer-only functions are called concurrently by multiple - domains, the queue may enter an unexpected state, due to data races - and a lack of linearizability. The same goes for producer-only functions. - *) - (** {1 API} *) type 'a t diff --git a/src/spsc_queue/spsc_queue_unsafe.mli b/src/spsc_queue/spsc_queue_unsafe.mli index 776c6aa1..58306f29 100644 --- a/src/spsc_queue/spsc_queue_unsafe.mli +++ b/src/spsc_queue/spsc_queue_unsafe.mli @@ -1 +1,9 @@ +(** Optimized lock-free single-producer, single-consumer queue. + + {b Warning}: This queue does not include safety mechanisms to prevent + misuse. If consumer-only functions are called concurrently by multiple + domains, the queue may enter an unexpected state, due to data races + and a lack of linearizability. The same goes for producer-only functions. + *) + include Spsc_queue_intf.SPSC_queue diff --git a/src/treiber_stack.mli b/src/treiber_stack.mli index 4553e19b..3d1d9c8d 100644 --- a/src/treiber_stack.mli +++ b/src/treiber_stack.mli @@ -1,4 +1,4 @@ -(** Classic multi-producer multi-consumer Treiber stack. +(** Lock-free multi-producer multi-consumer Treiber stack. All functions are lock-free. It is the recommended starting point when needing a LIFO structure. *)