spectroscope 0.1.0

Consistency and isolation level checkers for distributed systems testing
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65

//! Basic usage of the set-full linearizability checker.
//!
//! Run with: cargo run --example basic

use spectroscope::history::{History, Op, Pid};
use spectroscope::set_full::{SetFullChecker, Validity};

/// A value being added to or read from the set.
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
struct Val(u32);

fn main() {
    // A history records operations from concurrent processes.
    // Each operation has an invocation (start) and completion (ok/fail).
    let mut history = History::new();

    // Process 0 adds element 1
    history.push(Op::add_invoke(0, Pid(0), Val(1)).at_millis(0));
    history.push(Op::add_ok(1, Pid(0), Val(1)).at_millis(5));

    // Process 1 adds element 2
    history.push(Op::add_invoke(2, Pid(1), Val(2)).at_millis(2));
    history.push(Op::add_ok(3, Pid(1), Val(2)).at_millis(7));

    // Process 2 reads and sees both elements
    history.push(Op::read_invoke(4, Pid(2)).at_millis(10));
    history.push(Op::read_ok(5, Pid(2), [Val(1), Val(2)]).at_millis(12));

    // Check the history
    let result = SetFullChecker::default().check(&history);

    println!("Validity: {:?}", result.valid);
    println!("Elements added: {}", result.attempt_count);
    println!("Stable (visible): {}", result.stable_count);
    println!("Lost: {}", result.lost_count);

    assert_eq!(result.valid, Validity::Valid);

    // Now let's create an invalid history where an element disappears
    println!("\n--- Invalid history (element lost) ---\n");

    let mut bad_history = History::new();

    // Add element 1
    bad_history.push(Op::add_invoke(0, Pid(0), Val(1)).at_millis(0));
    bad_history.push(Op::add_ok(1, Pid(0), Val(1)).at_millis(5));

    // First read sees it
    bad_history.push(Op::read_invoke(2, Pid(1)).at_millis(10));
    bad_history.push(Op::read_ok(3, Pid(1), [Val(1)]).at_millis(12));

    // Second read doesn't see it - element was lost!
    bad_history.push(Op::read_invoke(4, Pid(1)).at_millis(20));
    bad_history.push(Op::read_ok(5, Pid(1), []).at_millis(22));

    let bad_result = SetFullChecker::default().check(&bad_history);

    println!("Validity: {:?}", bad_result.valid);
    println!("Lost elements: {:?}", bad_result.lost);

    assert_eq!(bad_result.valid, Validity::Invalid);
    assert_eq!(bad_result.lost, vec![Val(1)]);

    println!("\nDone!");
}