package kcas

  1. Overview
  2. Docs
package kcas
Legend:
Library
Module
Module type
Parameter
Class
Class type

Explicit transaction log passing on shared memory locations.

type 'x t

Type of an explicit transaction log on shared memory locations.

Note that a transaction log itself is not domain-safe and should generally only be used by a single domain. If a new domain is spawned inside a function recording shared memory accesses to a log and the new domain also records accesses to the log it may become inconsistent.

Recording accesses

Accesses of shared memory locations using an explicit transaction log first ensure that the initial value of the shared memory location is recorded in the log and then act on the current value of the shared memory location as recorded in the log.

val get : xt:'x t -> 'a Loc.t -> 'a

get ~xt r returns the current value of the shared memory location r in the explicit transaction log xt.

val set : xt:'x t -> 'a Loc.t -> 'a -> unit

set ~xt r v records the current value of the shared memory location r to be the given value v in the explicit transaction log xt.

val update : xt:'x t -> 'a Loc.t -> ('a -> 'a) -> 'a

update ~xt r f is equivalent to let x = get ~xt r in set ~xt r (f x); x with the limitation that f must not and is not allowed to record accesses to the transaction log.

val modify : xt:'x t -> 'a Loc.t -> ('a -> 'a) -> unit

modify ~xt r f is equivalent to let x = get ~xt r in set ~xt r (f x) with the limitation that f must not and is not allowed to record accesses to the transaction log.

val exchange : xt:'x t -> 'a Loc.t -> 'a -> 'a

exchange ~xt r v is equivalent to update ~xt r (fun _ -> v).

val fetch_and_add : xt:'c t -> int Loc.t -> int -> int

fetch_and_add ~xt r n is equivalent to update ~xt r ((+) n).

val incr : xt:'x t -> int Loc.t -> unit

incr ~xt r is equivalent to fetch_and_add ~xt r 1 |> ignore.

val decr : xt:'x t -> int Loc.t -> unit

decr ~xt r is equivalent to fetch_and_add ~xt r (-1) |> ignore.

Performing accesses

type 'a tx = {
  1. tx : 'x. xt:'x t -> 'a;
}

Type of a transaction function that is polymorphic with respect to an explicit transaction log. The universal quantification helps to ensure that the transaction log cannot accidentally escape.

val call : 'a tx -> xt:'x t -> 'a

call ~xt tx is equivalent to tx.Xt.tx ~xt.

val attempt : ?mode:Mode.t -> 'a tx -> 'a

attempt tx attempts to atomically perform the transaction over shared memory locations recorded by calling tx with a fresh explicit transaction log. If used in Mode.obstruction_free may raise Mode.Interference. Otherwise either raises Exit on failure to commit the transaction or returns the result of the transaction. The default for attempt is Mode.lock_free.

val commit : ?backoff:Backoff.t -> ?mode:Mode.t -> 'a tx -> 'a

commit tx repeats attempt tx until it does not raise Exit or Mode.Interference and then either returns or raises whatever attempt returned or raised.

The default for commit is Mode.obstruction_free. However, after enough attempts have failed during the verification step, commit switches to Mode.lock_free.

Note that, aside from using exponential backoff to reduce contention, the transaction mechanism has no way to intelligently wait until shared memory locations are modified by other domains.

Conversions

val of_tx : 'a Tx.t -> xt:'x t -> 'a

of_tx tx converts the given Tx transaction tx to an explicit log passing function.

val to_tx : 'a tx -> 'a Tx.t

to_tx tx converts the given explicit log passing function tx to a Tx transaction.