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

extern crate alloc;

use alloc::collections::BTreeMap;
use alloc::vec::Vec;

use crate::kairos::Kairos;
use crate::metis::{Anchor, Dot, Locus};
use proptest::prelude::*;

use super::super::{arb_ops, run};

proptest! {
    /// C7: `children_of(anchor)` agrees with the `order()` sibling order on BOTH
    /// sides (S127). For the origin and, for every woven dot, its After and Before
    /// buckets, the maintained bucket equals the dots the naive reference groups
    /// under that anchor, in the same STORED order (rank descending, dot ascending
    /// on ties), visible and tombstone alike.
    #[test]
    fn prop_children_of_agrees_with_the_sibling_order(ops in arb_ops()) {
        let (live, record) = run(&ops);
        for seq in &live {
            // The naive sibling buckets, built independently from this replica's
            // loci (rank descending, dot ascending), including tombstones.
            let held: BTreeMap<Dot, Locus> = record
                .woven
                .iter()
                .filter(|(dot, _)| seq.store().locus(**dot).is_some())
                .map(|(&dot, &locus)| (dot, locus))
                .collect();
            let naive_bucket = |anchor: Anchor| -> Vec<Dot> {
                let mut kids: Vec<Dot> = held
                    .iter()
                    .filter(|(_, t)| t.anchor == anchor)
                    .map(|(&d, _)| d)
                    .collect();
                kids.sort_by(|a, b| {
                    let (ra, rb): (Kairos, Kairos) = (held[a].rank, held[b].rank);
                    rb.cmp(&ra).then_with(|| a.cmp(b))
                });
                kids
            };
            // The origin bucket.
            let got_origin: Vec<Dot> = seq.store().children_of(Anchor::Origin).collect();
            prop_assert_eq!(got_origin, naive_bucket(Anchor::Origin));
            // Every woven dot's After and Before buckets.
            for &dot in held.keys() {
                let after = Anchor::After(dot.into());
                let before = Anchor::Before(dot.into());
                let got_after: Vec<Dot> = seq.store().children_of(after).collect();
                prop_assert_eq!(got_after, naive_bucket(after));
                let got_before: Vec<Dot> = seq.store().children_of(before).collect();
                prop_assert_eq!(got_before, naive_bucket(before));
            }
        }
    }
}