package 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:

• Efficient: In the common uncontended case only k + 1 single-word CASes are required per k-CAS and, as a special case, 1-CAS requires only a single single-word CAS.

• Lock-free: The underlying algorithm guarantees that at least one operation will be able to make progress.

• Disjoint-access parallel: Unrelated operations progress independently, without interference, even if they occur at the same time.

• Read-only compares: The algorithm supports obstruction-free read-only compare (CMP) operations that can be performed on overlapping locations in parallel without interference.

• Blocking await: The algorithm supports timeouts and awaiting for changes to any number of shared memory locations.

• Composable: Independently developed transactions can be composed with ease sequentially, conjunctively, conditionally, and disjunctively.

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)
  in
  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.

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:

• backoff specifies the configuration for the Backoff mechanism. In special cases, having more detailed knowledge of the application, one might adjust the configuration to improve performance.

• timeoutf specifies a timeout in seconds and, if specified, the Timeout.Timeout exception may be raised by the operation to signal that the timeout expired.

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.