Like check, but wraps exceptions up and returns them as a map like

{:valid? :unknown :error {:via {:type clojure.lang.Exceptioninfo, …} …}

Plots clock offsets on all nodes

Takes a map of names to checkers, and returns a checker which runs each check (possibly in parallel) and returns a map of names to results; plus a top-level :valid? key which is true iff every checker considered the history valid.

Takes positive integer limit and a checker. Puts an upper bound on the number of concurrent executions of this checker. Use this when a checker is particularly thread or memory intensive, to reduce context switching and memory cost.

A counter starts at zero; add operations should increment it by that much, and reads should return the present value. This checker validates that at each read, the value is greater than the sum of all :ok increments, and lower than the sum of all attempted increments.

Note that this counter verifier assumes the value monotonically increases: decrements are not allowed.

Returns a map:

:valid? Whether the counter remained within bounds :reads [lower-bound read-value upper-bound …] :errors [lower-bound read-value upper-bound …]

; Not implemented, but might be nice:

:max-absolute-error The lower read upper where read falls furthest outside :max-relative-error Same, but with error computed as a fraction of the mean}

A Tesser fold which looks for :drain operations with their value being a collection of queue elements, and expands them to a sequence of :dequeue invoke/complete pairs.

Computes a map of percentiles (0–1, not 0–100, we’re not monsters) of a collection of numbers, taken at percentiles points. If the collection is empty, returns nil.

Spits out graphs of latencies. Checker options take precedence over those passed in with this constructor.

Validates linearizability with Knossos. Defaults to the competition checker, but can be controlled by passing either :linear or :wgl.

Takes an options map for arguments, ex. {:model (model/cas-register) :algorithm :wgl}

Takes a PCRE regular expression pattern (as a Pattern or string) and a filename. Checks the store directory for this test, and in each node directory (e.g. n1), examines the given file to see if it contains instances of the pattern. Returns :valid? true if no instances are found, and :valid? false otherwise, along with a :count of the number of matches, and a :matches list of maps, each with the node and matching string from the file.

(log-file-pattern-checker #“panic: (\w+)$” “db.log”)

{:valid? false :count 5 :matches {:node “n1” :line “panic: invariant violation” “invariant violation” …]}}

Merge n :valid values, yielding the one with the highest priority.

An empty checker that only returns nil.

Composes various performance statistics. Checker options take precedence over those passed in with this constructor.

Every dequeue must come from somewhere. Validates queue operations by assuming every non-failing enqueue succeeded, and only OK dequeues succeeded, then reducing the model with that history. Every subhistory of every queue should obey this property. Should probably be used with an unordered queue model, because we don’t look for alternate orderings. O(n).

Spits out graphs of throughput over time. Checker options take precedence over those passed in with this constructor.

Given a set of :add operations followed by a final :read, verifies that every successfully added element is present in the read, and that the read contains only elements for which an add was attempted.

A more rigorous set analysis. We allow :add operations which add a single element, and :reads which return all elements present at that time. For each element, we construct a timeline like so:

[nonexistent] ... [created] ... [present] ... [absent] ... [present] ...

For each element:

The add is the operation which added that element.

The known time is the completion time of the add, or first read, whichever is earlier.

The stable time is the time after which every read which begins observes the element. If every read beginning after the add time observes the element, the stable time is the add time. If the final read fails to observe the element, the stable time is nil.

A stable element is one which has a stable time.

The lost time is the time after which no operation observes that element. If the most final read observes the element, the lost time is nil.

A lost element is one which has a lost time.

An element can be either stable or lost, but not both.

The first read latency is 0 if the first read invoked after the add time observes the element. If the element is never observed, it is nil. Otherwise, the first read delay is the time from the completion of the write to the invocation of the first read.

The stable latency is the time between the add time and the stable time, or 0, whichever is greater.

Options are:

:linearizable?    If true, we expect this set to be linearizable, and
                  stale reads result in an invalid result.

Computes aggregate results:

:valid?               False if there were any lost elements.
                      :unknown if there were no lost *or* stale elements;
                      e.g. if the test never inserted anything, every
                      insert crashed, etc. For :linearizable? tests,
                      false if there were lost *or* stale elements.
:attempt-count        Number of attempted inserts
:stable-count         Number of elements which had a time after which
                      they were always found
:lost                 Elements which had a time after which
                      they were never found
:lost-count           Number of lost elements
:never-read           Elements where no read began after the time when
                      that element was known to have been inserted.
                      Includes elements which were never known to have
                      been inserted.
:never-read-count     Number of elements never read
:stale                Elements which failed to appear in a read beginning
                      after we knew the operation completed.
:stale-count          Number of stale elements.
:worst-stale          Detailed description of stale elements with the
                      highest stable latencies; e.g. which ones took the
                      longest to show up.
:stable-latencies     Map of quantiles to latencies, in milliseconds, it
                      took for elements to become stable. 0 indicates the
                      element was linearizable.
:lost-latencies       Map of quantiles to latencies, in milliseconds, it
                      took for elements to become lost. 0 indicates the
                      element was known to be inserted, but never
                      observed.

Given an add invocation, constructs a new set element state record to track that element

Takes a SetFullElement and computes a map of final results from it:

:element The element itself :outcome :stable, :lost, :never-read :lost-latency :stable-latency

Takes options from set-full, and a collection of SetFullElements. Computes agggregate results; see set-full for details.

Computes basic statistics about success and failure rates, both overall and broken down by :f. Results are valid only if every :f has at some :ok operations; otherwise they’re :unknown.

Helper for computing stats over a history or filtered history.

What goes in must come out. Verifies that every successful enqueue has a successful dequeue. Queues only obey this property if the history includes draining them completely. O(n).

Everything is awesoooommmmme!

Returns information about unhandled exceptions: a sequence of maps sorted in descending frequency order, each with:

:class    The class of the exception thrown
:count    How many of this exception we observed
:example  An example operation

Checks that a unique id generator actually emits unique IDs. Expects a history with :f :generate invocations matched by :ok responses with distinct IDs for their :values. IDs should be comparable. Returns

{:valid?              Were all IDs unique?
 :attempted-count     Number of attempted ID generation calls
 :acknowledged-count  Number of IDs actually returned successfully
 :duplicated-count    Number of IDs which were not distinct
 :duplicated          A map of some duplicate IDs to the number of times
                      they appeared--not complete for perf reasons :D
 :range               [lowest-id highest-id]}

A map of :valid? values to their importance. Larger numbers are considered more signficant and dominate when checkers are composed.