A model specifies the behavior of a singlethreaded datatype, transitioning from one state to another given an operation.
A model specifies the behavior of a singlethreaded datatype, transitioning from one state to another given an operation.
(cas-register)(cas-register value)A compare-and-set register
A compare-and-set register
(inconsistent msg)Represents an invalid termination of a model; e.g. that an operation could not have taken place.
Represents an invalid termination of a model; e.g. that an operation could not have taken place.
(inconsistent? model)Is a model inconsistent?
Is a model inconsistent?
(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.
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)A single mutex responding to :acquire and :release messages
A single mutex responding to :acquire and :release messages
A model which always returns itself, unchanged.
A model which always returns itself, unchanged.
(set)A set which responds to :add and :read.
A set which responds to :add and :read.
(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.
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)A queue which does not order its pending elements.
A queue which does not order its pending elements.
cljdoc builds & hosts documentation for Clojure/Script libraries
| Ctrl+k | Jump to recent docs |
| ← | Move to previous article |
| → | Move to next article |
| Ctrl+/ | Jump to the search field |