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

//! Convergence and the atomic-reassignment law over generated op tapes.

use proptest::prelude::*;

use crate::metis::Kind;

use super::super::TestNode;
use super::{arb_ops, observed_under, page_with, run, settle};

proptest! {
    /// Any tape of composer writes, exclusive re-kinds, retracts, and gossip
    /// steps converges under full anti-entropy: one pair, one context, one
    /// survivor law, however the kinds fought.
    #[test]
    fn prop_fleet_converges_under_full_exchange(ops in arb_ops()) {
        let mut fleet = run(&ops);
        settle(&mut fleet);
        prop_assert_eq!(fleet[0].state(), fleet[1].state());
        prop_assert_eq!(fleet[1].state(), fleet[2].state());
    }

    /// The exclusive re-kind is atomic at any synced peer: after absorbing
    /// exactly the one covered delta, the block's evidence is the fresh kind
    /// and nothing else, whatever state the tape had built under the key
    /// (the stage A three-delta window, closed structurally).
    #[test]
    fn prop_rekind_is_atomic_at_any_synced_peer(ops in arb_ops(), key in 0u8..3) {
        let mut fleet = run(&ops);
        settle(&mut fleet);

        let writer = &mut fleet[0];
        let (_, delta) = writer.compose_super(
            |dot| {
                let mut block = TestNode::new();
                assert!(block.write_tag(dot, Kind::Register));
                page_with(key, block)
            },
            |held| observed_under(held, key),
        );

        let peer = &mut fleet[1];
        let _ = peer.absorb(1, &delta);
        let block = peer.state().store().children().get(&key)
            .expect("the fresh tag write keeps the key alive");
        let kinds = block.kinds_present();
        prop_assert_eq!(kinds.len(), 1, "no stale evidence survives the one delta");
        prop_assert!(kinds.contains(Kind::Register));
        prop_assert!(block.register().is_empty(), "empty of its kind");
        prop_assert_eq!(block.tag().len(), 1, "exactly the fresh tag write");
    }
}