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

extern crate alloc;

use alloc::collections::BTreeSet;
use alloc::string::String;

use super::super::super::support::dot;
use crate::metis::{Dot, DotFun, DotSet, DotStore};
use proptest::prelude::*;

use super::{arb_seed, covered, value_for};

proptest! {
    /// The survivor law, exact per dot with values checked.
    #[test]
    fn prop_survivor_law_is_exact_with_values(a in arb_seed(), b in arb_seed()) {
        let ca = covered(&a);
        let cb = covered(&b);
        let merged = ca.store().causal_merge(ca.context(), cb.store(), cb.context());
        let a_dots: BTreeSet<Dot> = ca.store().dots().collect();
        let b_dots: BTreeSet<Dot> = cb.store().dots().collect();
        let merged_dots: BTreeSet<Dot> = merged.dots().collect();
        for station in 0u32..4 {
            for counter in 1u64..9 {
                let probe = dot(station, counter);
                let in_a = a_dots.contains(&probe);
                let in_b = b_dots.contains(&probe);
                let survives = (in_a && (in_b || !cb.context().contains(probe)))
                    || (in_b && (in_a || !ca.context().contains(probe)));
                prop_assert_eq!(merged_dots.contains(&probe), survives);
                if survives {
                    let got = merged.get(probe).expect("a survivor carries content");
                    prop_assert_eq!(got, &value_for(station, counter));
                }
            }
        }
    }

    /// Commutative under basis-honest values: equal dots carry equal values, so
    /// keep-self and keep-other agree on every shared dot.
    #[test]
    fn prop_causal_merge_is_commutative(a in arb_seed(), b in arb_seed()) {
        let ca = covered(&a);
        let cb = covered(&b);
        let ab = ca.store().causal_merge(ca.context(), cb.store(), cb.context());
        let ba = cb.store().causal_merge(cb.context(), ca.store(), ca.context());
        prop_assert_eq!(ab, ba);
    }

    /// Associative: the two groupings of a three-way fold agree.
    #[test]
    fn prop_causal_merge_is_associative(a in arb_seed(), b in arb_seed(), c in arb_seed()) {
        let ca = covered(&a);
        let cb = covered(&b);
        let cc = covered(&c);

        let bc = cb.store().causal_merge(cb.context(), cc.store(), cc.context());
        let bc_ctx = cb.context().merge(cc.context());
        let left = ca.store().causal_merge(ca.context(), &bc, &bc_ctx);

        let ab = ca.store().causal_merge(ca.context(), cb.store(), cb.context());
        let ab_ctx = ca.context().merge(cb.context());
        let right = ab.causal_merge(&ab_ctx, cc.store(), cc.context());

        prop_assert_eq!(left, right);
    }

    /// Idempotent: a covered store merged with itself under its own context is
    /// itself.
    #[test]
    fn prop_causal_merge_is_idempotent(a in arb_seed()) {
        let ca = covered(&a);
        let merged = ca.store().causal_merge(ca.context(), ca.store(), ca.context());
        prop_assert_eq!(&merged, ca.store());
    }

    /// Bottom identity: the bottom store under the empty context leaves a
    /// covered store unchanged from either side.
    #[test]
    fn prop_bottom_is_the_identity(a in arb_seed()) {
        let ca = covered(&a);
        let bottom = DotFun::<String>::new();
        let empty = DotSet::new();
        let right = ca.store().causal_merge(ca.context(), &bottom, &empty);
        prop_assert_eq!(&right, ca.store());
        let left = bottom.causal_merge(&empty, ca.store(), ca.context());
        prop_assert_eq!(&left, ca.store());
    }
}