Module Kcas

This library provides a software transactional memory (STM) implementation based on an atomic lock-free multi-word compare-and-set (MCAS) algorithm enhanced with read-only compare operations and ability to block awaiting for changes.

Features and properties:

In other words, performance should be acceptable and scalable for many use cases, the non-blocking properties should allow use in many contexts including those where locks are not acceptable, and the features provided should support most practical needs.

A quick tour

Let's first open the library for convenience:

open Kcas

To use the library one creates shared memory locations:

# let a = Loc.make 0
  and b = Loc.make 0
  and x = Loc.make 0
val a : int Loc.t = Kcas.Loc.Loc {Kcas.Loc.state = <poly>; id = <poly>}
val b : int Loc.t = Kcas.Loc.Loc {Kcas.Loc.state = <poly>; id = <poly>}
val x : int Loc.t = Kcas.Loc.Loc {Kcas.Loc.state = <poly>; id = <poly>}

One can then manipulate the locations individually:

# Loc.set a 10
- : unit = ()

# Loc.get a
- : int = 10

# Loc.compare_and_set b 0 52
- : bool = true

# Loc.get b
- : int = 52

Block waiting for changes to locations:

# let a_domain = Domain.spawn @@ fun () ->
    let x = Loc.get_as (fun x -> Retry.unless (x <> 0); x) x in
    Printf.sprintf "The answer is %d!" x
val a_domain : string Domain.t = <abstr>

Perform transactions over locations:

# let tx ~xt =
    let a = Xt.get ~xt a
    and b = Xt.get ~xt b in
    Xt.set ~xt x (b - a)
  Xt.commit { tx }
- : unit = ()

And now we have it:

# Domain.join a_domain
- : string = "The answer is 42!"

The main repository includes a longer introduction with many examples and discussion of more advanced topics for designing lock-free algorithms.

Auxiliary modules

The modules in this section serve auxiliary purposes. On a first read you can skip over these. The documentation links back to these modules where appropriate.

module Timeout : sig ... end

Timeout support.

module Retry : sig ... end

Retry support.

module Mode : sig ... end

Operating modes of the k-CAS-n-CMP algorithm.

Individual locations

Individual shared memory locations can be created and manipulated through the Loc module that is essentially compatible with the Stdlib.Atomic module except that some of the operations take additional optional arguments:

module Loc : sig ... end

Shared memory locations.

Manipulating multiple locations atomically

Multiple shared memory locations can be manipulated atomically using the Xt module to explicitly pass a transaction log to record accesses.

Atomic operations over multiple shared memory locations are performed in two or three phases:

1. The first phase essentially records a list or log of operations to access shared memory locations. The first phase involves code you write as a user of the library. Aside from some advanced techniques, shared memory locations are not mutated during this phase.

2. The second phase attempts to perform the operations atomically. This is done internally by the library implementation. Only logically invisible writes to shared memory locations are performed during this phase.

3. In `Obstruction_free mode a third phase verifies all read-only operations. This is also done internally by the library implementation.

Each phase may fail. In particular, in the first phase, as no changes to shared memory have yet been attempted, it is safe, for example, to raise exceptions to signal failure. Failure on the third phase is automatically handled by Xt.commit.

Only after all phases have completed succesfully, the writes to shared memory locations are atomically marked as having taken effect and subsequent reads of the locations will be able to see the newly written values.

module Xt : sig ... end

Explicit transaction log passing on shared memory locations.