2 releases
0.1.1 | Sep 28, 2023 |
---|---|
0.1.0 | Sep 22, 2023 |
#827 in Concurrency
340KB
776 lines
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 valuex
is modeled byResponse(Read(Some(x)))
. We are use anOption
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 byCall(Write(y))
and the response is modeled byResponse(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
.