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

extern crate alloc;

use super::super::support::perm_of;
use super::support::producer;
use crate::metis::Event;
use alloc::vec::Vec;
use proptest::prelude::*;

proptest! {
    /// Successive produces advance the sender's own dot by exactly one.
    #[test]
    fn prop_produce_is_self_contiguous(n in 1u64..30) {
        let mut p = producer(1);
        for expected in 1..=n {
            let event = p.produce(0u16, ());
            prop_assert_eq!(event.deps.get(1), expected);
            prop_assert_eq!(p.knowledge().get(1), expected);
        }
    }

    /// Produced deps equal post-increment knowledge and dominate every observed event.
    #[test]
    fn prop_produce_deps_are_closed(perm in (1usize..8).prop_flat_map(perm_of)) {
        let k = perm.len();
        let mut a = producer(1);
        let events: Vec<Event<()>> = (0..k).map(|_| a.produce(0u16, ())).collect();
        let mut b = producer(2);
        for &i in &perm {
            b.observe(&events[i]);
        }
        let event = b.produce(0u16, ());
        prop_assert_eq!(&event.deps, b.knowledge());
        for observed in &events {
            prop_assert!(observed.deps <= event.deps);
        }
        prop_assert_eq!(event.deps.get(1), u64::try_from(k).unwrap());
        prop_assert_eq!(event.deps.get(2), 1);
    }

    /// A produced stamp strictly exceeds every observed event's stamp.
    #[test]
    fn prop_produce_stamp_dominates(perm in (1usize..8).prop_flat_map(perm_of)) {
        let k = perm.len();
        let mut a = producer(1);
        let events: Vec<Event<()>> = (0..k).map(|_| a.produce(0u16, ())).collect();
        let mut b = producer(2);
        for &i in &perm {
            b.observe(&events[i]);
        }
        let event = b.produce(0u16, ());
        for observed in &events {
            prop_assert!(event.stamp > observed.stamp);
        }
    }

    /// Observing the same events in any permutation yields the same knowledge.
    #[test]
    fn prop_observe_is_order_invariant(
        (perm_a, perm_b) in (2usize..10).prop_flat_map(|n| (perm_of(n), perm_of(n))),
    ) {
        let n = perm_a.len();
        let mut s1 = producer(1);
        let mut s3 = producer(3);
        let events: Vec<Event<()>> = (0..n)
            .map(|i| if i % 2 == 0 { s1.produce(0u16, ()) } else { s3.produce(0u16, ()) })
            .collect();
        let mut b1 = producer(2);
        let mut b2 = producer(2);
        for &i in &perm_a {
            b1.observe(&events[i]);
        }
        for &i in &perm_b {
            b2.observe(&events[i]);
        }
        prop_assert_eq!(b1.knowledge(), b2.knowledge());
        let e1 = b1.produce(0u16, ());
        let e2 = b2.produce(0u16, ());
        for observed in &events {
            prop_assert!(e1.stamp > observed.stamp);
            prop_assert!(e2.stamp > observed.stamp);
        }
    }

    /// Self-echoes leave knowledge unchanged and never break monotonicity.
    #[test]
    fn prop_self_echo_is_safe(k in 1usize..10) {
        let mut p = producer(1);
        let own: Vec<Event<()>> = (0..k).map(|_| p.produce(0u16, ())).collect();
        let knowledge_before = p.knowledge().clone();
        for event in &own {
            p.observe(event);
        }
        prop_assert_eq!(p.knowledge(), &knowledge_before);
        let next = p.produce(0u16, ());
        for event in &own {
            prop_assert!(next.stamp > event.stamp);
        }
    }
}