Module KcasSource

Sourcetype 'a ref

Type of shared memory reference

Sourcetype t

Type of compare and swap value

Sourcetype 'a cas_result =
  1. | Aborted
  2. | Failed
  3. | Success of 'a

The type of CAS result.

Sourceval ref : 'a -> 'a ref

ref x returns a reference on a shared memory ceils containing the value x

Sourceval equal : 'a ref -> 'b ref -> bool
Sourceval is_on_ref : t -> 'a ref -> bool
Sourceval mk_cas : 'a ref -> 'a -> 'a -> t

mk_cas a o n returns a new CAS value, which when performed, updates the reference a to n if the current content of a is o

Sourceval set : 'a ref -> 'a -> unit

set r n updates the reference r to value n directly. Not Safe to use with shared memory !

Sourceval cas : 'a ref -> 'a -> 'a -> bool

cas r e u updates the reference r to value u if the current content of r is e.

Sourceval commit : t -> bool

commit c performs the CAS c and returns true if the CAS is successful.

Sourceval kCAS : t list -> bool

kCAS l performs a lock-free multi-word CAS and returns true if the multi-word CAS is successful.

kCAS requires ref of provided operations to follow a global total order. To eliminate a class of bugs kCAS presorts provided operations. If the operations are given in either ascending or descending order of get_id then the presort is done in linear time O(n). Otherwise presort may take linearithmic time O(n log n).

Sourceval get : 'a ref -> 'a

get a reads the value contained in reference a.

Sourceval get_id : 'a ref -> int

get_id a returns the unique id of the reference a.

Sourceval try_map : 'a ref -> ('a -> 'a option) -> 'a cas_result

try_map r f invokes f c, where c is the result of get r. If the result of f c is None, then Aborted is returned. If the result of f c is Some v, then attempt to CAS update r from c to v. If the CAS succeeds, then Success c is returned. If the CAS fails, then Failed is returned.

Sourceval map : 'a ref -> ('a -> 'a option) -> 'a cas_result

Like try_map but retries on CAS failure. Hence, map r f never returns Failed.

Sourceval incr : int ref -> unit

incr r atomically increments r

Sourceval decr : int ref -> unit

decr r atomically decrements r

Sourcemodule type Backoff = sig ... end
Sourcemodule type W1 = sig ... end
Sourcemodule W1 : W1