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

extern crate alloc;

use alloc::collections::{BTreeMap, BTreeSet};
use alloc::vec::Vec;

use super::super::{Record, Seq, arb_ops_with_paste, reference_order, run};
use crate::metis::Dot;
use proptest::prelude::*;

/// The naive order of a per-replica record slice: the reference algorithm run
/// against exactly the dots one replica holds. Used by the per-replica reads so
/// the oracle matches what a single replica (not the fold) can see.
fn naive_order_of(seq: &Seq, record: &Record) -> Vec<Dot> {
    // Restrict the oracle to the loci this replica actually carries (a
    // replica may hold a strict subset after partial gossip), and expel the
    // dots it does not currently show.
    let mut woven = BTreeMap::new();
    let mut expelled = BTreeSet::new();
    for (&dot, &locus) in &record.woven {
        if seq.store().locus(dot).is_some() {
            let _ = woven.insert(dot, locus);
            if !seq.store().is_visible(dot) {
                let _ = expelled.insert(dot);
            }
        }
    }
    reference_order(&Record { woven, expelled })
}

proptest! {
    /// C8 law: the maintained (cached) `order()` agrees with the naive
    /// independent reference on EVERY reachable state, not just the fold. After
    /// any history, each individual replica's `order()` equals the reference
    /// order built from the oracle restricted to that replica's loci. The
    /// cache never diverges from the algorithm it accelerates.
    #[test]
    fn prop_cached_order_agrees_with_naive_on_every_replica(ops in arb_ops_with_paste()) {
        let (live, record) = run(&ops);
        for seq in &live {
            let got = seq.store().order();
            let expected = naive_order_of(seq, &record);
            prop_assert_eq!(got, expected);
        }
    }
}