Shared functions for performing forensic reconstruction of a nonlinearizable history's final moments.
Shared functions for performing forensic reconstruction of a nonlinearizable history's final moments.
Command-line verification of edn histories.
Command-line verification of edn histories.
A checker which uses both WGL and linear analyses, terminating as soon as one has a decision.
A checker which uses both WGL and linear analyses, terminating as soon as one has a decision.
Operations on histories
Operations on histories
An implementation of the linear algorithm from http://www.cs.ox.ac.uk/people/gavin.lowe/LinearizabiltyTesting/paper.pdf
An implementation of the linear algorithm from http://www.cs.ox.ac.uk/people/gavin.lowe/LinearizabiltyTesting/paper.pdf
Datatypes for search configurations
Datatypes for search configurations
Constructs reports from a linear analysis.
When a linear analyzer terminates it gives us a set of configs, each of which consists of a model, a final operation, and a set of pending operations. Our job is to render those operations like so:
+---------+ +--------+
proc 0 | write 1 | | read 0 |
+---------+ +--------+
+---------+
proc 1 | write 0 |
+---------+
------------ time ---------->
Constructs reports from a linear analysis. When a linear analyzer terminates it gives us a set of configs, each of which consists of a model, a final operation, and a set of pending operations. Our job is to render those operations like so: +---------+ +--------+ proc 0 | write 1 | | read 0 | +---------+ +--------+ +---------+ proc 1 | write 0 | +---------+ ------------ time ---------->
Helps manage memory pressure
Helps manage memory pressure
A model specifies the behavior of a singlethreaded datatype, transitioning from one state to another given an operation.
A model specifies the behavior of a singlethreaded datatype, transitioning from one state to another given an operation.
We can spend a lot of time comparing models for equality, and constructing/GCing models. However, Jepsen tests generally have a relatively small state space. A register, for instance, might take on 5 integer values, and support 5 reads, 5 writes, and 5*5 compare-and-set transitions.
So let's do something sneaky. We can read over the history and compute an upper bound on its state space. If the space is sufficiently dense, we can simply precompute the entire state space and transitions and store them as a graph. That means:
This computation might be expensive, but we only have to do it once, and it can pay by speeding up the exponentially-complex search later.
We provide a Wrapper type which has the same state space structure as the underlying model, but much faster execution. You can perform your search using the Wrapper in place of the original Model, then call (model wrapper) to obtain the corresponding original Model for that state.
We can spend a lot of time comparing models for equality, and constructing/GCing models. However, Jepsen tests generally have a relatively small state space. A register, for instance, might take on 5 integer values, and support 5 reads, 5 writes, and 5*5 compare-and-set transitions. So let's do something sneaky. We can read over the history and compute an upper bound on its state space. If the space is sufficiently dense, we can simply *precompute* the entire state space and transitions and store them as a graph. That means: - We don't have to actually *run* the model for every transition--we can just walk the graph. - We can re-use a single copy of each state instead of a new one: fewer allocations! - Re-using the same arguments and states means we can use referential equality comparisons instead of =. - We can do truly evil things: because we've enumerated all reachable states, and all transitions, we can simply *number* them and represent their transitions as an array. A *small* array. We're talking a handful of cache lines, and it's immutable. :D This computation might be expensive, but we only have to do it once, and it can pay by speeding up the exponentially-complex search later. We provide a Wrapper type which has the same state space structure as the underlying model, but much faster execution. You can perform your search using the Wrapper in place of the original Model, then call (model wrapper) to obtain the corresponding original Model for that state.
Operations on operations!
An operation is comprised of a process
with a type
indicating whether it
is invoking, completing, failing, or noting progress of a function f
,
called with an argument value
. In addition, operations may have an :index
which identifies their position in a history, and carry extra keys.
Operations on operations! An operation is comprised of a `process` with a `type` indicating whether it is invoking, completing, failing, or noting progress of a function `f`, called with an argument `value`. In addition, operations may have an `:index` which identifies their position in a history, and carry extra keys.
A high-performance priority queue where only approximate ordering is required.
A high-performance priority queue where only approximate ordering is required.
Manages reporting and aborting searches
Manages reporting and aborting searches
Polymorphic interface for managing search lifecycles.
Polymorphic interface for managing search lifecycles.
Toolbox
Toolbox
A weakly consistent concurrent cache. We need an efficient way for many threads to let each other know what parts of the state space have already been explored.
With thanks to Coda Hale for his advice.
A weakly consistent concurrent cache. We need an efficient way for many threads to let each other know what parts of the state space have already been explored. With thanks to Coda Hale for his advice.
An implementation of the Wing and Gong linearizability checker, plus Lowe's extensions, as described in
http://www.cs.cmu.edu/~wing/publications/WingGong93.pdf http://www.cs.ox.ac.uk/people/gavin.lowe/LinearizabiltyTesting/paper.pdf https://arxiv.org/pdf/1504.00204.pdf
An implementation of the Wing and Gong linearizability checker, plus Lowe's extensions, as described in http://www.cs.cmu.edu/~wing/publications/WingGong93.pdf http://www.cs.ox.ac.uk/people/gavin.lowe/LinearizabiltyTesting/paper.pdf https://arxiv.org/pdf/1504.00204.pdf
A history traversal structure built around a mutable unsynchronized doubly linked list which supports O(1) removal and insertion of nodes.
A history traversal structure built around a mutable unsynchronized doubly linked list which supports O(1) removal and insertion of nodes.
cljdoc is a website building & hosting documentation for Clojure/Script libraries
× close