# Module Stm

    module Stm: sig .. end

A user-space STM library for vmthreads, system threads, process and network programs(TODO).

STM model

    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`.

Transactional variable

    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.