Trait stateright::semantics::ConsistencyTester

pub trait ConsistencyTester<T, RefObj>where
    RefObj: SequentialSpec,
    T: Copy,{
    // Required methods
    fn on_invoke(
        &mut self,
        thread_id: T,
        op: RefObj::Op
    ) -> Result<&mut Self, String>;
    fn on_return(
        &mut self,
        thread_id: T,
        ret: RefObj::Ret
    ) -> Result<&mut Self, String>;
    fn is_consistent(&self) -> bool;

    // Provided method
    fn on_invret(
        &mut self,
        thread_id: T,
        op: RefObj::Op,
        ret: RefObj::Ret
    ) -> Result<&mut Self, String> { ... }
}

An implementation of this trait tests the consistency of a concurrent system with respect to a “reference sequential specification” SequentialSpec. The interface for doing so involves recording operation invocations and returns.

Currently Stateright includes implementations in the form of a LinearizabilityTester and SequentialConsistencyTester.

Required Methods

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

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

fn is_consistent(&self) -> bool

Indicates whether the recorded history is consistent with the semantics expected by the tester.

Provided Methods

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.

Implementors

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,

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