package kcas

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

Auxiliary modules

module Backoff : module type of Backoff

Randomized exponential backoff mechanism.

module Retry : sig ... end

Retry support.

module Mode : sig ... end

Operating modes of the k-CAS-n-CMP algorithm.

Individual locations

Individual shared memory locations can be 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.
module Loc : sig ... end

Shared memory locations.

Manipulating multiple locations atomically

Multiple shared memory locations can be manipulated atomically using either

  • Xt, to explicitly pass a transaction log to record accesses, or
  • Op, to specify a list of primitive operations to perform.

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.

2. The second phase attempts to perform the operations atomically.

3. In Mode.obstruction_free a third phase verifies all read-only operations.

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 raises Mode.Interference, which is typically automatically handled by Xt.commit.

Composable transactions on multiple locations

The Xt module provides a way to implement composable transactions over shared memory locations. A transaction 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.

WARNING: Operations provided by the Loc module for accessing individual shared memory locations are not transactional. There are cases where it can be advantageous to perform operations along with a transaction that do not get recorded into the transaction log, but doing so requires one to reason about the potential parallel interleavings of operations.

Transactions should also 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.

module Xt : sig ... end

Explicit transaction log passing on shared memory locations.

Multi-word compare-and-set operations

The Op module provides a multi-word compare-and-set (MCAS) interface for manipulating multiple locations atomically. This is a low-level interface not intended for most users.

module Op : sig ... end

Multi-word compare-and-set operations on shared memory locations.