todc-utils

Utilities for building and testing distributed algorithms.

Examples

Consider the following sequential specification for 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 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.