Transactions on shared memory locations.
Type of transactions on shared memory locations.
Here is an example of unconditionally
committing a transaction that swaps the values of the two shared memory locations
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
get y_loc and
set y_loc x are intentionally one after the other, because the internal log used within transactions to record
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
forgets the access in case
x_loc had a negative value and then reads
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 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.
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_as g r v is equivalent to
update r (fun _ -> v) |> map g.
val return : 'a -> 'a t
return v is a transactional operation whose result is the value
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
( 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).
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)
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 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
(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.
val forget : 'a t
forget is equivalent to
delay (fun () -> raise Exit).
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
commit tx repeats
attempt tx until it does not raise
Mode.Interference and then either returns or raises whatever attempt returned or raised.
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.