knossos.linear — knossos 0.3.9

An implementation of the linear algorithm from http://www.cs.ox.ac.uk/people/gavin.lowe/LinearizabiltyTesting/paper.pdf

analysis clj

(analysis model history)

(analysis model history opts)

Given an initial model state and a history, checks to see if the history is linearizable. Returns a map with a :valid? bool and additional debugging information.

Can also take an options map: {:time-limit ms} Duration to wait before returning with result :unknown

check clj

(check model history configs state)

final-paths clj

(final-paths history op configs indices)

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}

jit-linearizations clj

(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.

jit-linearizations-cache clj

(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.

parallel-threshold clj

How many configs do we need before we start parallelizing?

results-for-interrupted-state clj

(results-for-interrupted-state history configs state)

Computes a result map for an interrupted search.

start-analysis clj

(start-analysis model history)

Spawns a Search to check a history.

step clj

(step history state cache configs op)

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.

t-call clj

(t-call config op)

If calls and rets contain no call for a process, that process can invoke an operation, generating a new configuration.

t-lin clj

(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.

t-ret clj

(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