Module Stm

module Stm: sig .. end

type 'a stm 

The type of a transaction, when executed will produce a result of type 'a.

val return : 'a -> 'a stm

Primitive to wrap a plain of type 'a value to a 'a stm, which when being executed, will produces the orignal value.

val bind : 'a stm -> ('a -> 'b stm) -> 'b stm

bind t f is a transaction, when executed, first behavior as transaction t, then feed the reture value to f to get the consecutive transaction to execute next.

val (>>=) : 'a stm -> ('a -> 'b stm) -> 'b stm

t >>= f is an alternative notation of bind t f

val (>>) : 'a stm -> 'b stm -> 'b stm

t1 >> t2 is equal to t1 >>= fun _ -> t2 which first execute t1 and wait for its result but ignore it, and then behaviors like t2

val abort : 'a stm

abort is a single transaction, when executed, abort the whole execution from current point. The result of abort an execution is detailed in the documentation of execution primitive atom_once below.

val retry : 'a stm

retry is a transaction, when executed, first wait for the changing of any transactional variables being read in the history of current execution, then relaunch the whole execution.

val retry_now : 'a stm

retry_now is a transaction in the same spirit with retry, the only difference is that it does not wait for any changes and relaunch the execution immediately. This can be useful in a language with side-effect, see also the documentation on atom_once

val wait : unit stm

wait is a transaction, when executed, simply wait for the changing of any transactional variables being read in the history of current execution, but without relaunch it. Semantically, you can consider retry as wait >> retry_now

val or_else : 'a stm -> 'a stm -> 'a stm

or_else t1 t2 is a transaction, when executed, first try to execute t1. If not encountering any retry (retry_now) or abort, it behaviors just as t1, otherwise it try t2 in the same way. If both t1 and t2 abort, the whole execution will abort; if either of them retry_now, the whole execution will relaunch immediately; if either of them retry, the execution will wait on its waiting condition and then relaunch; if both of them retry, the execution will wait on both their waiting conditions and then relaunch.

val catch : 'a stm -> (exn -> 'a stm) -> 'a stm

catch t f is a transaction, when executed, behaviors as t if no exception arise, otherwise f is used to catch this exception and produce the replacing transaction to execute. Note that catch is transaction-level try ... with.

E.g., let t3 = t1 >>= fun x -> let y = possible_exn x in t2, here t3 is a transaction with potential exception inside, try t3 with ... won't catch it because t3 is not executed yet, and try atom_once t3 with ... can catch it but then t3 lost its composability. The solution is catch t3 (function _ -> t4) which catches exceptions inside t3 and results a valid transaction being able to furtherly composed; another possibility is to catch the exception normally outside transactions like t1 >>= fun x -> let y = try possible_exn x with _ -> some_value in t2.

val atom_once : 'a stm -> 'a option

atom_once execute a transaction and result in Some v if the transaction success and None if the transaction fail (due to conflicting in committing or abort). One difference between OCaml and Haskell is that OCaml is not pure and can hide side-effect anywhere while Haskell is pure and can seperate values with/without side-effect by types. On STM, any transaction may fail and relaunch for some times before its success, so any side-effects inside the transaction may be launched several times. Haskell forbid side effect inside transaction through types, whereas we won't be able to do that with OCaml. Instead of asking, but have no means to detect or forbid, the programmers to program without side-effect inside transaction, or modifying heavily the underlying run-time of a language with a imperative nature to be able to catch/revert side-effect, we simply tell it from type that "A transaction may fail" and let the programmer decide what to do. This kind of things already exist in OCaml such as exception. E.g. try incr i; danger_v1 with _ -> decr i; v2, it's the programmers' responsibility to revert i or choose not to do the side-effect modification inside a dangerous envrionment, if that's what they mean. On the other hand, the good thing is that now the programmers have more flexibility in controlling the execution of transactions, e.g. they may choose in purpose not to repeatedly execute the transaction after the committing fails x times.

val atom : 'a stm -> 'a

This is an analog of atomically in Haskell, which repeatedly execute a transaction until the committing succeed. As being said in atom_once, the control is given to the programmer, the atom can defined by themselves as let rec atom t = match atom_once t with Some v -> v | _ -> atom t. Providing it is just for convenience. In the same way, you can define various helper functions such as check.

As already warned (see atom_once, transactions may fail, relauching transactions also means relaunching side-effects inside a transaction if any. So usually you should avoid side-effect, unless it's something you don't care or even something you want: as an example, you may want to add a harmless print routine inside the transaction to be able to debug that how may times the transaction fails before its success :)

Unlike in haskell, we allow nested atom_once or atom.

type 'a tvar 

the type of transactional variable, which has inside a value of type 'a

val tvar : 'a -> 'a tvar

Toplevel tvar declaration, produce a transaction variable from a value. See new_tvar

val new_tvar : 'a -> 'a tvar stm

We provide two functions to create a transactional variable from common value: tvar is traditional toplevel declaration as those new* and create* functions seen in most other library, it is ensured to succeed; while new_tvar is a transactional declaration (as in Haskell) which may fail if the execution of the whole transaction it's bound in fails.

We do not follow the idea on the relation between tvar allocation and exception from the original STM paper (last paragraph of section 3.5), as we explicitly provide this two different declaration method: toplevel declaration tvar is ensured to be succeed; new_tvar is itself transactional, hence by no means should it be specially ensured to succeed always, if it's value is exposed after a fail transaction by exception etc, visiting it later will result in a Not_found exception, which exactly indicates what has happened: the new_tvar does not succeed.

val read_tvar : 'a tvar -> 'a stm

Read value from a transactional variable, results in a transaction which can be further composed with other transactions through bind etc., or executed right away with atom etc. to get the final result

val write_tvar : 'a tvar -> 'a -> unit stm

write_tvar tv v write value v to transactional variable tv, results in a transaction whose type is unit. As read_tvar, the result transaction is for composing or executing.

Warning: do not operate the value of a transactional variable though other way exception write_tvar: such as producing the tvar from a mutable value or reference and secretly changing it in traditional way. First, it breaks the transactional semantics; second, in all possibility you won't be able to do that, as the value of tvar is isolated.