lincheck 0.1.1

A linearizability checker for concurrent data structures
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29

/// The sequential implementation of a data structure.
pub trait SequentialSpec {
    /// The type of operations.
    type Op;

    /// The type of return values.
    type Ret;

    /// Creates a new instance of the data structure.
    fn new() -> Self;

    /// Executes an operation on the data structure.
    fn exec(&mut self, op: Self::Op) -> Self::Ret;
}

/// The concurrent implementation of a data structure.
pub trait ConcurrentSpec {
    /// The type of operations.
    type Op;

    /// The type of return values.
    type Ret;

    /// Creates a new instance of the data structure.
    fn new() -> Self;

    /// Executes an operation on the data structure.
    fn exec(&self, op: Self::Op) -> Self::Ret;
}