Module Kcas

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.