package kcas

  1. Overview
  2. Docs

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.

It is important to understand that it is possible for a transaction to observe the contents of two (or more) different shared memory locations from two (or more) different committed updates. This means that invariants that hold between two (or more) different shared memory locations may be seen as broken inside the transaction function. However, it is not possible to commit a transaction after it has seen such an inconsistent view of the shared memory locations.

To mitigate potential issues due to this torn read anomaly and due to very long running transactions, all of the access recording operations in this section periodically validate the entire transaction log. An important guideline for writing transactions is that loops inside a transaction should always include an access of some shared memory location through the transaction log or should otherwise be guaranteed to be bounded.

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 access 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 access 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 swap : xt:'x t -> 'a Loc.t -> 'a Loc.t -> unit

swap ~xt l1 l2 is equivalent to set ~xt l1 @@ exchange ~xt l2 @@ get ~xt l1.

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

compare_and_swap ~xt r before after is equivalent to

update ~xt r @@ fun actual ->
if actual == before then after else actual
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.

Blocking

val to_blocking : xt:'x t -> (xt:'x t -> 'a option) -> 'a

to_blocking ~xt tx converts the non-blocking transaction tx to a blocking transaction by retrying on None.

val to_nonblocking : xt:'x t -> (xt:'x t -> 'a) -> 'a option

to_nonblocking ~xt tx converts the blocking transaction tx to a non-blocking transaction by returning None on retry.

Post commit actions

val post_commit : xt:'x t -> (unit -> unit) -> unit

post_commit ~xt action adds the action to be performed after the transaction has been performed successfully.

Advanced

val is_in_log : xt:'x t -> 'a Loc.t -> bool

is_in_log ~xt r determines whether the shared memory location r has been accessed by the transaction.

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 commit : ?backoff:Backoff.t -> ?mode:Mode.t -> 'a tx -> 'a

commit tx repeatedly calls tx to record a log of shared memory accesses and attempts to perform them atomically until it succeeds and then returns whatever tx returned. tx may raise Retry.Later to explicitly request a retry or any other exception to abort the transaction.

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 commit never raises the Mode.Interference exception.

OCaml

Innovation. Community. Security.