package kcas
Library
Module
Module type
Parameter
Class
Class type
Operations on shared memory locations.
make_cas r before after
is an operation that attempts to set the shared memory location r
to the after
value and succeeds if the current content of r
is the before
value.
make_cmp r expected
is an operation that succeeds if the current value of the shared memory location r
is the expected
value.
val get_id : t -> int
get_id op
returns the unique id of the shared memory reference targeted by the op
eration.
is_on_loc op r
determines whether the target of op
is the shared memory location r
.
val atomic : t -> bool
atomic op
attempts to perform the given operation atomically. Returns true
on success and false
on failure.
atomically ops
attempts to perform the given operations atomically. If used in Mode.obstruction_free
may raise Mode.Interference
. Otherwise returns true
on success and false
on failure. The default for atomically
is Mode.lock_free
.
The algorithm requires provided operations to follow a global total order. To eliminate a class of bugs, the operations are sorted automatically. If the operations are given in either ascending or descending order of the targeted shared memory location ids, then sorting is done in linear time O(n)
and does not increase the time complexity of the algorithm. Otherwise sorting may take linearithmic time O(n*log(n))
.