todc-utils

构建和测试分布式算法的实用工具。

示例

考虑以下包含 u32 值的寄存器的顺序规范。

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),
        }
    }
}

使用 Action::Call 和 Action::Response 类型，我们可以将读取和写入操作建模如下

• 读取操作的调用由 Call(Read(None)) 模型，包含值 x 的响应由 Response(Read(Some(x))) 模型。我们使用 Option 是因为读取的值只能在寄存器响应后才知道。
• 同样，值 y 的写入操作的调用由 Call(Write(y)) 模型，响应由 Response(Write(y)) 模型。

接下来，我们可以定义此规范的线性化，并检查一些历史记录。

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));

有关使用 WGLChecker 检查更复杂历史记录的线性化的示例，请参阅 todc-mem/tests/snapshot/common.rs 或 todc-utils/tests/linearizability/etcd.rs。