package kcas

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.

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

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.

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.

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.

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

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

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

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

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.

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

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.

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.

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

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