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

use super::super::super::support::arb_vv;
use super::arb_roster;
use crate::metis::with_scope;
use proptest::prelude::*;

proptest! {
    /// Scoped vector folds commute with unbranded restriction.
    #[test]
    fn prop_scoped_vector_folds_commute_with_restriction(
        a in arb_vv(), b in arb_vv(), r in arb_roster(),
    ) {
        let expected_merge = a.merge(&b).restrict(r.iter().copied());
        let expected_meet = a.meet(&b).restrict(r.iter().copied());
        let (merged, met) = with_scope(r.iter().copied(), |scope| {
            let ra = scope.restrict(&a);
            let rb = scope.restrict(&b);
            (ra.merge(&rb).forget(), ra.meet(&rb).forget())
        });
        prop_assert_eq!(merged, expected_merge);
        prop_assert_eq!(met, expected_meet);
    }

    /// Scoped order verdicts match unbranded restriction verdicts and preserve
    /// global order.
    #[test]
    fn prop_scoped_order_preserves_global_order(
        a in arb_vv(), b in arb_vv(), r in arb_roster(),
    ) {
        let ra = a.restrict(r.iter().copied());
        let rb = b.restrict(r.iter().copied());
        with_scope(r.iter().copied(), |scope| {
            let sa = scope.restrict(&a);
            let sb = scope.restrict(&b);
            if a <= b {
                prop_assert!(!sb.happens_before(&sa) || sa == sb);
                prop_assert!(sa.partial_cmp_scoped(&sb) != Some(core::cmp::Ordering::Greater));
            }
            prop_assert_eq!(sa.partial_cmp_scoped(&sb), ra.partial_cmp(&rb));
            prop_assert_eq!(sa.happens_before(&sb), ra.happens_before(&rb));
            Ok(())
        })?;
    }

    /// Scoped concurrency exactly matches the restricted vectors and reflects
    /// back to the original vectors when true.
    #[test]
    fn prop_concurrent_globally_reflects(
        a in arb_vv(), b in arb_vv(), r in arb_roster(),
    ) {
        let ra = a.restrict(r.iter().copied());
        let rb = b.restrict(r.iter().copied());
        with_scope(r.iter().copied(), |scope| {
            let sa = scope.restrict(&a);
            let sb = scope.restrict(&b);
            let verdict = sa.concurrent_globally(&sb);
            prop_assert_eq!(verdict, ra.concurrent(&rb));
            if verdict {
                prop_assert!(a.concurrent(&b));
            }
            Ok(())
        })?;
    }

    /// `map` keeps the brand and applies the closure.
    #[test]
    fn prop_map_keeps_the_brand_and_applies_the_closure(
        a in arb_vv(), b in arb_vv(), r in arb_roster(),
    ) {
        let (mapped_a, merged) = with_scope(r.iter().copied(), |scope| {
            let ra = scope.restrict(&a);
            let rb = scope.restrict(&b);
            let ma = ra.clone().map(|v| v.merge(&b.restrict(r.iter().copied())));
            let value = ra.map(|v| v.merge(&rb.forget()));
            (ma.forget(), value.forget())
        });
        let expected = a
            .restrict(r.iter().copied())
            .merge(&b.restrict(r.iter().copied()));
        prop_assert_eq!(&mapped_a, &expected);
        prop_assert_eq!(merged, expected);
    }
}