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
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124

extern crate alloc;

use alloc::vec::Vec;

use super::super::support::dot;
use crate::metis::{Composer, DotMap, DotSet, Dotted, Purview};
use proptest::prelude::*;

mod common;
mod owed;
mod rows;

/// The document shape the run exercises: caller keys over bare presence dots.
type Doc = Dotted<DotMap<u8, DotSet>>;

/// The number of replicas / roster peers in a simulated run.
const REPLICAS: usize = 3;

/// One step of a simulated multi-replica run. Replica `i` writes as station
/// `i + 1` (station `0` is not valid), so dot assignment exercises the real
/// `next_dot` path.
#[derive(Clone, Debug)]
enum Op {
    /// Replica assigns a fresh dot under `key` and merges the write delta.
    Add { replica: usize, key: u8 },
    /// Replica supersedes exactly the dots it currently observes under `key`.
    Remove { replica: usize, key: u8 },
    /// Replica `to` merges a delta `from` owes it, and `to`'s tracker notes
    /// the context of the delta actually received (genuine evidence).
    Gossip { from: usize, to: usize },
}

fn arb_ops() -> impl Strategy<Value = Vec<Op>> {
    let op = prop_oneof![
        (0..REPLICAS, 0u8..3).prop_map(|(replica, key)| Op::Add { replica, key }),
        (0..REPLICAS, 0u8..3).prop_map(|(replica, key)| Op::Remove { replica, key }),
        (0..REPLICAS, 0..REPLICAS).prop_map(|(from, to)| Op::Gossip { from, to }),
    ];
    prop::collection::vec(op, 0..24)
}

/// The station id replica `i` writes as.
fn station_of(replica: usize) -> u32 {
    u32::try_from(replica + 1).unwrap()
}

/// The roster of station ids the run and the note streams range over,
/// ascending: `station_of(0..REPLICAS)`.
fn roster() -> Vec<u32> {
    (0..REPLICAS).map(station_of).collect()
}

/// The transcript a run leaves behind: the final replica states and, per
/// replica, the tracker built from the contexts of deltas that replica
/// actually received (the genuine-evidence discipline). Every replica tracks
/// the whole roster of peers.
struct Transcript {
    live: Vec<Doc>,
    trackers: Vec<Purview>,
}

/// Replays a history over fresh replicas. Gossip ships a targeted delta (via
/// the sender's `delta_for` against the receiver's context) and the receiver's
/// tracker notes the *sender*'s context, exactly the whole-state evidence an
/// anti-entropy exchange yields.
fn run(ops: &[Op]) -> Transcript {
    let roster = roster();
    let mut live: Vec<Doc> = (0..REPLICAS).map(|_| Dotted::new()).collect();
    let mut trackers: Vec<Purview> = (0..REPLICAS)
        .map(|_| Purview::new(roster.iter().copied()))
        .collect();
    for op in ops {
        match *op {
            Op::Add { replica, key } => {
                let fresh = live[replica].next_dot(station_of(replica));
                let mut held = DotSet::new();
                assert!(held.insert(fresh));
                let delta = Dotted::from_store(DotMap::singleton(key, held));
                live[replica] = live[replica].merge(&delta);
            }
            Op::Remove { replica, key } => {
                let observed = live[replica].store().get(&key).cloned().unwrap_or_default();
                let delta = Dotted::from_context(observed);
                live[replica] = live[replica].merge(&delta);
            }
            Op::Gossip { from, to } => {
                // The receiver learns the sender's state THROUGH the receive
                // path: a composer adopts its state and absorbs the sender's full
                // state as a delta, minting a `Received` that testifies to the
                // sender and the context it demonstrably held. The tracker notes
                // that receipt, so every row rises only by genuine receive
                // evidence (never a raw DotSet).
                let mut sink = Composer::adopt(station_of(to), live[to].clone());
                let received = sink.absorb(station_of(from), &live[from]);
                live[to] = sink.state().clone();
                trackers[to].note(&received).unwrap();
            }
        }
    }
    Transcript { live, trackers }
}

/// The naive model of `common`: the intersection of every row, computed off the
/// tracker's own rows read through `of`.
fn model_common(purview: &Purview, roster: &[u32]) -> DotSet {
    let mut rows = roster.iter().map(|&peer| purview.of(peer).unwrap());
    let Some(first) = rows.next() else {
        return DotSet::new();
    };
    rows.fold(first.clone(), |acc, row| acc.intersect(row))
}

/// A stream of `(peer, evidence)` notes over the roster `1..=REPLICAS`, small
/// enough that rows overlap and `common` moves.
fn arb_notes() -> impl Strategy<Value = Vec<(u32, DotSet)>> {
    let evidence = prop::collection::vec((1u32..=4, 1u64..6), 0..6).prop_map(|pairs| {
        let mut set = DotSet::new();
        for (station, counter) in pairs {
            let _ = set.insert(dot(station, counter));
        }
        set
    });
    prop::collection::vec((station_of(0)..=station_of(REPLICAS - 1), evidence), 0..16)
}