Struct stateright::semantics::LinearizabilityTester

pub struct LinearizabilityTester<ThreadId, RefObj: SequentialSpec> { /* private fields */ }

This tester captures a potentially concurrent history of operations and validates that it adheres to a SequentialSpec based on the linearizability consistency model. This model requires that operations be applied atomically and that sequenced (non-concurrent) operations are applied in order.

If you’re not sure whether to pick this or SequentialConsistencyTester, favor LinearizabilityTester.

Linearizability

Unlike with sequential consistency, all sequenced (non-concurrent) operations must respect a happens-before relationship, even across threads, which ensures that histories respect “real time” ordering (defined more precisely below). Anomalies are prevented because threads all agree on the viable order of operations. For example, the later read by Thread 2 must read the value of Thread 1’s write (rather than a differing earlier value) since those two operations are not concurrent:

          -----------Time------------------------------>
Thread 1: [write invoked... and returns]
Thread 2:                                 [read invoked... and returns]

While “real time” is a common way to phrase an implicit total ordering on non-concurrent events spanning threads, a more precise way to think about this is that prior to Thread 2 starting its read, Thread 1 is capable of communicating with Thread 2 indicating that the write finished. This perspective avoids introducing the notion of a shared global time, which is often a misleading perspective when it comes to distributed systems (or even modern physics in general).

The SequentialSpec will imply additional ordering constraints based on semantics specific to each operation. For example, a value cannot be popped off a stack before it is pushed. It is then the responsibility of this tester to establish whether a valid total ordering of events exists under these constraints.

See also: SequentialConsistencyTester.

Implementations

impl<T: Ord, RefObj: SequentialSpec> LinearizabilityTester<T, RefObj>

pub fn new(init_ref_obj: RefObj) -> Self

Constructs a LinearizabilityTester.

pub fn len(&self) -> usize

Indicates the aggregate number of operations completed or in flight across all threads.

impl<T, RefObj> LinearizabilityTester<T, RefObj>where T: Copy + Debug + Ord, RefObj: Clone + SequentialSpec, RefObj::Op: Clone + Debug, RefObj::Ret: Clone + Debug + PartialEq,

pub fn serialized_history(&self) -> Option<Vec<(RefObj::Op, RefObj::Ret)>>

Attempts to serialize the recorded partially ordered operation history into a total order that is consistent with a reference object’s operational semantics.

Trait Implementations

impl<ThreadId: Clone, RefObj: Clone + SequentialSpec> Clone for LinearizabilityTester<ThreadId, RefObj>where RefObj::Op: Clone, RefObj::Ret: Clone,

fn clone(&self) -> LinearizabilityTester<ThreadId, RefObj>

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl<T, RefObj> ConsistencyTester<T, RefObj> for LinearizabilityTester<T, RefObj>where T: Copy + Debug + Ord, RefObj: Clone + SequentialSpec, RefObj::Op: Clone + Debug, RefObj::Ret: Clone + Debug + PartialEq,

fn on_invoke( &mut self, thread_id: T, op: RefObj::Op ) -> Result<&mut Self, String>

Indicates that a thread invoked an operation. Returns Ok(...) if the history is valid, even if it is not lineariable.

See LinearizabilityTester::serialized_history.

fn on_return( &mut self, thread_id: T, ret: RefObj::Ret ) -> Result<&mut Self, String>

Indicates that a thread’s earlier operation invocation returned. Returns Ok(...) if the history is valid, even if it is not linearizable.

See LinearizabilityTester::serialized_history.

fn is_consistent(&self) -> bool

Indicates whether the recorded history is linearizable.

fn on_invret( &mut self, thread_id: T, op: RefObj::Op, ret: RefObj::Ret ) -> Result<&mut Self, String>

A helper that indicates both an operation and corresponding return value for a thread. Returns Ok(...) if the history is valid, even if it is not consistent.

impl<ThreadId: Debug, RefObj: Debug + SequentialSpec> Debug for LinearizabilityTester<ThreadId, RefObj>where RefObj::Op: Debug, RefObj::Ret: Debug,

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<T: Ord, RefObj> Default for LinearizabilityTester<T, RefObj>where RefObj: Default + SequentialSpec,

fn default() -> Self

Returns the “default value” for a type.

impl<ThreadId: Hash, RefObj: Hash + SequentialSpec> Hash for LinearizabilityTester<ThreadId, RefObj>where RefObj::Op: Hash, RefObj::Ret: Hash,

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl<ThreadId: PartialEq, RefObj: PartialEq + SequentialSpec> PartialEq<LinearizabilityTester<ThreadId, RefObj>> for LinearizabilityTester<ThreadId, RefObj>where RefObj::Op: PartialEq, RefObj::Ret: PartialEq,

fn eq(&self, other: &LinearizabilityTester<ThreadId, RefObj>) -> bool

This method tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

This method tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl<T, RefObj> Serialize for LinearizabilityTester<T, RefObj>where RefObj: Serialize + SequentialSpec, RefObj::Op: Serialize, RefObj::Ret: Serialize, T: Ord + Serialize,

fn serialize<Ser: Serializer>(&self, ser: Ser) -> Result<Ser::Ok, Ser::Error>

Serialize this value into the given Serde serializer.

impl<ThreadId: Eq, RefObj: Eq + SequentialSpec> Eq for LinearizabilityTester<ThreadId, RefObj>where RefObj::Op: Eq, RefObj::Ret: Eq,

impl<ThreadId, RefObj: SequentialSpec> StructuralEq for LinearizabilityTester<ThreadId, RefObj>

impl<ThreadId, RefObj: SequentialSpec> StructuralPartialEq for LinearizabilityTester<ThreadId, RefObj>