knossos.linear
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
analysisclj
(analysis model history)Given an initial model state and a history, checks to see if the history is linearizable. Returns a map with a :valid? bool and a :config configset from its final state, plus an offending :op if an operation forced the analyzer to discover there are no linearizable paths.
Given an initial model state and a history, checks to see if the history is linearizable. Returns a map with a :valid? bool and a :config configset from its final state, plus an offending :op if an operation forced the analyzer to discover there are no linearizable paths.
extend-pathclj
(extend-path prefix ops)Given a path and some operations, applies those operations to extend the path until hitting an inconsistent point.
Given a path and some operations, applies those operations to extend the path until hitting an inconsistent point.
final-pathsclj
(final-paths history op configs)When a search crashes, we have an operation which would not linearize even given all pending operations. We also have a series of configurations, each of which is comprised of a model and a process state, resulting from the completion of the last ok operation.
We can expand such a configuration into a set of paths, each ending in an inconsistent state transition. Normally, when we compute JIT linearizations, we drop inconsistent outcomes. Here we want to preserve them--and the paths that lead to them. Our aim is to show exhaustively why no configuration linearized.
Returns a set of paths, where a path is a sequence of transitions like:
{:op some-op
:model model-resulting-from-applying-op}
When a search crashes, we have an operation which would not linearize even
given all pending operations. We also have a series of configurations, each
of which is comprised of a model and a process state, resulting from the
completion of the last ok operation.
We can expand such a configuration into a set of paths, each ending in an
inconsistent state transition. Normally, when we compute JIT linearizations,
we drop inconsistent outcomes. Here we want to preserve them--and the paths
that lead to them. Our aim is to show exhaustively *why* no configuration
linearized.
Returns a set of paths, where a path is a sequence of transitions like:
{:op some-op
:model model-resulting-from-applying-op}final-paths-for-configclj
(final-paths-for-config prefix final config)Returns a set of final paths for a specific configuration.
Returns a set of final paths for a specific configuration.
jit-linearizationsclj
(jit-linearizations cache config final)(jit-linearizations cache final configs config)Takes an initial configuration, a collection of pending invocations, and a final invocation to linearize and return. Explores all orders of pending invocations, and returns a sequence of valid configurations with that final invocation linearized.
Takes an initial configuration, a collection of pending invocations, and a final invocation to linearize and return. Explores all orders of pending invocations, and returns a sequence of valid configurations with that final invocation linearized.
jit-linearizations-cacheclj
(jit-linearizations-cache)Construct a cache for memoizing jit-linearizations.
jit-linearizations is pure.
Assume we're processing a single ok operation with a given configset. Let c1 and c2 be two configs from that configset. If c1 and c2 wind up calling (at any depth), jit-linearizations for the same config, they'll see the same set of resulting configs, and perform the same final linearization and final return on each. We can skip one of them.
So, we construct a concurrent hashset here and use it to prune duplicate searches.
Construct a cache for memoizing jit-linearizations. jit-linearizations is pure. Assume we're processing a single ok operation with a given configset. Let c1 and c2 be two configs from that configset. If c1 and c2 wind up calling (at any depth), jit-linearizations for *the same config*, they'll see *the same* set of resulting configs, and perform *the same* final linearization and final return on each. We can skip one of them. So, we construct a concurrent hashset here and use it to prune duplicate searches.
parallel-thresholdclj
How many configs do we need before we start parallelizing?
How many configs do we need before we start parallelizing?
previous-okclj
(previous-ok history op)Given a history and an operation, looks backwards in the history to find the previous ok. Returns nil if there was none.
Given a history and an operation, looks backwards in the history to find the previous ok. Returns nil if there was none.
reporter!clj
(reporter! state)Spawns a reporting thread that periodically logs the state of the analysis. State is an atom with :running?, :configs, and :op.
Spawns a reporting thread that periodically logs the state of the analysis. State is an atom with :running?, :configs, and :op.
reporting-intervalclj
How long (in ms) to sleep between status updates
How long (in ms) to sleep between status updates
stepclj
(step history state cache configs op)Advance one step through the history. Takes a configset, returns a new configset--or a reduced failure.
Advance one step through the history. Takes a configset, returns a new configset--or a reduced failure.
step-ok!clj
(step-ok! cache config-set config ok)Takes a jit cache, a ConfigSet, a config and an ok operation. If the
operation has already been linearized, returns a ConfigSet containing only
configuration, but with the ok op removed from the config's rets.
If the operation hasn't been linearized yet, takes all pending calls from other threads and linearizes them in each possible order, creating a set of new configurations. Finally, attempts to linearize and return the given operation on each of those configs.
Returns the ConfigSet.
Takes a jit cache, a ConfigSet, a config and an ok operation. If the operation has already been linearized, returns a ConfigSet containing only `configuration`, but with the ok op removed from the config's rets. If the operation hasn't been linearized yet, takes all pending calls from other threads and linearizes them in each possible order, creating a set of new configurations. Finally, attempts to linearize and return the given operation on each of those configs. Returns the ConfigSet.
t-callclj
(t-call config op)If calls and rets contain no call for a process, that process can invoke an operation, generating a new configuration.
If calls and rets contain no call for a process, that process can invoke an operation, generating a new configuration.
t-linclj
(t-lin config op)A pending call can be linearized by transforming the current state, moving the invocation from calls to rets. Returns nil if linearizing this operation would be inconsistent. Updates last-lin-op for the config.
A pending call can be linearized by transforming the current state, moving the invocation from calls to rets. Returns nil if linearizing this operation would be inconsistent. Updates last-lin-op for the config.
t-retclj
(t-ret config op)A pending return can be completed. It's legal to provide an invocation or a completion here--all that matters is the :process
A pending return can be completed. It's legal to provide an invocation or a completion here--all that matters is the :process
cljdoc is a website building & hosting documentation for Clojure/Script libraries
× close