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.
(build-wrappers history models transitions)
Computes a map of models to wrappers around those models. Does not link wrappers in a succession graph; use link-wrappers! to build the graph.
Computes a map of models to wrappers around those models. Does not link wrappers in a succession graph; use link-wrappers! to build the graph.
(canonical-history history)
(canonical-history history history' fs values)
Returns a copy of history where all equal :fs and :values are replaced by identical objects.
Returns a copy of history where all equal :fs and :values are replaced by identical objects.
(expand-models transitions models)
Given a coll of transitions and a set of models, returns a lazy sequence of every model reachable by applying any transition to any model.
Given a coll of transitions and a set of models, returns a lazy sequence of every model reachable by applying any transition to any model.
(link-wrappers! models->wrappers transitions)
Fills in the successors graph for a set of wrappers. Takes a map of models to wrappers and an array of transitions. Mutates wrappers in place.
Fills in the successors graph for a set of wrappers. Takes a map of models to wrappers and an array of transitions. Mutates wrappers in place.
We want to avoid burning too much time, or memory, on this memoization process. If we think a history may have more than this many reachable states, we don't bother memoizing.
We want to avoid burning too much time, or memory, on this memoization process. If we think a history may have more than this many reachable states, we don't bother memoizing.
(memo model history)
Given an initial model and a history, explores the state space exhaustively. Returns a map with:
:history a version of the history compatible with the returned model. :wrapper a Model and Wrapper which can be used in place of the original model. Only compatible with the history provided.
Guarantees that the wrapper linearizes equivalently to the given model, and that (unwrap wrapper) will return the equivalent model at any point in the search.
If the state space is too large to memoize, the returned model will be the original model m. (unwrap m) will return m in this case.
Given an initial model and a history, explores the state space exhaustively. Returns a map with: :history a version of the history compatible with the returned model. :wrapper a Model and Wrapper which can be used in place of the original model. Only compatible with the history provided. Guarantees that the wrapper linearizes equivalently to the given model, and that (unwrap wrapper) will return the equivalent model at any point in the search. If the state space is too large to memoize, the returned model will be the original model m. (unwrap m) will return m in this case.
(models transitions model)
Given a coll of transitions and an initial model, computes the complete set of all reachable models.
Given a coll of transitions and an initial model, computes the complete set of all reachable models.
(op->transition op)
Maps an operation to a state transition: just its :f and :value.
Maps an operation to a state transition: just its :f and :value.
(transition-index history transitions)
Given a history and an array of transitions, computes an int array mapping each invocation's :index to the index of the corresponding transition.
Given a history and an array of transitions, computes an int array mapping each invocation's :index to the index of the corresponding transition.
(transitions history)
A set of all unique {:f f :value value} transitions for invocations in a history.
A set of all unique {:f f :value value} transitions for invocations in a history.
(unwrap x)
If x is a Wrapper, return its underlying model. Otherwise, returns x.
If x is a Wrapper, return its underlying model. Otherwise, returns x.
(wrapper model history)
Given a model and a history, returns a Wrapper for that model over that history.
Given a model and a history, returns a Wrapper for that model over that history.
cljdoc is a website building & hosting documentation for Clojure/Script libraries
× close