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

use super::super::super::support::dot;
use super::{Doc, arb_ops, run};
use crate::metis::{DotSet, DotStore};
use proptest::prelude::*;

proptest! {
    /// The pair merge is the semilattice join over run-reached states.
    #[test]
    fn prop_merge_is_a_semilattice_join(ops in arb_ops()) {
        let (live, _) = run(&ops);
        let (a, b, c) = (&live[0], &live[1], &live[2]);
        prop_assert_eq!(a.merge(b), b.merge(a));
        prop_assert_eq!(a.merge(b).merge(c), a.merge(&b.merge(c)));
        prop_assert_eq!(&a.merge(a), a);
        prop_assert_eq!(&a.merge(&Doc::new()), a);
    }

    /// A dot survives iff no side that saw it has dropped it.
    #[test]
    fn prop_survivor_law_is_exact(
        (a_ctx, a_keep) in arb_covered(), (b_ctx, b_keep) in arb_covered(),
    ) {
        let merged = a_keep.causal_merge(&a_ctx, &b_keep, &b_ctx);
        for station in 0u32..3 {
            for counter in 1u64..8 {
                let probe = dot(station, counter);
                let survives = (a_keep.contains(probe) && b_keep.contains(probe))
                    || (a_keep.contains(probe) && !b_ctx.contains(probe))
                    || (b_keep.contains(probe) && !a_ctx.contains(probe));
                prop_assert_eq!(merged.contains(probe), survives);
            }
        }
    }

    /// The in-place pair fold agrees with the pure merge on every run-reached
    /// state: `merge_from` is `merge` in cost clothing (S182). Exercises the
    /// `DotMap` default body, the `DotSet` override underneath it, and the
    /// in-place context union in one law.
    #[test]
    fn prop_merge_from_agrees_with_merge(ops in arb_ops()) {
        let (live, _) = run(&ops);
        for a in &live {
            for b in &live {
                let mut folded = a.clone();
                folded.merge_from(b);
                prop_assert_eq!(folded, a.merge(b));
            }
        }
    }

    /// The DotSet store override agrees with the pure survivor merge on
    /// arbitrary covered pairs, including mid-prefix removals (the floor
    /// retraction path).
    #[test]
    fn prop_dot_set_in_place_fold_agrees(
        (a_ctx, a_keep) in arb_covered(), (b_ctx, b_keep) in arb_covered(),
    ) {
        let pure = a_keep.causal_merge(&a_ctx, &b_keep, &b_ctx);
        let mut folded = a_keep;
        folded.causal_merge_from(&a_ctx, &b_keep, &b_ctx);
        prop_assert_eq!(folded, pure);
    }

    /// Context is the knowledge join; store sits below the plain union.
    #[test]
    fn prop_projections_split_knowledge_from_survival(ops in arb_ops()) {
        let (live, _) = run(&ops);
        let (a, b) = (&live[0], &live[1]);
        let merged = a.merge(b);
        prop_assert_eq!(merged.context(), &a.context().merge(b.context()));

        let store_union = a
            .store()
            .causal_merge(&DotSet::new(), b.store(), &DotSet::new());
        for (key, held) in merged.store() {
            let both = store_union.get(key).expect("survivors come from the union");
            for held_dot in held.difference(&DotSet::new()) {
                prop_assert!(both.contains(held_dot));
            }
        }
    }
}

fn arb_covered() -> impl Strategy<Value = (DotSet, DotSet)> {
    prop::collection::vec(((0u32..3, 1u64..8), prop::bool::ANY), 0..16).prop_map(|seen| {
        let mut context = DotSet::new();
        let mut store = DotSet::new();
        for ((station, counter), keep) in seen {
            let _ = context.insert(dot(station, counter));
            if keep {
                let _ = store.insert(dot(station, counter));
            }
        }
        (context, store)
    })
}