Validates that a history is correct with respect to some model.
Validates that a history is correct with respect to some model.
(check-safe checker test history)
(check-safe checker test history opts)
Like check, but wraps exceptions up and returns them as a map like
{:valid? :unknown :error "..."}
Like check, but wraps exceptions up and returns them as a map like {:valid? :unknown :error "..."}
(check checker test history opts)
Verify the history is correct. Returns a map like
{:valid? true}
or
{:valid? false :some-details ... :failed-at [details of specific operations]}
Opts is a map of options controlling checker execution. Keys include:
:subdirectory - A directory within this test's store directory where output files should be written. Defaults to nil.
DEPRECATED Checkers should now implement the 4-arity check method
without model. If the checker still needs a model, provide it at
construction rather than as an argument to Checker/check
. See the
queue and linearizable checkers for examples.
Verify the history is correct. Returns a map like {:valid? true} or {:valid? false :some-details ... :failed-at [details of specific operations]} Opts is a map of options controlling checker execution. Keys include: :subdirectory - A directory within this test's store directory where output files should be written. Defaults to nil. DEPRECATED Checkers should now implement the 4-arity check method without model. If the checker still needs a model, provide it at construction rather than as an argument to `Checker/check`. See the queue and linearizable checkers for examples.
(clock-plot)
Plots clock offsets on all nodes
Plots clock offsets on all nodes
(compose checker-map)
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 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.
(concurrency-limit limit checker)
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.
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.
(counter)
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 attempted decrements, and lower than the sum of all attempted increments and :ok decrements.
Returns a map:
{:valid? Whether the counter remained within bounds :reads [[lower-bound read-value upper-bound] ...] :errors [[lower-bound read-value upper-bound] ...] :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 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 attempted decrements, and lower than the sum of all attempted increments and :ok decrements. Returns a map: {:valid? Whether the counter remained within bounds :reads [[lower-bound read-value upper-bound] ...] :errors [[lower-bound read-value upper-bound] ...] :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}
(expand-queue-drain-ops history)
Takes a history. Looks for :drain operations with their value being a collection of queue elements, and expands them to a sequence of :dequeue invoke/complete pairs.
Takes a history. Looks for :drain operations with their value being a collection of queue elements, and expands them to a sequence of :dequeue invoke/complete pairs.
(frequency-distribution points c)
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.
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.
(latency-graph)
(latency-graph opts)
Spits out graphs of latencies. Checker options take precedence over those passed in with this constructor.
Spits out graphs of latencies. Checker options take precedence over those passed in with this constructor.
(linearizable {:keys [algorithm model]})
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}
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}
(merge-valid valids)
Merge n :valid values, yielding the one with the highest priority.
Merge n :valid values, yielding the one with the highest priority.
(noop)
An empty checker that only returns nil.
An empty checker that only returns nil.
(perf)
(perf opts)
Composes various performance statistics. Checker options take precedence over those passed in with this constructor.
Composes various performance statistics. Checker options take precedence over those passed in with this constructor.
(queue model)
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).
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).
(rate-graph)
(rate-graph opts)
Spits out graphs of throughput over time. Checker options take precedence over those passed in with this constructor.
Spits out graphs of throughput over time. Checker options take precedence over those passed in with this constructor.
(set)
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.
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.
(set-full)
(set-full checker-opts)
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.
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.
(set-full-add element-state op)
(set-full-element op)
Given an add invocation, constructs a new set element state record to track that element
Given an add invocation, constructs a new set element state record to track that element
(set-full-element-results e)
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 a SetFullElement and computes a map of final results from it: :element The element itself :outcome :stable, :lost, :never-read :lost-latency :stable-latency
(set-full-read-absent element-state inv op)
(set-full-read-present element-state inv op)
(set-full-results opts elements)
Takes options from set-full, and a collection of SetFullElements. Computes agggregate results; see set-full for details.
Takes options from set-full, and a collection of SetFullElements. Computes agggregate results; see set-full for details.
(total-queue)
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).
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).
(unbridled-optimism)
Everything is awesoooommmmme!
Everything is awesoooommmmme!
(unique-ids)
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]}
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.
A map of :valid? values to their importance. Larger numbers are considered more signficant and dominate when checkers are composed.
cljdoc is a website building & hosting documentation for Clojure/Script libraries
× close