knossos.core — org.clojars.khdegraaf/knossos 0.2.9.2-SNAPSHOT

advance-world clj

(advance-world world ops)

Given a world and a series of operations, applies those operations to the given world. The returned world will have a new model reflecting its state with the given operations applied, and its fixed history will have the given history appended. Those ops will also be absent from its pending operations.

analysis clj

(analysis model history)

Returns a map of information about the linearizability of a history. Completes the history and searches for a linearization.

awfulness clj

(awfulness world)

How bad is this world to explore?

degenerate-world-key clj

(degenerate-world-key world)

An object which uniquely identifies whether or not a world is linearizable. If two worlds have the same degenerate-world-key (in the context of a history), their linearizability is equivalent.

Here we take advantage of the fact that worlds with equivalent pending operations and equivalent positions in the history will linearize equivalently regardless of exactly what fixed path we took to get to this point. This degeneracy allows us to dramatically prune the search space.

explode-then-prune-world clj

(explode-then-prune-world history seen deepest stats world)

Given a history and a world, generates a reducible sequence of possible subseqeuent worlds, obtained in two phases:

1. If the next operation in the history for this world is an invocation, we find all possible subsequent worlds as a result of that invocation.

2. For all immediately subsequent ok, fail, and info operations, use those operations to prune and further advance the worlds from phase 1.

explore-world! clj

(explore-world! history running? leaders seen deepest stats world)

Explores a world's direct successors, reinjecting each into leaders. Returns the number of worlds reinserted into leaders. Uses the seen cache to avoid exploring worlds already visited. Updates deepest with new worlds at the highest index in the history. Guarantees that by return time, all worlds reinjected into leaders will be known to be extant.

explorer clj

(explorer history running? leaders seen deepest stats i)

Pulls worlds off of the leader atom, explores them, and pushes resulting worlds back onto the leader atom.

fail-op clj

fail? clj

fold-completion-into-world clj

(fold-completion-into-world world completion)

Given a world and a completion operation, returns world if the operation took place in that world, else nil. Advances the world index by one.

fold-completion-into-worlds clj

(fold-completion-into-worlds worlds completion)

Given a sequence of worlds and a completion operation, returns only those worlds where that operation took place; e.g. is not still pending.

TODO: replace the corresponding element in the history with the completion.

fold-failure-into-world clj

(fold-failure-into-world world failure)

Given a world and a failed operation, returns world if the operation did not take place, and removes the operation from the pending ops in that world. Advances world index by one.

Note that a failed operation is an operation which is known to have failed; e.g. the system guarantees that it did not take place. This is different from an indeterminate failure.

fold-failure-into-worlds clj

(fold-failure-into-worlds worlds failure)

Given a sequence of worlds and a failed operation, returns only those worlds where that operation did not take place, and removes the operation from the pending ops in those worlds.

fold-info-into-world clj

(fold-info-into-world world info)

Given a world and an info operation, returns a subsequent world. Info operations don't appear in the fixed history; only the index advances.

fold-invocation-into-world clj

(fold-invocation-into-world world invocation)

Given a world and a new invoke operation, adds the operation to the pending set for the world, and yields a collection of all possible worlds from that. Increments world index.

fold-op-into-world clj

(fold-op-into-world world op)

Given a world and any type of operation, folds that operation into the world and returns a sequence of possible worlds. Increments the world index.

fold-op-into-worlds clj

(fold-op-into-worlds worlds op)

Given a set of worlds and any type of operation, folds that operation into the set and returns a new set of possible worlds.

inconsistent-world? clj

(inconsistent-world? world)

Is the model for this world in an inconsistent state?

invoke-op clj

invoke? clj

linearizable-prefix clj

(linearizable-prefix model history)

Computes the longest prefix of a history which is linearizable.

linearizable-prefix-and-worlds clj

(linearizable-prefix-and-worlds model history)

Returns a vector consisting of the longest linearizable prefix and the worlds just prior to exhaustion.

If you think about a lightning strike, where the history stretches from the initial state in the thundercloud to the final state somewhere in the ground, we're trying to find a path--any path--for a lightning bolt to jump from cloud to ground.

Given a world at the tip of the lightning bolt, we can reach out to several nearby worlds just slightly ahead of ours, using fold-op-into-world. If there are no worlds left, we've struck a dead end and that particular fork of the lightning bolt terminates. If there are worlds left, we want to explore them--but it's not clear in what order.

Moreover, some paths are more expensive to traverse than others. Worlds with a high number of pending operations, for instance, are particularly expensive because each step explores n! operations. If we can find a quicker path to ground, we should take it.

We do this by keeping a set of all incomplete worlds, and following the worlds that seem to be doing the best. We leave the hard worlds for later. Each thread pulls a world off of the incomplete set, explodes it into several new worlds, and pushes those worlds back into the set. We call this set leaders.

If we reach a world which has no future operations--whose index is equal to the length of the history--we've found a linearization and can terminate.

If we ever run out of leaders, then we know no linearization is possible. Disproving linearizability can be much more expensive than proving it; we have to keep trying and trying until every possible option has been exhausted.

linearizations clj

(linearizations model history)

Given a model and a history, returns all possible worlds where that history is linearizable. Brute-force, expensive, but deterministic, simple, and useful for short histories.

next-op clj

(next-op history world)

The next operation from the history to be applied to a world, based on the world's index, or nil when out of bounds.

ok-op clj

ok? clj

op clj

outof clj

(outof coll things-to-remove)

Like into, but uses disj on a hashset

possible-worlds clj

(possible-worlds world)

Given a world, generates all possible future worlds consistent with the given world's pending operations. For instance, in the world

{:fixed [:a :b] :pending [:c :d]}

We know :a and :b have already happened, but :c and :d could happen, in either order, so long as they occur after :a and :b. Here are the possible worlds:

None of them may have happened:

{:fixed [:a :b] :pending [:c :d]}

One of the two could have happened:

{:fixed [:a :b :c] :pending [:d]} {:fixed [:a :b :d] :pending [:c]}

Both could have happened:

{:fixed [:a :b :c :d] :pending []} {:fixed [:a :b :d :c] :pending []}

So: we are looking for the permutations of all subsets of all pending operations.

prune-world clj

(prune-world history seen deepest stats world)

Given a history and a world, advances the world through as many operations in the history as possible, without splitting into multiple worlds. Returns a new world (possibly the same as the input), or nil if the world was found to be inconsistent.

seen-world!? clj

(seen-world!? seen world)

Given a mutable hashmap of seen worlds, ensures that an entry exists for the given world, and returns truthy iff that world had already been seen.

short-circuit! clj

(short-circuit! history running? world)

If we've reached a world with an index as deep as the history, we can abort all threads immediately.

update-deepest-world! clj

(update-deepest-world! deepest world)

If this is the deepest world we've seen, add it to the deepest list.

world clj

(world model)

A world represents the state of the system at one particular point in time. It comprises a known timeline of operations, and a set of operations which are pending. Finally, there's an integer index which indicates the number of operations this world has consumed from the history.