package kcas

Auxiliary modules

Individual locations

Individual shared memory locations can be manipulated through the Loc module that is essentially compatible with the Stdlib Atomic module.

Manipulating multiple locations atomically

Multiple shared memory locations can be manipulated atomically using either

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

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.

Composable transactions on multiple locations

The Tx and Xt modules provide two different ways to implement composable transactions over shared memory locations. Using either of those one essentially declares a transaction that specifies how to access shared memory locations. To actually perform the accesses one then separately commits the transaction.

Accesses of shared memory locations inside either form of transaction should generally use the access operations, such as Tx.get and Xt.get, provided by the corresponding module. 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.

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.