Xt (kcas.Kcas.Xt) (original) (raw)

Module Kcas.Xt

Explicit transaction log passing on shared memory locations.

This module provides a way to implement composable transactions over shared memory locations. A transaction is a function written by the library user and can be thought of as a specification of a sequence of Xt.get and Xt.set accesses to shared memory locations. To actually perform the accesses one then Xt.commits the transaction.

Transactions should generally not perform arbitrary side-effects, because when a transaction is committed it may be attempted multiple times meaning that the side-effects are also performed multiple times. Xt.post_commit can be used to perform an action only once after the transaction has been committed succesfully.

WARNING: To make it clear, the operations provided by the Loc module for accessing individual shared memory locations do not implicitly go through the transaction mechanism and should generally not be used within transactions. There are advanced algorithms where one might, within a transaction, perform operations that do not get recorded into the transaction log. Using such techniques correctly requires expert knowledge and is not recommended for casual users.

As an example, consider an implementation of doubly-linked circular lists. Instead of using a mutable field, ref, or Atomic.t, one would use a shared memory location, or Loc.t, for the pointers in the node type:

type 'a node = { succ : 'a node Loc.t; pred : 'a node Loc.t; datum : 'a }

To remove a node safely one wants to atomically update the succ and pred pointers of the predecessor and successor nodes and to also update the succ and pred pointers of a node to point to the node itself, so that removal becomes an idempotent operation. Using explicit transaction log passing one could implement the remove operation as follows:

let remove ~xt node =
  (* Read pointers to the predecessor and successor nodes: *)
  let pred = Xt.get ~xt node.pred in
  let succ = Xt.get ~xt node.succ in
  (* Update pointers in this node: *)
  Xt.set ~xt node.succ node;
  Xt.set ~xt node.pred node;
  (* Update pointers to this node: *)
  Xt.set ~xt pred.succ succ;
  Xt.set ~xt succ.pred pred

The labeled argument, ~xt, refers to the transaction log. Transactional operations like Xt.get and Xt.set are then recorded in that log. To actually remove a node, we need to commit the transaction

Xt.commit { tx = remove node }

which repeatedly calls the transaction function, tx, to record a transaction log and attempts to atomically perform it until it succeeds.

Notice that remove is not recursive. It doesn't have to account for failure or perform a backoff. It is also not necessary to know or keep track of what the previous values of locations were. All of that is taken care of for us by the transaction log and the Xt.commit function. Furthermore, remove can easily be called as a part of a more complex transaction.

type 'x t

Type of an explicit transaction log on shared memory locations.

Note that a transaction log itself is not safe against concurrent or parallel use and should generally only be used by a single thread of execution. If a new thread of execution is spawned inside a function recording shared memory accesses to a log and the new thread of execution 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 for the transaction attempt to succeed after it has seen such an inconsistent view of the shared memory locations.

To mitigate potential issues due to this read skew anomaly and due to very long running transactions, all of the access recording operations in this section periodically validate the entire transaction log when a previously accessed location is accessed again. 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](#type-t) -> 'a [Loc.t](../Loc/index.html#type-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](#type-t) -> 'a [Loc.t](../Loc/index.html#type-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](#type-t) -> 'a [Loc.t](../Loc/index.html#type-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](#type-t) -> 'a [Loc.t](../Loc/index.html#type-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](#type-t) -> 'a [Loc.t](../Loc/index.html#type-t) -> 'a -> 'a

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

val swap : xt:'x [t](#type-t) -> 'a [Loc.t](../Loc/index.html#type-t) -> 'a [Loc.t](../Loc/index.html#type-t) -> unit

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

val compare_and_set : xt:'x [t](#type-t) -> 'a [Loc.t](../Loc/index.html#type-t) -> 'a -> 'a -> bool

compare_and_set ~xt r before after is equivalent to compare_and_swap ~xt r before after == before.

val compare_and_swap : xt:'x [t](#type-t) -> 'a [Loc.t](../Loc/index.html#type-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:'x [t](#type-t) -> int [Loc.t](../Loc/index.html#type-t) -> int -> int

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

val incr : xt:'x [t](#type-t) -> int [Loc.t](../Loc/index.html#type-t) -> unit

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

val decr : xt:'x [t](#type-t) -> int [Loc.t](../Loc/index.html#type-t) -> unit

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

Blocking

val to_blocking : xt:'x [t](#type-t) -> (xt:'x [t](#type-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](#type-t) -> (xt:'x [t](#type-t) -> 'a) -> 'a option

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

Nested transactions

The transaction mechanism does not implicitly rollback changes recorded in the transaction log. Using snapshot and rollback it is possible to implement nested conditional transactions that may tentatively record changes in the transaction log and then later discard those changes.

type 'x snap

Type of a snapshot of a transaction log.

val snapshot : xt:'x [t](#type-t) -> 'x [snap](#type-snap)

snapshot ~xt returns a snapshot of the transaction log.

Taking a snapshot is a fast constant time O(1) operation.

val rollback : xt:'x [t](#type-t) -> 'x [snap](#type-snap) -> unit

rollback ~xt snap discards any changes of shared memory locations recorded in the transaction log after the snap was taken by snapshot.

Performing a rollback is potentially as expensive as linear time O(n) in the number of locations accessed, but, depending on the exact access patterns, may also be performed more quickly. The implementation is optimized with the assumption that a rollback is performed at most once per snapshot.

NOTE: Only changes are discarded. Any location newly accessed after the snapshot was taken will remain recorded in the log as a read-only entry.

val first : xt:'x [t](#type-t) -> (xt:'x [t](#type-t) -> 'a) list -> 'a

first ~xt txs calls each transaction in the given list in turn and either returns the value returned by the first transaction in the list or raises Retry.Later in case all of the transactions raised Retry.Later.

NOTE: first does not automatically rollback changes made by the transactions.

Post commit actions

val post_commit : xt:'x [t](#type-t) -> (unit -> unit) -> unit

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

Validation

val validate : xt:'x [t](#type-t) -> 'a [Loc.t](../Loc/index.html#type-t) -> unit

validate ~xt r determines whether the shared memory location r has been modified outside of the transaction and raises Retry.Invalid in case it has.

Due to the possibility of read skew, in cases where some important invariant should hold between two or more different shared memory locations, one may explicitly validate the locations, after reading all of them, to ensure that no read skew is possible.

Advanced

val is_in_log : xt:'x [t](#type-t) -> 'a [Loc.t](../Loc/index.html#type-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](#type-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 : xt:'x [t](#type-t) -> 'a [tx](#type-tx) -> 'a

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

val commit : ?timeoutf:float -> ?backoff:Backoff.t -> ?mode:[Mode.t](../Mode/index.html#type-t) -> 'a [tx](#type-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 or Retry.Invalid to explicitly request a retry or any other exception to abort the transaction.

The default mode for commit is `Obstruction_free. However, after enough attempts have failed during the verification step, commit switches to `Lock_free.