knossos.model — knossos 0.3.9

A model specifies the behavior of a singlethreaded datatype, transitioning from one state to another given an operation.

cas-register clj

(cas-register)

(cas-register value)

A compare-and-set register

fifo-queue clj

(fifo-queue)

A FIFO queue.

inconsistent clj

(inconsistent msg)

Represents an invalid termination of a model; e.g. that an operation could not have taken place.

inconsistent? clj

(inconsistent? model)

Is a model inconsistent?

multi-register clj

(multi-register values)

A register supporting read and write transactions over registers identified by keys. Takes a map of initial keys to values. Supports a single :f for ops, :txn, whose value is a transaction: a sequence of [f k v] tuples, where :f is :read or :write, k is a key, and v is a value. Nil reads are always legal.

mutex clj

(mutex)

A single mutex responding to :acquire and :release messages

noop clj

A model which always returns itself, unchanged.

register clj

(register)

(register x)

A read-write register.

set clj

(set)

A set which responds to :add and :read.

step clj

(step model op)

The job of a model is to validate that a sequence of operations applied to it is consistent. Each invocation of (step model op) returns a new state of the model, or, if the operation was inconsistent with the model's state, returns a (knossos/inconsistent msg). (reduce step model history) then validates that a particular history is valid, and returns the final state of the model.

Models should be a pure, deterministic function of their state and an operation's :f and :value.

unordered-queue clj

(unordered-queue)

A queue which does not order its pending elements.