Skip to content

Commit

Permalink
Improve documentation. (#177)
Browse files Browse the repository at this point in the history
  • Loading branch information
lyrm authored Dec 4, 2024
1 parent 78bbd54 commit 23c957d
Show file tree
Hide file tree
Showing 16 changed files with 173 additions and 82 deletions.
8 changes: 4 additions & 4 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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.

Expand Down
8 changes: 8 additions & 0 deletions src/bounded_queue/bounded_queue.mli
Original file line number Diff line number Diff line change
@@ -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
8 changes: 0 additions & 8 deletions src/bounded_queue/bounded_queue_intf.mli
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
8 changes: 8 additions & 0 deletions src/bounded_queue/bounded_queue_unsafe.mli
Original file line number Diff line number Diff line change
@@ -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
2 changes: 1 addition & 1 deletion src/htbl/htbl.mli
Original file line number Diff line number Diff line change
@@ -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
Expand Down
2 changes: 1 addition & 1 deletion src/htbl/htbl_unsafe.mli
Original file line number Diff line number Diff line change
@@ -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
Expand Down
14 changes: 14 additions & 0 deletions src/michael_scott_queue/michael_scott_queue.mli
Original file line number Diff line number Diff line change
@@ -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
14 changes: 0 additions & 14 deletions src/michael_scott_queue/michael_scott_queue_intf.mli
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
15 changes: 15 additions & 0 deletions src/michael_scott_queue/michael_scott_queue_unsafe.mli
Original file line number Diff line number Diff line change
@@ -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
68 changes: 34 additions & 34 deletions src/mpsc_queue.mli
Original file line number Diff line number Diff line change
@@ -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} *)
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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.
Expand All @@ -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. *)

Expand All @@ -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
Expand Down
66 changes: 57 additions & 9 deletions src/saturn.mli
Original file line number Diff line number Diff line change
Expand Up @@ -26,22 +26,70 @@ Copyright (c) 2017, Nicolas ASSOUAD <[email protected]>
########
*)

(** 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
16 changes: 14 additions & 2 deletions src/skiplist.mli
Original file line number Diff line number Diff line change
@@ -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}*)

Expand Down Expand Up @@ -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.
Expand Down
8 changes: 8 additions & 0 deletions src/spsc_queue/spsc_queue.mli
Original file line number Diff line number Diff line change
@@ -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
8 changes: 0 additions & 8 deletions src/spsc_queue/spsc_queue_intf.mli
Original file line number Diff line number Diff line change
@@ -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
Expand Down
8 changes: 8 additions & 0 deletions src/spsc_queue/spsc_queue_unsafe.mli
Original file line number Diff line number Diff line change
@@ -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
Loading

0 comments on commit 23c957d

Please sign in to comment.