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
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104

extern crate alloc;

use alloc::vec::Vec;

use crate::metis::{Dot, DotSet, Dotted, Retired};
use proptest::prelude::*;

use super::super::{REPLICAS, Seq, arb_ops, condense_pair, run};

proptest! {
    /// `condense` under an honest claim preserves order and convergence.
    #[test]
    fn prop_condense_under_an_honest_claim_preserves_order(ops in arb_ops()) {
        let (live, record) = run(&ops);

        let fold = live.iter().fold(Seq::new(), |acc, r| acc.merge(r));
        let mut converged: Vec<Seq> = live.iter().map(|r| r.merge(&fold)).collect();
        let orders_before: Vec<Vec<Dot>> =
            converged.iter().map(|r| r.store().order()).collect();

        let mut retired = DotSet::new();
        for &dot in &record.expelled {
            let _ = retired.insert(dot);
        }

        let retired = Retired::trust(retired);
        for r in &mut converged {
            let mut rhapsody = r.store().clone();
            let _ = rhapsody.condense(&retired);
            *r = Dotted::try_new(rhapsody, r.context().clone()).unwrap();
        }

        for (r, before) in converged.iter().zip(&orders_before) {
            prop_assert_eq!(&r.store().order(), before);
            // The maintained recording have-set tracks the excision: for
            // every dot the run wove, the witness claims it iff the skeleton
            // still holds its locus (a condensed replica must stop claiming
            // what it can no longer serve).
            for &dot in record.woven.keys() {
                prop_assert_eq!(
                    r.store().woven().contains(dot),
                    r.store().locus(dot).is_some(),
                );
            }
        }

        let forward = converged.iter().fold(Seq::new(), |acc, r| acc.merge(r));
        let backward = converged.iter().rev().fold(Seq::new(), |acc, r| acc.merge(r));
        let forward_order = forward.store().order();
        prop_assert_eq!(&forward_order, &backward.store().order());
        prop_assert_eq!(&forward_order, &orders_before[0]);
        for r in &converged {
            prop_assert_eq!(&forward.merge(r).store().order(), &forward_order);
        }
    }

    /// `condense(a.merge(b))` and `condense(a).merge(condense(b))` read the same
    /// order under a shared honest claim.
    #[test]
    fn prop_condense_commutes_with_merge(ops in arb_ops()) {
        let (live, record) = run(&ops);

        let fold = live.iter().fold(Seq::new(), |acc, r| acc.merge(r));
        let converged: Vec<Seq> = live.iter().map(|r| r.merge(&fold)).collect();
        let a = &converged[0];
        let b = &converged[REPLICAS - 1];

        let mut retired = DotSet::new();
        for &dot in &record.expelled {
            let _ = retired.insert(dot);
        }
        let retired = Retired::trust(retired);

        let left = condense_pair(&a.merge(b), &retired);
        let right = condense_pair(a, &retired).merge(&condense_pair(b, &retired));

        prop_assert_eq!(left.store().order(), right.store().order());
    }

    /// A superset claim condenses idempotently over a subset claim.
    #[test]
    fn prop_monotone_claim_condense_is_idempotent(ops in arb_ops()) {
        let (live, record) = run(&ops);
        let fold = live.iter().fold(Seq::new(), |acc, r| acc.merge(r));
        let converged = live[0].merge(&fold);

        let expelled: Vec<Dot> = record.expelled.iter().copied().collect();
        let mut r1 = DotSet::new();
        let mut r2 = DotSet::new();
        for (i, &dot) in expelled.iter().enumerate() {
            let _ = r2.insert(dot);
            if i % 2 == 0 {
                let _ = r1.insert(dot);
            }
        }
        let (r1, r2) = (Retired::trust(r1), Retired::trust(r2));

        let staged = condense_pair(&condense_pair(&converged, &r1), &r2);
        let one_shot = condense_pair(&converged, &r2);

        prop_assert_eq!(staged.store().skeleton_len(), one_shot.store().skeleton_len());
        prop_assert_eq!(staged.store().order(), one_shot.store().order());
    }
}