6d7cd481f9
Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VdfEGXA7aJ6ftMsCc9PJze
381 lines
11 KiB
Rust
381 lines
11 KiB
Rust
//! An edge over a network that drops, duplicates, garbles and reorders frames.
|
|
//! Evidence: `context/test-evidence/zset.md`.
|
|
|
|
mod support;
|
|
|
|
use proptest::prelude::*;
|
|
use std::collections::{HashMap, VecDeque};
|
|
use std::sync::{Arc, Mutex};
|
|
use support::Text;
|
|
use zset::{Circuit, EdgeSink, EdgeSource, Output, Pipe, Recv, Refused, Stamp, ZSet};
|
|
|
|
type Z = ZSet<u8>;
|
|
|
|
/// One direction of the network: frames in flight (which the test may reorder, drop, duplicate
|
|
/// or garble) and frames delivered (which `try_recv` takes in order).
|
|
#[derive(Default)]
|
|
struct Lane {
|
|
flight: Vec<String>,
|
|
ready: VecDeque<String>,
|
|
}
|
|
|
|
#[derive(Default)]
|
|
struct Net {
|
|
lanes: [Lane; 2],
|
|
cap: usize,
|
|
}
|
|
|
|
type Shared = Arc<Mutex<Net>>;
|
|
|
|
/// One end: sends into lane `out`, receives from the other one.
|
|
struct End {
|
|
net: Shared,
|
|
out: usize,
|
|
}
|
|
|
|
impl Pipe<String> for End {
|
|
fn try_send(&mut self, wire: String) -> Result<(), Refused<String>> {
|
|
let mut n = self.net.lock().unwrap();
|
|
let cap = n.cap;
|
|
let lane = &mut n.lanes[self.out];
|
|
if lane.flight.len() + lane.ready.len() >= cap {
|
|
return Err(Refused::Full(wire));
|
|
}
|
|
lane.flight.push(wire);
|
|
Ok(())
|
|
}
|
|
|
|
fn try_recv(&mut self) -> Result<String, Recv> {
|
|
let mut n = self.net.lock().unwrap();
|
|
n.lanes[1 - self.out].ready.pop_front().ok_or(Recv::Empty)
|
|
}
|
|
}
|
|
|
|
fn net(cap: usize) -> (Shared, End, End) {
|
|
let shared: Shared = Arc::new(Mutex::new(Net {
|
|
cap,
|
|
..Net::default()
|
|
}));
|
|
let sink_end = End {
|
|
net: shared.clone(),
|
|
out: 0,
|
|
};
|
|
let src_end = End {
|
|
net: shared.clone(),
|
|
out: 1,
|
|
};
|
|
(shared, sink_end, src_end)
|
|
}
|
|
|
|
struct World {
|
|
net: Shared,
|
|
sink: EdgeSink<u8, Text, End>,
|
|
src: EdgeSource<u8, Text, End>,
|
|
cons: Circuit,
|
|
out: Output<u8>,
|
|
got: Z,
|
|
total: Z,
|
|
epoch: u64,
|
|
seq: u64,
|
|
history: HashMap<(u64, u64), Z>,
|
|
joined_max: u64,
|
|
}
|
|
|
|
impl World {
|
|
fn new(cap: usize) -> Self {
|
|
let (shared, a, b) = net(cap);
|
|
let mut cons = Circuit::new();
|
|
let (i, s) = cons.input::<u8>();
|
|
let out = cons.output(&s);
|
|
let mut history = HashMap::new();
|
|
history.insert((1, 0), Z::new());
|
|
World {
|
|
net: shared,
|
|
sink: EdgeSink::new(Text, a, 1),
|
|
src: EdgeSource::new(Text, b, i),
|
|
cons,
|
|
out,
|
|
got: Z::new(),
|
|
total: Z::new(),
|
|
epoch: 1,
|
|
seq: 0,
|
|
history,
|
|
joined_max: 0,
|
|
}
|
|
}
|
|
|
|
fn commit(&mut self, d: Z) {
|
|
self.total += &d;
|
|
self.seq += 1;
|
|
self.sink.committed(d);
|
|
self.history
|
|
.insert((self.epoch, self.seq), self.total.clone());
|
|
}
|
|
|
|
fn restart_sink(&mut self, seq: u64) {
|
|
self.epoch += 1;
|
|
self.seq = seq;
|
|
let old = std::mem::replace(
|
|
&mut self.sink,
|
|
EdgeSink::new(
|
|
Text,
|
|
End {
|
|
net: self.net.clone(),
|
|
out: 0,
|
|
},
|
|
0,
|
|
),
|
|
);
|
|
self.sink = old.restart(self.epoch, seq, self.total.clone());
|
|
self.history.insert((self.epoch, seq), self.total.clone());
|
|
}
|
|
|
|
/// The consumer process lost its state: a brand-new receiver, with no token to carry over.
|
|
fn new_source(&mut self) {
|
|
let mut cons = Circuit::new();
|
|
let (i, s) = cons.input::<u8>();
|
|
self.out = cons.output(&s);
|
|
let end = End {
|
|
net: self.net.clone(),
|
|
out: 1,
|
|
};
|
|
self.src = EdgeSource::new(Text, end, i);
|
|
self.cons = cons;
|
|
self.got = Z::new();
|
|
self.joined_max = 0;
|
|
}
|
|
|
|
fn restart_source(&mut self) {
|
|
let mut cons = Circuit::new();
|
|
let (i, s) = cons.input::<u8>();
|
|
self.out = cons.output(&s);
|
|
let old = std::mem::replace(
|
|
&mut self.src,
|
|
EdgeSource::new(
|
|
Text,
|
|
End {
|
|
net: self.net.clone(),
|
|
out: 1,
|
|
},
|
|
i,
|
|
),
|
|
);
|
|
self.src = old.restart(i);
|
|
self.cons = cons;
|
|
self.got = Z::new();
|
|
self.joined_max = 0;
|
|
}
|
|
|
|
fn step(&mut self) {
|
|
self.cons.step();
|
|
self.got += self.cons.take(&self.out);
|
|
}
|
|
|
|
fn lane(&mut self, dir: usize, idx: usize, f: impl FnOnce(&mut Lane, usize)) {
|
|
let mut n = self.net.lock().unwrap();
|
|
let lane = &mut n.lanes[dir];
|
|
if !lane.flight.is_empty() {
|
|
let at = idx % lane.flight.len();
|
|
f(lane, at);
|
|
}
|
|
}
|
|
|
|
/// The two safety rules, after every action.
|
|
fn check(&mut self, when: &str) {
|
|
if let Some(Stamp { epoch, seq }) = self.src.stamp() {
|
|
assert!(
|
|
epoch >= self.joined_max,
|
|
"[older] {when}: the receiver went back from epoch {} to {epoch}",
|
|
self.joined_max
|
|
);
|
|
self.joined_max = epoch;
|
|
let want = self.history.get(&(epoch, seq));
|
|
assert_eq!(
|
|
Some(self.src.held()),
|
|
want,
|
|
"[claim] {when}: held is not the sender's integral at ({epoch}, {seq})"
|
|
);
|
|
}
|
|
}
|
|
|
|
fn settle(&mut self) {
|
|
for _ in 0..400 {
|
|
let silent = {
|
|
let mut n = self.net.lock().unwrap();
|
|
let silent = n
|
|
.lanes
|
|
.iter()
|
|
.all(|l| l.flight.is_empty() && l.ready.is_empty());
|
|
for lane in &mut n.lanes {
|
|
let flight = std::mem::take(&mut lane.flight);
|
|
lane.ready.extend(flight);
|
|
}
|
|
silent
|
|
};
|
|
self.sink.pump();
|
|
let read = self.src.poll(&mut self.cons, 8);
|
|
self.step();
|
|
self.check("settle");
|
|
let quiet = {
|
|
let n = self.net.lock().unwrap();
|
|
n.lanes
|
|
.iter()
|
|
.all(|l| l.flight.is_empty() && l.ready.is_empty())
|
|
};
|
|
if quiet
|
|
&& !self.sink.backlog()
|
|
&& !self.src.stale()
|
|
&& self.src.stamp() == Some(self.sink.stamp())
|
|
{
|
|
break;
|
|
}
|
|
if silent && read == 0 {
|
|
// Nothing was in flight: the reply is lost, not late. Only now does the timeout fire.
|
|
self.src.connection_lost();
|
|
}
|
|
}
|
|
assert_eq!(
|
|
self.src.stamp(),
|
|
Some(self.sink.stamp()),
|
|
"[settle] never caught up"
|
|
);
|
|
self.step();
|
|
assert_eq!(self.got, self.total, "[settle] the consumer's integral");
|
|
}
|
|
}
|
|
|
|
#[derive(Clone, Debug)]
|
|
enum Act {
|
|
Commit(Vec<(u8, i64)>),
|
|
Pump,
|
|
Poll(usize),
|
|
Step,
|
|
Timeout,
|
|
Deliver(usize, usize),
|
|
Drop(usize, usize),
|
|
Dup(usize, usize),
|
|
Garble(usize, usize),
|
|
RestartSink(u64),
|
|
RestartSource,
|
|
NewSource,
|
|
}
|
|
|
|
fn act() -> impl Strategy<Value = Act> {
|
|
let lane = 0usize..2;
|
|
let at = 0usize..8;
|
|
prop_oneof![
|
|
5 => prop::collection::vec((0u8..10, -2i64..=2), 0..3).prop_map(Act::Commit),
|
|
4 => Just(Act::Pump),
|
|
4 => (1usize..4).prop_map(Act::Poll),
|
|
2 => Just(Act::Step),
|
|
2 => Just(Act::Timeout),
|
|
8 => (lane.clone(), at.clone()).prop_map(|(l, i)| Act::Deliver(l, i)),
|
|
2 => (lane.clone(), at.clone()).prop_map(|(l, i)| Act::Drop(l, i)),
|
|
2 => (lane.clone(), at.clone()).prop_map(|(l, i)| Act::Dup(l, i)),
|
|
1 => (lane, at).prop_map(|(l, i)| Act::Garble(l, i)),
|
|
1 => (0u64..8).prop_map(Act::RestartSink),
|
|
1 => Just(Act::RestartSource),
|
|
1 => Just(Act::NewSource),
|
|
]
|
|
}
|
|
|
|
fn run(cap: usize, acts: &[Act]) {
|
|
let mut w = World::new(cap);
|
|
for (n, a) in acts.iter().enumerate() {
|
|
match a {
|
|
Act::Commit(d) => w.commit(d.iter().copied().collect()),
|
|
Act::Pump => {
|
|
w.sink.pump();
|
|
}
|
|
Act::Poll(m) => {
|
|
w.src.poll(&mut w.cons, *m);
|
|
}
|
|
Act::Step => w.step(),
|
|
Act::Timeout => w.src.connection_lost(),
|
|
Act::Deliver(d, i) => w.lane(*d, *i, |l, at| {
|
|
let f = l.flight.remove(at);
|
|
l.ready.push_back(f);
|
|
}),
|
|
Act::Drop(d, i) => w.lane(*d, *i, |l, at| {
|
|
l.flight.remove(at);
|
|
}),
|
|
Act::Dup(d, i) => w.lane(*d, *i, |l, at| {
|
|
let f = l.flight[at].clone();
|
|
l.flight.push(f);
|
|
}),
|
|
Act::Garble(d, i) => w.lane(*d, *i, |l, at| l.flight[at] = "garbage".to_string()),
|
|
Act::RestartSink(seq) => w.restart_sink(*seq),
|
|
Act::RestartSource => w.restart_source(),
|
|
Act::NewSource => w.new_source(),
|
|
}
|
|
w.check(&format!("after action {n} ({a:?})"));
|
|
}
|
|
w.settle();
|
|
}
|
|
|
|
proptest! {
|
|
/// Any history over a lossy, duplicating, garbling, reordering network keeps both safety
|
|
/// rules at every step, and settles to the sender's integral once the network is reliable.
|
|
#[test]
|
|
fn the_receiver_is_never_wrong_over_a_hostile_network(
|
|
acts in prop::collection::vec(act(), 0..60), cap in 1usize..5,
|
|
) {
|
|
run(cap, &acts);
|
|
}
|
|
}
|
|
|
|
#[test]
|
|
fn the_reviewers_late_reply_case_is_a_history() {
|
|
// Epoch 1 reads a request, its reply is delayed, the sender restarts, and the late reply comes.
|
|
// One frame per poll, so each is judged on its own.
|
|
let acts = [
|
|
Act::Poll(1),
|
|
Act::Pump,
|
|
Act::Commit(vec![(1, 1)]),
|
|
Act::Deliver(1, 0),
|
|
Act::Pump,
|
|
Act::RestartSink(3),
|
|
Act::Timeout,
|
|
Act::Poll(1),
|
|
Act::Deliver(1, 0),
|
|
Act::Pump,
|
|
Act::Deliver(0, 1),
|
|
Act::Poll(1),
|
|
Act::Deliver(0, 0),
|
|
Act::Poll(1),
|
|
Act::Poll(1),
|
|
];
|
|
run(2, &acts);
|
|
}
|
|
|
|
#[test]
|
|
fn review_token_collision_after_new_source() {
|
|
// The old receiver's request 2 is answered by E1 and the reply is delayed. E1 dies, E2 takes
|
|
// over, a new receiver joins E2 and times out, and the dead reply arrives for its request 2.
|
|
let acts = [
|
|
Act::Poll(1),
|
|
Act::Deliver(1, 0),
|
|
Act::Pump,
|
|
Act::Deliver(0, 0),
|
|
Act::Poll(4),
|
|
Act::Commit(vec![(1, 1)]),
|
|
Act::Timeout,
|
|
Act::Poll(1),
|
|
Act::Deliver(1, 0),
|
|
Act::Pump,
|
|
Act::RestartSink(5),
|
|
Act::Commit(vec![(2, 1)]),
|
|
Act::NewSource,
|
|
Act::Poll(1),
|
|
Act::Deliver(1, 0),
|
|
Act::Pump,
|
|
Act::Deliver(0, 1),
|
|
Act::Poll(4),
|
|
Act::Timeout,
|
|
Act::Poll(1),
|
|
Act::Deliver(0, 0),
|
|
Act::Poll(4),
|
|
];
|
|
run(4, &acts);
|
|
}
|