knossos.wgl — knossos 0.3.9

An implementation of the Wing and Gong linearizability checker, plus Lowe's extensions, as described in

http://www.cs.cmu.edu/~wing/publications/WingGong93.pdf http://www.cs.ox.ac.uk/people/gavin.lowe/LinearizabiltyTesting/paper.pdf https://arxiv.org/pdf/1504.00204.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

bitset-highest-contiguous-linearized clj

(bitset-highest-contiguous-linearized b)

What's the highest entry-id this BitSet has linearized, such that every lower entry ID is also linearized? -1 if nothing linearized.

cache-config clj

(cache-config linearized model op)

check clj

(check model history state)

concurrent-ops-at clj

(concurrent-ops-at history target-op)

Given a history and a particular operation in that history, computes the set of invoke operations concurrent with that particular operation.

configurations-which-linearized-up-to clj

(configurations-which-linearized-up-to entry-id configs)

Filters a collection of configurations to only those which linearized every operation up to and including the given entry id.

final-paths clj

(final-paths history pair-index final-op configs indices)

We have a raw history, a final ok op which was nonlinearizable, and a collection of cache configurations. We're going to compute the set of potentially concurrent calls at the nonlinearizable ok operation.

Then we'll filter the configurations to those which got the furthest into the history. Each config tells us the state of the system after linearizing a set of operations. We take that state and apply all concurrent operations to it, in every possible order, ending with the final op which broke linearizability.

highest-contiguous-linearized-entry-id clj

(highest-contiguous-linearized-entry-id configs)

Finds the highest linearized entry id given a set of CacheConfigs. -1 if no entries linearized. Because our search is speculative, we may actually try linearizing random high entry IDs even though we can't linearize smaller ones. For that reason, we use the highest contiguous entry ID.

history-without-linearized clj

(history-without-linearized history linearized)

Takes a history and a linearized bitset, and constructs a sequence over that history with already linearized operations removed.

invalid-analysis clj

(invalid-analysis history configs state)

Constructs an analysis of an invalid terminal state.

invoke-and-ok-for-entry-id clj

(invoke-and-ok-for-entry-id history entry-id)

Given a history and an entry ID, finds the [invocation completion] operation for that entry ID.

linearized clj

(linearized c)

map->Op clj

(map->Op m)

Construct an Op from a map.

max-entry-id clj

(max-entry-id history)

What's the highest entry ID in this history?

Op->map clj

(Op->map op)

Turns an Op back into a plain old map, stripping its entry ids.

render-op clj

(render-op indices op)

Prepares an op to be returned by converting it to a plain old map and reassigning its external index

start-analysis clj

(start-analysis model history)

Spawn a thread to check a history. Returns a Search.

with-entry-ids clj

(with-entry-ids history)

Assigns a sequential :entry-id to every invocation and completion. We're going to pick these ids in a sort of subtle way, because when it comes time to identify the point where we got stuck in the search, we want to be able to look at a linearized bitset and quickly identify the highest OK operation we linearized. To that end, we assign ok invocations the range 0..c, and crashed operations c+1..n, such that contiguous ranges of linearized ops represent progress through every required OK operation in the history.