package dscheck

  1. Overview
  2. Docs

Module Dscheck.TracedAtomicSource

Sourcetype !'a t

An atomic (mutable) reference to a value of type 'a.

Sourceval make : 'a -> 'a t

Create an atomic reference.

Sourceval make_contended : 'a -> 'a t

Create an atomic reference that is alone on a cache line. It occupies 4-16x the memory of one allocated with make v.

The primary purpose is to prevent false-sharing and the resulting performance degradation. When a CPU performs an atomic operation, it temporarily takes ownership of an entire cache line that contains the atomic reference. If multiple atomic references share the same cache line, modifying these disjoint memory regions simultaneously becomes impossible, which can create a bottleneck. Hence, as a general guideline, if an atomic reference is experiencing contention, assigning it its own cache line may enhance performance.

Sourceval get : 'a t -> 'a

Get the current value of the atomic reference.

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

Set a new value for the atomic reference.

Sourceval exchange : 'a t -> 'a -> 'a

Set a new value for the atomic reference, and return the current value.

Sourceval compare_and_set : 'a t -> 'a -> 'a -> bool

compare_and_set r seen v sets the new value of r to v only if its current value is physically equal to seen -- the comparison and the set occur atomically. Returns true if the comparison succeeded (so the set happened) and false otherwise.

Sourceval fetch_and_add : int t -> int -> int

fetch_and_add r n atomically increments the value of r by n, and returns the current value (before the increment).

Sourceval incr : int t -> unit

incr r atomically increments the value of r by 1.

Sourceval decr : int t -> unit

decr r atomically decrements the value of r by 1.

Sourceval trace : ?impl:[ `Random of int | `Dpor | `Dpor_source ] -> ?interleavings:out_channel -> ?record_traces:bool -> (unit -> unit) -> unit

trace ?interleavings ?record_traces f starts the simulation trace.

impl lets user choose the underlying exploration algorithm.

If interleavings output channel is provided, DSCheck will continously print the visited interleavings there.

record_traces enables Trace_tracker, which is typically used for testing DSCheck itself.

Sourceval spawn : (unit -> unit) -> unit

spawn f as a new 'thread'

Sourceval check : (unit -> bool) -> unit

if f returns false then an assertion has failed

Sourceval final : (unit -> unit) -> unit

run f after all processes complete

Sourceval every : (unit -> unit) -> unit

run f between every possible interleaving