Struct WGLChecker

pub struct WGLChecker<S: Specification> { /* private fields */ }

A linearizability checker.

An implementation of the algorithm originally defined by Jeannette Wing and Chun Gong [WG93], and extended by Gavin Lowe [L17]. This particular implementation is based on the description given by Alex Horn and Daniel Kroenig [HK15].

Given a history of operations, the algorithm works by linearizing each operation as soon as possible. When an operation cannot be linearized, it backtracks and proceeds with the next operation. Memoization occurs by caching each partial linearization, and preventing the algorithm from continuing its search when it is already known that the state of the object and remaining operations have no valid linearization.

Examples

Consider the following Specification of a register containing u32 values.

use todc_utils::specifications::Specification;

#[derive(Copy, Clone, Debug)]
enum RegisterOp {
    Read(Option<u32>),
    Write(u32),
}

use RegisterOp::{Read, Write};

struct RegisterSpec;

impl Specification for RegisterSpec {
    type State = u32;
    type Operation = RegisterOp;
     
    fn init() -> Self::State {
        0
    }

    fn apply(operation: &Self::Operation, state: &Self::State) -> (bool, Self::State) {
        match operation {
            // A read is valid if the value returned is equal to the
            // current state. Reads always leave the state unchanged.
            Read(value) => match value {
                Some(value) => (value == state, *state),
                None => (false, *state)
            },
            // Writes are always valid, and update the state to be
            // equal to the value being written.
            Write(value) => (true, *value),
        }
    }
}

Using the Action::Call and Action::Response types, we can model read and write operations as follows:

• The call of a read operation is modeled by Call(Read(None)) and a response containing the value x is modeled by Response(Read(Some(x))). We are required to use an Option because the value being read cannot be known until the register responds.
• Similarily, the call of a write operation with the value y is modeled by Call(Write(y)) and the response is modeled by Response(Write(y)).

Next, we can define a linearizability for this specification, and check some histories.

use todc_utils::linearizability::{WGLChecker, history::{History, Action::{Call, Response}}};

type RegisterChecker = WGLChecker<RegisterSpec>;

// A history of sequantial operations is always linearizable.
// PO |------|          Write(0)
// P1          |------| Read(Some(0))
let history = History::from_actions(vec![
    (0, Call(Write(0))),
    (0, Response(Write(0))),
    (1, Call(Read(None))),
    (1, Response(Read(Some(0)))),
]);
assert!(RegisterChecker::is_linearizable(history));

// Concurrent operations might not be linearized
// in the order in which they are called.
// PO |--------------|  Write(0)
// P1  |--------------| Write(1)
// P2    |---|          Read(Some(1))
// P3           |---|   Read(Some(0))
let history = History::from_actions(vec![
    (0, Call(Write(0))),
    (1, Call(Write(1))),
    (2, Call(Read(None))),
    (2, Response(Read(Some(1)))),
    (3, Call(Read(None))),
    (3, Response(Read(Some(0)))),
    (0, Response(Write(0))),
    (1, Response(Write(1))),
]);
assert!(RegisterChecker::is_linearizable(history));

// A sequentially consistent history is **not**
// necessarily linearizable.
// PO |---|             Write(0)
// P1 |---|             Write(1)
// P2       |---|       Read(Some(1))
// P3             |---| Read(Some(0))
let history = History::from_actions(vec![
    (0, Call(Write(0))),
    (1, Call(Write(1))),
    (0, Response(Write(0))),
    (1, Response(Write(1))),
    (2, Call(Read(None))),
    (2, Response(Read(Some(1)))),
    (3, Call(Read(None))),
    (3, Response(Read(Some(0)))),
]);
assert!(!RegisterChecker::is_linearizable(history));

For examples of using WGLChecker to check the linearizability of more complex histories, see todc-mem/tests/snapshot/common.rs or todc-utils/tests/linearizability/etcd.rs.

Implementations in Other Languages

For an implementation in C++, see linearizability-checker. For an implementation in Go, see porcupine.

Implementations

impl<S: Specification> WGLChecker<S>

pub fn is_linearizable(history: History<S::Operation>) -> bool

Returns whether the history of operations is linearizable with respect to the specification.