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

extern crate alloc;

use super::super::support::{arb_history, deliverable, drain, perm_of};
use crate::metis::{CausalIdeal, VersionVector};
use alloc::vec::Vec;
use proptest::prelude::*;

proptest! {
    /// Every released event is deliverable against the events already released.
    #[test]
    fn prop_release_respects_causality(
        (history, perm) in arb_history()
            .prop_flat_map(|history| {
                let perm = perm_of(history.len());
                (Just(history), perm)
            }),
    ) {
        let mut buf = CausalIdeal::new();
        for &index in &perm {
            buf.insert(history[index].clone());
        }
        let released = drain(&mut buf);

        let mut delivered = VersionVector::new();
        for &payload in &released {
            let event = &history[payload as usize];
            prop_assert!(deliverable(event, &delivered));
            delivered = delivered.merge(&event.deps);
        }
    }

    /// A valid history carries the full closure, so every distinct event releases once.
    #[test]
    fn prop_every_event_released_once(
        (history, perm) in arb_history()
            .prop_flat_map(|history| {
                let perm = perm_of(history.len());
                (Just(history), perm)
            }),
    ) {
        let mut buf = CausalIdeal::new();
        for &index in &perm {
            buf.insert(history[index].clone());
        }
        let mut released = drain(&mut buf);

        prop_assert_eq!(buf.pending_len(), 0);
        prop_assert_eq!(released.len(), history.len());
        released.sort_unstable();
        let n = u32::try_from(history.len()).unwrap();
        prop_assert_eq!(released, (0..n).collect::<Vec<u32>>());
    }

    /// Inserting every event twice still releases each exactly once.
    #[test]
    fn prop_duplicates_dropped(
        (history, perm) in arb_history()
            .prop_flat_map(|history| {
                let perm = perm_of(history.len() * 2);
                (Just(history), perm)
            }),
    ) {
        let n = history.len();
        let mut buf = CausalIdeal::new();
        for &index in &perm {
            buf.insert(history[index % n].clone());
        }
        let mut released = drain(&mut buf);

        prop_assert_eq!(released.len(), n);
        released.sort_unstable();
        released.dedup();
        prop_assert_eq!(released.len(), n);
    }

    /// Release order is a function of the events, not their arrival order.
    #[test]
    fn prop_release_order_is_permutation_invariant(
        (history, perm_a, perm_b) in arb_history()
            .prop_flat_map(|history| {
                let len = history.len();
                (Just(history), perm_of(len), perm_of(len))
            }),
    ) {
        let release = |perm: &[usize]| {
            let mut buf = CausalIdeal::new();
            for &index in perm {
                buf.insert(history[index].clone());
            }
            drain(&mut buf)
        };
        prop_assert_eq!(release(&perm_a), release(&perm_b));
    }
}