Documentation ¶
Index ¶
- func CheckEvents(model Model, history []Event) bool
- func CheckEventsVerbose(model Model, history []Event, timeout time.Duration) (CheckResult, LinearizationInfo)
- func CheckOperations(model Model, history []Operation) bool
- func CheckOperationsVerbose(model Model, history []Operation, timeout time.Duration) (CheckResult, LinearizationInfo)
- func Visualize(model Model, info LinearizationInfo, output io.Writer) error
- func VisualizePath(model Model, info LinearizationInfo, path string) error
- type CheckResult
- type Event
- type EventKind
- type LinearizationInfo
- type Model
- type Operation
Constants ¶
This section is empty.
Variables ¶
This section is empty.
Functions ¶
func CheckEvents ¶
CheckEvents checks whether a history is linearizable.
func CheckEventsVerbose ¶
func CheckEventsVerbose(model Model, history []Event, timeout time.Duration) (CheckResult, LinearizationInfo)
CheckEventsVerbose checks whether a history is linearizable while computing data that can be used to visualize the history and linearization.
The returned LinearizationInfo can be used with Visualize.
func CheckOperations ¶
CheckOperations checks whether a history is linearizable.
func CheckOperationsVerbose ¶
func CheckOperationsVerbose(model Model, history []Operation, timeout time.Duration) (CheckResult, LinearizationInfo)
CheckOperationsVerbose checks whether a history is linearizable while computing data that can be used to visualize the history and linearization.
The returned LinearizationInfo can be used with Visualize.
func Visualize ¶
func Visualize(model Model, info LinearizationInfo, output io.Writer) error
Visualize produces a visualization of a history and (partial) linearization as an HTML file that can be viewed in a web browser.
If the history is linearizable, the visualization shows the linearization of the history. If the history is not linearizable, the visualization shows partial linearizations and illegal linearization points.
To get the LinearizationInfo that this function requires, you can use CheckOperationsVerbose / CheckEventsVerbose.
This function writes the visualization, an HTML file with embedded JavaScript and data, to the given output.
func VisualizePath ¶
func VisualizePath(model Model, info LinearizationInfo, path string) error
VisualizePath is a wrapper around Visualize to write the visualization to a file path.
Types ¶
type CheckResult ¶
type CheckResult string
A CheckResult is the result of a linearizability check.
Checking for linearizability is decidable, but it is an NP-hard problem, so the checker might take a long time. If a timeout is not given, functions in this package will always return Ok or Illegal, but if a timeout is supplied, then some functions may return Unknown. Depending on the use case, you can interpret an Unknown result as Ok (i.e., the tool didn't find a linearizability violation within the given timeout).
const ( Unknown CheckResult = "Unknown" // timed out Ok CheckResult = "Ok" Illegal CheckResult = "Illegal" )
func CheckEventsTimeout ¶
func CheckEventsTimeout(model Model, history []Event, timeout time.Duration) CheckResult
CheckEventsTimeout checks whether a history is linearizable, with a timeout.
A timeout of 0 is interpreted as an unlimited timeout.
func CheckOperationsTimeout ¶
func CheckOperationsTimeout(model Model, history []Operation, timeout time.Duration) CheckResult
CheckOperationsTimeout checks whether a history is linearizable, with a timeout.
A timeout of 0 is interpreted as an unlimited timeout.
type Event ¶
type Event struct { ClientId int // optional, unless you want a visualization; zero-indexed Kind EventKind Value interface{} Id int }
An Event is an element of a history, a function call event or a return event.
This package supports two different representations of histories, as a sequence of Event or Operation. In the Event representation, function calls and returns are only relatively ordered and do not have absolute timestamps.
The Id field is used to match a function call event with its corresponding return event.
type EventKind ¶
type EventKind bool
An EventKind tags an Event as either a function call or a return.
type LinearizationInfo ¶ added in v0.1.6
type LinearizationInfo struct {
// contains filtered or unexported fields
}
type Model ¶
type Model struct { // Partition functions, such that a history is linearizable if and only // if each partition is linearizable. If left nil, this package will // skip partitioning. Partition func(history []Operation) [][]Operation PartitionEvent func(history []Event) [][]Event // Initial state of the system. Init func() interface{} // Step function for the system. Returns whether or not the system // could take this step with the given inputs and outputs and also // returns the new state. This function must be a pure function: it // cannot mutate the given state. Step func(state interface{}, input interface{}, output interface{}) (bool, interface{}) // Equality on states. If left nil, this package will use == as a // fallback ([ShallowEqual]). Equal func(state1, state2 interface{}) bool // For visualization, describe an operation as a string. For example, // "Get('x') -> 'y'". Can be omitted if you're not producing // visualizations. DescribeOperation func(input interface{}, output interface{}) string // For visualization purposes, describe a state as a string. For // example, "{'x' -> 'y', 'z' -> 'w'}". Can be omitted if you're not // producing visualizations. DescribeState func(state interface{}) string }
A Model is a sequential specification of a system.
Note: models in this package are expected to be purely functional. That is, the model Step function should not modify the given state (or input or output), but return a new state.
Only the Init, Step, and Equal functions are necessary to specify if you just want to test histories for linearizability.
Implementing the partition functions can greatly improve performance. If you're implementing the partition function, the model Init and Step functions can be per-partition. For example, if your specification is for a key-value store and you partition by key, then the per-partition state representation can just be a single value rather than a map.
Implementing DescribeOperation and DescribeState will produce nicer visualizations.
It may be helpful to look at this package's test code for examples of how to write models, including models that include partition functions.
type Operation ¶
type Operation struct { ClientId int // optional, unless you want a visualization; zero-indexed Input interface{} Call int64 // invocation timestamp Output interface{} Return int64 // response timestamp }
An Operation is an element of a history.
This package supports two different representations of histories, as a sequence of Operation or Event. In the Operation representation, function call/returns are packaged together, along with timestamps of when the function call was made and when the function call returned.