module Stm:sig
..end
A user-space STM library for vmthreads, system threads, process and network programs(TODO).
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.