Module Private.Cells

A lock-free queue-like structure with suspension and cancellation.

This module provides an infinite sequence of atomic cells, which can be used for whatever you like. There are two pointers into this sequence: a suspend (consumer) pointer and a resume (producer) pointer. These are similar to the head and tail pointers in a traditional queue, except that the consumer is also permitted to get ahead of the producer.

To use this as a plain queue, each producer calls Make.next_resume to get the cell at the resume (tail) pointer (and advance it atomically), then stores its value in the cell. Each consumer calls Make.next_suspend to get the next cell at the head of the queue (and advance the suspend pointer).

The consumer/suspender is permitted to get ahead of the producer. In this case, the consumer will CAS the cell from its initial state to a Request state containing a callback to receive the value when it arrives. When a producer later tries to CAS the cell from the initial state to holding a value, it will fail and find the Request with the callback function instead. It can then provide the value directly to the callback.

A suspender can be cancelled by CASing the Request to a Cancelled state. It should also call Make.cancel_cell (if the CAS succeeds), to allow the cell to be freed. If a resumer's CAS fails because the cell is cancelled, it can retry with a fresh cell.

For efficiency, cells are grouped into segments, which are stored in a linked list. Once all the cells in a segment are cancelled, the whole segment may be freed.

This is based on A formally-verified framework for fair synchronization in kotlin coroutines, Appendix C, which contains more details and examples of use.

This module also adds the Make.resume_all function, which is useful for broadcasting.

module type CELL = sig ... end

The signature for user-defined cell contents.

module Make (Cell : CELL) : sig ... end