Type of transactions on shared memory locations.

A transaction can be thought of as a specification of a sequence of get and set accesses to shared memory locations that can be attempted to perform the accesses atomically.

Transactions can be composed both sequentially (see let*) and conditionally (see (<|>) and forget).

Here is an example of unconditionally committing a transaction that swaps the values of the two shared memory locations x_loc and y_loc and returns their sum:

  commit begin
    let* x = get x_loc
    and* y = get y_loc in
    let+ () = set y_loc x
    and+ () = set x_loc y in
    x + y
  end

Above, get y_loc and set y_loc x are intentionally one after the other, because the internal log used within transactions to record gets and sets is optimized for accessing recently accessed elements again.

Here is an example of attempting a conditional transaction

  attempt begin
    begin
      let* x = get x_loc in
      if x < 0 then
        forget
      else
        return x
    end
    <|> get y_loc
  end

that reads x_loc, but forgets the access in case x_loc had a negative value and then reads y_loc instead.

What does that actually mean? Let's assume x_loc initially contains a negative value. During the first phase of the transaction x_loc is read and is found to be negative. The access is forgotten. Let's assume that after that the value of x_loc is modified by some other domain. The transaction continues to read y_loc and results in the value of y_loc. The transaction is allowed to commit despite the value of x_loc having been changed during the transaction.

Consider the following similar looking conditional transaction attempt:

  attempt begin
    let* x = get x_loc in
    if x < 0 then
      get y_loc
    else
      return x
  end

If some other domain modifies x_loc after it has been read by the above transaction attempt, then the commit phase will fail, because the access of x_loc is found to be inconsistent.

Note that neither of the above conditional examples is generally preferred, because they have fundamentally different semantics and the choice of whether accesses should, should not, or may be safely forgotten depends on what the desired semantics are for the transaction.

get r accesses the shared memory location r inside the transaction and results in the current value of r inside the transaction.

get_as g r is equivalent to get r |> map g.

set r v accesses the shared memory location r inside the transaction and sets the current value of r to the value v inside the transaction.

update r f is equivalent to let* x = get r in let+ () = set r (f x) in x.

update_as g r f is equivalent to update r f |> map g.

modify r f is equivalent to let* x = get r in set r (f x).

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

exchange_as g r v is equivalent to update r (fun _ -> v) |> map g.

return v is a transactional operation whose result is the value v.

let* x = x_tx in to_y_tx x is the sequential composition of the transaction x_tx with the transaction to_y_tx x computed from the result x of x_tx.

( and* ) x_tx tx_y is a transaction that performs both the transaction x_tx and the transaction tx_y and returns a pair of their results.

let+ x = tx in fn x is equivalent to let* x = tx in return (fn x).

and+ is a synonym for and* for use with let+.

u_tx >> x_tx is equivalent to let* _ = u_tx in x_tx.

u_tx >>. x is equivalent to let+ _ = u_tx in x.

>>= is a synonym for let*.

map xy x_tx is equivalent to let+ x = x_tx in xy x.

delay to_tx is equivalent to let* () = return () in to_tx ()

try_in e_to_y_tx x_to_y_tx x_tx is for handling exceptions during the access log recording phase of running a transaction. In case the transaction x_tx raises during the first phase, the accesses from x_tx are forgotten.

try_in e_to_y_tx x_to_y_tx x_tx is the equivalent of

  match run_phase_1 x_tx with
  | x -> run_phase_1 (x_to_y_tx x)
  | exception e -> run_phase_1 (e_to_y_tx e)

for transactions.

Note that the order of parameters is chosen with the following style in mind:

  transaction
  |> try_in (fun exn -> (* handle failure *)) @@ fun value ->
     (* continue successfully *)

l_tx <|> r_tx is a left-biased choice between the two transactions l_tx and r_tx.

If the l_tx transaction successfully produces a log of operations in the first phase of attempt, then those are attempted in the second phase. On the other hand, if the l_tx transaction raises Exit, then the choice acts like r_tx.

For example, (set x_loc x >> forget) <|> r_tx is equivalent to r_tx meaning that the set x_loc x access will not be part of the operations attempted in the second phase of a transaction.

forget is equivalent to delay (fun () -> raise Exit).

The name forget was chosen to give the idea that this causes the transaction to forget any accesses made during the forgotten part of a transaction.

attempt tx attempts to atomically perform the given transaction over shared memory locations. 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.