todc-utils

Utilities for building and testing distributed algorithms.

Examples

Consider the following sequential specification for a register containing u32 values.

```rs use todc_utils::specifications::Specification;

[derive(Copy, Clone, Debug)]

enum RegisterOp { Read(Option), 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.

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

type RegisterChecker = WGLChecker;

// A history of sequantial operations is always linearizable. // PO |------| Write(0) // P1 |------| Read(Some(0)) let history = History::fromactions(vec![ (0, Call(Write(0))), (0, Response(Write(0))), (1, Call(Read(None))), (1, Response(Read(Some(0)))), ]); assert!(RegisterChecker::islinearizable(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::fromactions(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::islinearizable(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::fromactions(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::islinearizable(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.