Struct stateright::semantics::LinearizabilityTester

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

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: SequentialSpec,
    RefObj::Op: Debug,
    RefObj::Ret: Debug + PartialEq, 

pub 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.

pub 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.

pub 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 lineariable.

See LinearizabilityTester::serialized_history.

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

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,
    RefObj::Op: Clone, 

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

Returns a copy of the value.

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

Performs copy-assignment from source.

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

pub 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, 

pub fn default() -> Self

Returns the "default value" for a type.

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

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

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

Feeds this value into the given Hasher.

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

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,
    RefObj::Op: PartialEq, 

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

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

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

This method tests for !=.

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

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

Serialize this value into the given Serde serializer.

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

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