minerva 0.2.0

Causal ordering for distributed systems
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
66
67
68
69
70
71
72
73
74
75
76

extern crate alloc;

use alloc::vec::Vec;

use crate::metis::{Dotted, Rhapsody};

use super::wire::round_trip_rhapsody;
use super::{Fleet, REPLICAS};

/// After the tape, gossip the fleet to convergence and assert the convergence
/// laws: fold-order independence, one visible order, a surviving wire law,
/// and the strong-list verdict over every order the whole run observed
/// (S288): one witness total order must embed them all.
pub(super) fn assert_convergence(fleet: &mut Fleet) {
    let states: Vec<Dotted<Rhapsody>> = fleet.live.iter().map(|r| r.state().clone()).collect();
    // Every pairwise merge from the pre-convergence snapshot is observed
    // first: the in-place loop below walks only one merge path (the first
    // replica absorbs the second, then the third meets their join), and a
    // transient contradiction in a skipped pair could hide behind the
    // healed full join (the S288 review's second finding; the ledger
    // exhibit pinning the detection power is
    // `strong_list::examples::test_a_skipped_pairwise_merge_can_hide_a_contradiction`).
    for i in 0..REPLICAS {
        for j in 0..REPLICAS {
            if i != j {
                let pairwise = states[i].merge(&states[j]);
                let order = pairwise.store().order();
                let _ = fleet.ledger.observe(&order);
            }
        }
    }
    let mut states = states;
    for _ in 0..REPLICAS {
        for i in 0..REPLICAS {
            for j in 0..REPLICAS {
                if i != j {
                    states[i] = states[i].merge(&states[j]);
                    // Every intermediate post-merge order is an observed
                    // state: a transient contradiction that later merges
                    // would heal must not escape the oracle (the S288
                    // review's first finding).
                    let order = states[i].store().order();
                    let _ = fleet.ledger.observe(&order);
                }
            }
        }
    }

    let forward = states
        .iter()
        .fold(Dotted::<Rhapsody>::new(), |acc, s| acc.merge(s));
    let backward = states
        .iter()
        .rev()
        .fold(Dotted::<Rhapsody>::new(), |acc, s| acc.merge(s));
    assert_eq!(forward, backward, "the fold must not depend on order");

    let target = forward.store().order();
    for state in &states {
        assert_eq!(
            state.store().order(),
            target,
            "every converged replica reads the one order",
        );
    }

    round_trip_rhapsody(forward.store());

    let _ = fleet.ledger.observe(&target);
    if let Err(contradiction) = fleet.ledger.verdict() {
        panic!(
            "the run's observed orders admit no single total order \
             (the strong list specification's order clause): {contradiction:?}",
        );
    }
}