Liking cljdoc? Tell your friends :D

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
raw docstring

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.
sourceraw docstring

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.
sourceraw docstring

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}
sourceraw docstring

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.
sourceraw docstring

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.
sourceraw docstring

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.
sourceraw docstring

parallel-thresholdclj

How many configs do we need before we start parallelizing?

How many configs do we need before we start parallelizing?
sourceraw docstring

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.
sourceraw docstring

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.
sourceraw docstring

reporting-intervalclj

How long (in ms) to sleep between status updates

How long (in ms) to sleep between status updates
sourceraw docstring

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.
sourceraw docstring

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.
sourceraw docstring

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.
sourceraw docstring

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.
sourceraw docstring

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
sourceraw docstring

cljdoc is a website building & hosting documentation for Clojure/Script libraries

× close