Harness ฉีด partition แบบดีเทอร์มินิสติก (Jepsen-lite) + linearizability checker
บท 6 คุณสร้างกลไก ลู่เข้า ครบชุดแล้ว — Merkle anti-entropy หา key ที่ต่างแบบ sub-linear, gossip กระจายข่าวใน O(log N), membership merge เป็น monotone semilattice ทุกชิ้นผ่าน property test เป็นพันๆ เคส แต่มีคำถามที่ยังค้าง: เรารู้ได้อย่างไรว่ามันถูกต้องตอนเครือข่าย “ขาดจริง” — ตอนที่ replica ครึ่งหนึ่งคุยกับอีกครึ่งไม่ได้ ต่างฝั่งต่างรับเขียน แล้วพอเชื่อมกลับ มันยังลู่เข้าหาค่าเดียวกันโดยไม่ทำ write ที่ ack ไปแล้วหล่นหาย?
บทนี้คือ ออราเคิล ของทั้งคอร์ส เราสร้าง harness ฉีด partitionpartitionเครือข่ายขาด: ข้ามกลุ่มส่งข้อความไม่ถึงกัน — ต้นเหตุของ split-brain ที่ harness ฉีดเข้าไป แบบดีเทอร์มินิสติก — รุ่นย่อของ JepsenJepsenระเบียบวิธีทดสอบระบบกระจายด้วยการฉีด fault แล้วตรวจ history; harness ในคอร์สนี้คือรุ่นย่อ — ที่ จำลอง เครือข่ายขาดใน process เดียว, ขับด้วย seed คงที่, ตัดจบด้วย hard timeout แล้ว assert สมบัติแบบกระจายที่ borrow checker มองไม่เห็น พร้อม linearizability checker ที่ทำหน้าที่เป็นออราเคิลอีกตัว บอกได้ว่า history ที่บันทึกมานั้น เรียงเป็นลำดับเชิงเส้นที่ถูกต้องได้ไหม และจบด้วยความจริงที่ขมที่สุดของบทนี้: ผ่าน 500 seed ไม่ใช่บทพิสูจน์
คอร์สนี้ ต่อยอด repo kaen-kvstore จาก #22 (code ตัวอย่างกำลังจัดทำ) — บทนี้สร้าง เครื่องมือทดสอบ ที่บท 8 (capstone) จะใช้ขับ cluster kaen-kvstore หลาย replica จริง harness, driver property test และ linearizability checker ในบทนี้คือ ออราเคิล ที่พิสูจน์สองสมบัติของ capstone (“ไม่มี acked write หายใต้ W+R>N” และ “replica ลู่เข้าหลัง heal”) — สมบัติที่ demo happy-path ยืนยันไม่ได้ ต้องใช้ harness ฉีด fault เท่านั้น ทั้งหมด Rust std ล้วน: splitmix64 เขียนเอง + std::sync::mpsc + BTreeMap — ไม่มี proptest, ไม่มี tokio, ไม่มี serde
ทุก snippet pin ที่ Rust stable 1.97.1 (ออก 2026-07-16) และ edition = “2024” — [dependencies] ใน Cargo.toml ว่างเปล่า ZERO external crate บทนี้แตะ std เพียง std::collections::BTreeMap, std::sync::mpsc, std::thread กับ std::time เท่านั้น ทุกโปรแกรม compile แบบ zero-warnings และ รันจริง บน musl + rust-lld เลขทุกตัวด้านล่างคือ output จริงที่ seed ล็อกไว้ รันซ้ำได้ byte-identical (ยืนยันแล้วด้วย md5sum ที่ตรงกันสองรอบ) และทุก harness รันจบใต้ timeout 60 ไม่มีค้าง
ทำไมต้องมี harness — compiler พิสูจน์ให้ไม่ได้
หัวข้อที่มีชื่อว่า “ทำไมต้องมี harness — compiler พิสูจน์ให้ไม่ได้”ย้อนกลับไปที่เส้น scope ของคอร์ส: borrow checker ของ Rust การันตี ในเครื่องเดียว ว่าไม่มี data race, ไม่มี use-after-free — แต่มัน มองไม่เห็น การสลับลำดับข้อความ, partition, หรือ clock skew เพราะสิ่งเหล่านั้นเกิด ระหว่าง process ไม่ใช่ ใน process code replication ที่ subtle-wrong compile ผ่าน zero-warnings และเดโม happy-path สวยได้สบายๆ
สมบัติแบบกระจายจึงต้องมี ออราเคิลตัวอื่น มายืนยัน และออราเคิลนั้นคือ harness ที่ ฉีด fault เข้าไปเองอย่างจงใจ แล้วตรวจผลลัพธ์ — นี่คือแก่นของระเบียบวิธี Jepsen ของ Kyle Kingsbury: อย่ารอให้ partition เกิดเองในโปรดักชัน จง สร้าง มันขึ้นมาในที่ควบคุมได้ แล้วดูว่าระบบยังรักษาสมบัติที่สัญญาไว้หรือไม่
แต่ Jepsen จริงรันบนหลายเครื่องด้วย wall-clock — เราย่อมันลงเป็น single-scheduler ใน process เดียว เพื่อให้ได้สิ่งที่มีค่าที่สุดในการทดสอบระบบกระจาย: ดีเทอร์มินิสซึม ถ้า harness สุ่มด้วยเวลาจริงหรือด้วยลำดับ thread ที่ OS จัด รันแดงครั้งหนึ่งแล้วรันซ้ำไม่ได้ — bug report ที่ reproduce ไม่ได้ก็ไร้ค่า วินัยของบทนี้คือ ทุก แหล่งสุ่มมาจาก splitmix64splitmix64PRNG ตัวเล็กเขียนเอง seed ได้ ผลซ้ำได้ 100% — แทน proptest/quickcheck ในแซนด์บ็อกซ์ std ล้วน ที่ seed คงที่ และ ทุก loop ที่อาจค้างถูกตัดด้วย budget
driver: for_all ที่คืน seed สำหรับ reproduce
หัวข้อที่มีชื่อว่า “driver: for_all ที่คืน seed สำหรับ reproduce”เริ่มที่เครื่องมือพื้นฐาน — PRNG ที่ seed ได้กับ property driver ตัวเล็ก for_all จะรัน property บน case-seed หลายพันตัวที่ ดึงจาก master stream และเมื่อเจอ counterexample ตัวแรก มันคืน seed ที่ทำให้พัง กลับมา นั่นคือ “poor-man’s shrink” — handle เดียวที่ reproduce เคสนั้นซ้ำได้ทันที:
struct Rng { state: u64,}impl Rng { fn new(seed: u64) -> Self { Self { state: seed } } fn next_u64(&mut self) -> u64 { self.state = self.state.wrapping_add(0x9E3779B97F4A7C15); let mut z = self.state; z = (z ^ (z >> 30)).wrapping_mul(0xBF58476D1CE4E5B9); z = (z ^ (z >> 27)).wrapping_mul(0x94D049BB133111EB); z ^ (z >> 31) } fn below(&mut self, n: u64) -> u64 { self.next_u64() % n } fn unit(&mut self) -> f64 { (self.next_u64() >> 11) as f64 / (1u64 << 53) as f64 }}
// Ok(passed) หรือ Err(reproducing_seed) เมื่อเจอ counterexample ตัวแรกfn for_all<F: Fn(u64) -> bool>(master: u64, cases: u64, prop: F) -> Result<u64, u64> { let mut seeder = Rng::new(master); for _ in 0..cases { let seed = seeder.next_u64(); if !prop(seed) { return Err(seed); } } Ok(cases)}mixing ทุกจุดใช้ wrapping_add/wrapping_mul เสมอ — ค่าคงที่ของ Vigna ล้นแน่นอน ถ้าใช้ +/* ธรรมดามันจะ panic ทันทีใน debug build เพื่อให้เห็นว่า driver พูดจริง เราเดโมสามอย่าง: ดีเทอร์มินิสซึม (new(42) ให้ stream เดียวกันเป๊ะ, new(43) เบนออก), property จริงที่ผ่าน แล้ว property ที่ จงใจให้เท็จ (พังเมื่อ below(1000) ตกที่ 500) เพื่อโชว์ว่า Err คืน seed ที่ reproduce ได้จริง:
fn main() { let (mut a, mut b) = (Rng::new(42), Rng::new(42)); let det = (0..8).all(|_| a.next_u64() == b.next_u64()); let diff = Rng::new(43).next_u64() != Rng::new(42).next_u64(); println!("determinism: new(42)==new(42) -> {det}; new(43)!=new(42) -> {diff}"); assert!(det && diff, "PRNG must be seed-deterministic");
let mut mr = Rng::new(0xDEAD_BEEFu64); let mean = (0..5000).map(|_| mr.unit()).sum::<f64>() / 5000.0; println!("mean of 5000 unit() draws (master=0xDEADBEEF) = {mean:.4}");
let master = 0xDEAD_BEEFu64; let cases = 5000u64;
// property จริง: below(n) < n ทุกครั้ง match for_all(master, cases, |seed| { let mut rr = Rng::new(seed); let n = 1 + rr.below(1000); rr.below(n) < n }) { Ok(k) => println!("range property below(n)<n : {k}/{cases} PASS"), Err(s) => println!("range property FAILED, reproduce with Rng::new({s})"), }
// property ที่จงใจให้เท็จ: พังเมื่อ below(1000)==500 match for_all(master, u64::MAX, |seed| { let mut rr = Rng::new(seed); rr.below(1000) != 500 }) { Ok(_) => println!("false property unexpectedly held"), Err(s) => { let mut chk = Rng::new(s); let got = chk.below(1000); println!("false property (below(1000)==500): reproduce with Rng::new({s})"); println!(" cross-check: Rng::new({s}).below(1000) = {got}"); assert_eq!(got, 500); } }}รันจริงได้ตามนี้:
determinism: new(42)==new(42) -> true; new(43)!=new(42) -> truemean of 5000 unit() draws (master=0xDEADBEEF) = 0.5048range property below(n)<n : 5000/5000 PASSfalse property (below(1000)==500): reproduce with Rng::new(12774923733135906520) cross-check: Rng::new(12774923733135906520).below(1000) = 500บรรทัดสำคัญคือบรรทัดสุดท้าย: property เท็จพังที่ case-seed 12774923733135906520 และ cross-check ยืนยันว่า Rng::new(12774923733135906520).below(1000) ให้ 500 เป๊ะ — เอา seed ตัวนี้ไปใส่ Rng::new(...) เมื่อไรก็ reproduce เคสที่พังได้ทันที นี่คือเหตุผลว่าทำไมเราต้อง พิมพ์ seed ออกมา เสมอ
harness ฉีด partition: เขียนสองฝั่ง, heal, ลู่เข้า
หัวข้อที่มีชื่อว่า “harness ฉีด partition: เขียนสองฝั่ง, heal, ลู่เข้า”หัวใจของบทคือ harness ที่ขับ 5 replica แบบ LWW-RegisterLWW-Registerรีจิสเตอร์ค่าเดียวที่ timestamp สูงสุดชนะ — ทิ้ง write ที่ concurrent (lossy โดย design) ด้วย W=R=3 (ดังนั้น W+R=6>5) เราแบ่ง cluster เป็นสองครึ่ง {0,1} กับ {2,3,4} แล้วเดินสี่เฟส: (1) เขียนตอนเชื่อมกันปกติ, (2) ฉีด partition แล้วเขียนบน ทั้งสองฝั่ง, (3) heal, (4) รัน anti-entropy จนถึง fixpoint — โดยมี round budget เป็น hard timeout
store แต่ละ replica เป็น BTreeMap<u64, Lww> ไม่ใช่ HashMap — RandomState ของ HashMap สุ่ม seed ต่อ process ลำดับ iteration จะต่างทุกครั้ง ทำลายดีเทอร์มินิสซึมทันที การ merge ของ LWW คือ “ค่าที่ (ts, node) ใหญ่สุดชนะ” ซึ่งเป็น total order deterministic:
#[derive(Clone, Copy, Debug, PartialEq, Eq)]struct Lww { ts: u64, node: u64, val: u64,}impl Lww { fn merge(self, other: Lww, buggy: bool) -> Lww { if buggy { // ❌ version ดิบ: บวก val => ไม่ idempotent => merge(a,a) != a // => anti-entropy ไม่มีวันถึง fixpoint compile ผ่าน แต่ค้าง Lww { ts: self.ts.max(other.ts), node: self.node.max(other.node), val: self.val.wrapping_add(other.val), } } else if (other.ts, other.node) > (self.ts, self.node) { other } else { self } }}buggy คือกับดักที่ตั้งไว้พิสูจน์ว่า timeout ทำงานจริง: merge ที่บวก val เป็น commutative และ associative แต่ ไม่ idempotent — merge(a, a) ให้ 2·val ไม่ใช่ a ผลคือ full-mesh anti-entropy ไม่มีวันหยุดนิ่ง val โตขึ้นทุกรอบ compiler จับ deadlock/ไม่ลู่เข้าแบบนี้ ไม่ได้เลย — จับได้ทางเดียวคือ round budget
anti-entropy วน full-mesh: ทุก replica merge จาก snapshot ของทุก replica อื่น จนกว่ารอบหนึ่งจะไม่มีอะไรเปลี่ยน (fixpoint) หรือหมด budget คืน Result<usize, usize> — Ok(rounds) เมื่อลู่เข้า, Err(budget) เมื่อ timeout:
type Store = BTreeMap<u64, Lww>;
fn anti_entropy(replicas: &mut [Store], buggy: bool, max_rounds: usize) -> Result<usize, usize> { for round in 1..=max_rounds { let snapshot = replicas.to_vec(); let mut changed = false; for i in 0..replicas.len() { for j in 0..replicas.len() { if i == j { continue; } for (&k, &v) in &snapshot[j] { match replicas[i].get(&k).copied() { None => { replicas[i].insert(k, v); changed = true; } Some(cur) => { let merged = cur.merge(v, buggy); if merged != cur { replicas[i].insert(k, merged); changed = true; } } } } } } if !changed { return Ok(round); } } Err(max_rounds) // hard timeout: ไม่ลู่เข้าในงบรอบที่ตั้งไว้}ระหว่าง partition, coordinator เขียนได้เฉพาะ replica ใน ครึ่งเดียวกัน — write จากฝั่ง A ถึงแค่ {0,1} = 2 node < W=3 จึง ไม่ ack (อาจหายก็ได้ ไม่การันตี), ส่วน write จากฝั่ง B ถึง {2,3,4} = 3 node = W จึง ack และ ต้อง รอดหลัง heal นี่คือแก่นของสมบัติ durability เราบังคับให้เกิด conflict บน key 0 ทุก seed (ฝั่ง A เขียนค่าหนึ่ง, ฝั่ง B เขียนอีกค่าด้วย ts สูงกว่า) เพื่อให้ split-brain เกิด จริง ทุกครั้ง แล้ว assert สองสมบัติ:
- convergence — หลัง heal ทุก replica เท่ากันเป๊ะ (byte-identical ผ่าน
BTreeMapordering) - durability — ไม่มี acked write หาย:
tsที่ลู่เข้า>=tsสูงสุดที่ ack ต่อ key เพราะ write ที่ ack แล้วถึง>=Wreplica และ LWW ทับได้เฉพาะด้วยtsที่สูงกว่า
--- partition-inject harness (base seed=0xC0FFEE, 500 trials) ---split-brain BEFORE heal : 500/500 (non-vacuous: every seed partitioned)converged AFTER heal : 500/500durable (no acked lost) : 500/500anti-entropy rounds to fixpoint: min=2 max=2negative control (buggy non-idempotent merge): TIMEOUT fired after 50 rounds500/500 seeds passing is BOUNDED CHECKING, not a proof (FLP 1985).อ่านทีละบรรทัด: 500/500 split-brain ก่อน heal คือ non-vacuity — ทุก seed แตกเป็นสองฝั่งที่เห็นค่าต่างกันจริง ไม่ใช่ผ่านเพราะไม่มีอะไรเกิด; 500/500 converged และ 500/500 durable คือสองสมบัติที่ผ่านทุก seed; rounds min=2 max=2 — semilattice ที่ถูกต้องบน full-mesh ลู่เข้าใน 2 รอบเสมอ; และบรรทัด TIMEOUT fired after 50 rounds คือ negative control — merge ดิบที่ไม่ idempotent ชน budget พอดี พิสูจน์ว่า hard timeout ไม่ใช่ของประดับ ถ้าเราไม่ตั้ง budget โปรแกรมนี้จะวนไม่จบและ compiler ไม่เตือนอะไรเลย
sequenceDiagram
participant A as ฝั่ง A {0,1}
participant B as ฝั่ง B {2,3,4}
Note over A,B: เฟส 1 — เชื่อมกัน: write ack ครบ (ถึงทั้ง 5 replica)
Note over A,B: 🧱 ฉีด partition (ตัดข้อความข้ามครึ่ง)
Note over A: เขียน key0 (ถึง 2 node < W ⇒ ไม่ ack)
Note over B: เขียน key0 ts สูงกว่า (ถึง 3 node = W ⇒ ack)
Note over A,B: split-brain: A ≠ B (500/500 seed)
Note over A,B: 🔗 heal + anti-entropy (budget 50 รอบ)
Note over A,B: ลู่เข้าใน 2 รอบ ⇒ ทุก replica เท่ากัน, acked write ของ B รอด
คำบรรยายภาพ: single-scheduler + seed คงที่ + round budget — harness ที่ “ไม่” ค้างและ “พูดจริง”: เขียนสองฝั่งตอน partition, ฝั่ง B ที่ถึง quorum ได้ ack แล้วต้องรอดหลัง heal, ทุก replica ลู่เข้าค่าเดียวใน 2 รอบ
ทุก assertion ในบทนี้มาคู่กับการทำให้มัน พังจริง ได้: (1) merge ที่ไม่ idempotent → TIMEOUT after 50 rounds (ถ้า budget หายไป harness จะค้าง compiler เงียบ); (2) merge ที่เก็บ ts ต่ำกว่า → durability assert fail (ACKED WRITE LOST); (3) เปลี่ยน BTreeMap เป็น HashMap → รันซ้ำได้ผลต่างเพราะ RandomState; (4) split-brain 500/500 คือ non-vacuity ที่กันไม่ให้ convergence “ผ่าน” เพราะไม่มีอะไรให้ลู่เข้าตั้งแต่แรก ถ้าคุณเขียน harness แล้วมัน ไม่เคย แดงเลยไม่ว่าจะใส่ bug อะไร แปลว่ามันไม่ได้ตรวจอะไร
linearizability checker: ออราเคิลที่บอกว่า history “เรียงเป็นเส้นได้ไหม”
หัวข้อที่มีชื่อว่า “linearizability checker: ออราเคิลที่บอกว่า history “เรียงเป็นเส้นได้ไหม””harness ตรวจ convergence ได้ แต่ยังมีสมบัติที่แรงกว่าและ store แบบ eventual-consistency ของเรา ไม่ การันตี นั่นคือ linearizabilitylinearizabilityมีลำดับรวมหนึ่งที่เคารพเวลาจริงและถูกต้องตาม object; quorum+LWW 'ไม่' การันตีข้อนี้: มี ลำดับรวมหนึ่งเดียว ที่ (ก) เคารพเวลาจริง — ถ้า op หนึ่งจบก่อนอีก op เริ่ม มันต้องมาก่อนในลำดับ — และ (ข) ถูกต้องตาม object (read คืนค่าที่เขียนล่าสุดในลำดับนั้น) หรือไม่
Herlihy กับ Wing (1990) นิยามมันไว้ และวิธีตรวจแบบ backtracking ของ Wing-Gong ก็ตรงไปตรงมา: ลอง “ทำให้เป็นเส้น” op ที่ ไปต่อได้ (ไม่มี op ไหนที่ต้องมาก่อนมัน — เงื่อนไขคือ op.call <= min(ret ของ op ที่ยังไม่ใช้)), เอาไป apply กับ register model แบบลำดับ, recurse, ถ้าตันก็ถอยกลับ:
#[derive(Clone, Copy)]struct Op { is_write: bool, arg: u64, // ค่าที่เขียน หรือค่าที่ read คืนมา call: u64, // เวลาจริงตอนเรียก ret: u64, // เวลาจริงตอนตอบ (ret > call)}
fn search(ops: &[Op], used: &mut [bool], remaining: usize, state: u64) -> bool { if remaining == 0 { return true; } let min_ret = ops .iter() .enumerate() .filter(|(i, _)| !used[*i]) .map(|(_, o)| o.ret) .min() .unwrap(); for i in 0..ops.len() { if used[i] { continue; } let o = ops[i]; if o.call > min_ret { continue; // มี op ที่จบก่อน o เริ่ม ⇒ o เป็นตัวถัดไปไม่ได้ } let new_state = if o.is_write { o.arg } else { if o.arg != state { continue; // read ผิดกฎภายใต้ลำดับนี้ ⇒ ลอง op อื่น } state }; used[i] = true; if search(ops, used, remaining - 1, new_state) { used[i] = false; return true; } used[i] = false; } false}ทดสอบ3 history บน register ที่เริ่มที่ 0: H1 เขียน 1 เสร็จแล้วอ่านทีหลังได้ 1 (เรียงเป็นเส้นได้); H2 เขียน 1 เสร็จที่เวลา 10 แต่ read ที่ เริ่มหลังจากนั้น (เวลา 20) กลับคืน 0 — นี่คือ anomaly ของ quorum+LWW แบบ eventual-consistency เป๊ะๆ เรียงเป็นเส้นไม่ได้; H3 มีสองเขียน ที่ซ้อนเวลากัน (concurrent) แล้ว read ตรงกันที่ 2 (มีลำดับ w1,w2,r2,r2 ที่ถูกกฎ):
H1 (write then read sees it) -> trueH2 (stale read = EC quorum anomaly) -> falseH3 (concurrent writes, reads agree) -> truechecker agrees: true / false / true.Running it on the EC quorum+LWW history (H2) returns FALSE by design.H2 -> false คือประเด็นทั้งหมด: store ของเรา — quorum + LWW + read-repair — ให้ freshness ในเชิงมีขอบเขต staleness (บท 3) แต่ ไม่การันตี linearizability read ที่ concurrent กันเห็นค่าเดินถอยหลังได้ checker นี้จึงเป็นออราเคิลที่ ทำเครื่องหมายเส้น scope ให้ชัด: จุดที่ linearizable-txn / consensus เริ่มต้น คือจุดที่ subset ที่เราลง code รันจริงจบลง
timeout อีกตัว: wall-clock ที่ขอบเครือข่ายจริง
หัวข้อที่มีชื่อว่า “timeout อีกตัว: wall-clock ที่ขอบเครือข่ายจริง”round budget คือ timeout ในตรรกะที่ทดสอบ แต่บท 8 จะมี std::net จริง และ socket ที่ปลายทางถูก partition จะ block ตลอดกาล timeout ตัวที่สองจึงเป็น wall-clock — recv_timeout — ที่แปลง block ชั่วนิรันดร์ให้เป็น error ที่กู้คืนได้ ทันที ไม่ใช่หลังจากผ่านไปหนึ่งชั่วโมง:
use std::sync::mpsc;use std::time::{Duration, Instant};
let (_tx, rx) = mpsc::channel::<u64>();let start = Instant::now();match rx.recv_timeout(Duration::from_millis(100)) { Ok(v) => println!("got {v}"), Err(_) => println!("partitioned peer: recv_timeout fired after {:?}", start.elapsed()),}_tx ต้องอยู่รอด (ไม่ถูก drop) มิฉะนั้น channel จะ disconnect แล้ว recv_timeout คืน error ทันที ด้วยเหตุผลผิด (Disconnected ไม่ใช่ Timeout) — เราต้องการให้มัน รอครบ 100ms แล้วค่อย timeout เพื่อจำลอง peer ที่เงียบ:
partitioned peer: recv_timeout fired after 101.589374ms (no forever-block)reachable peer answered: 7wall-clock deadlines live at the real-net boundary ONLY, never inside logic-under-test.(ตัวเลข 101.5ms เป็น wall-clock จึงไม่ deterministic — เป็นข้อยกเว้นที่ตั้งใจ: เวลาจริงอยู่ที่ ขอบ เครือข่ายเท่านั้น) กฎเหล็กคือ wall-clock deadline อยู่ที่ boundary ของ real-net เท่านั้น ห้ามหลุดเข้าไปในตรรกะที่ทดสอบ เพราะมันจะพาความ non-deterministic กลับมาทำลาย reproducibility ทั้งหมด — ในตรรกะใช้ round budget ที่นับเป็นจำนวนรอบ ไม่ใช่นับเป็นวินาที
A — Rust พิสูจน์ “ในเครื่องเดียว” ไม่ใช่ “แบบกระจาย” และ harness คือการตรวจแบบมีขอบเขต: ผ่าน 500/500 seed ไม่ใช่บทพิสูจน์ (FLP 1985) — มันสำรวจเฉพาะ interleaving ที่ splitmix64 เดินไปถึง impl ที่ subtle-wrong ผ่าน 500 seed แล้วพังบน schedule ที่ 501 ได้สบายๆ harness เป็น ออราเคิลที่ดีที่สุดที่ compiler เป็นให้ไม่ได้ แต่มันคือ bounded checking ไม่ใช่ proof
B — เส้น scope: นี่แหละ คือเหตุผลที่ consensus/Raft correctness เป็น ไดอะแกรมเท่านั้น ในบท 8 — quorum arithmetic เอ็นนิวเมอเรตครบทุก subset ได้ (บท 3 ทำไปแล้ว: 22M คู่) แต่ state space ของ partition × reorder × clock-skew ของ Raft ระเบิดจน ตรวจครบไม่ได้ Fischer-Lynch-Paterson (1985) พิสูจน์ว่าไม่มี consensus แบบ asynchronous ที่การันตีทั้ง terminate และถูกต้องต่อ adversarial scheduler ที่มี node เจ๊งแม้แต่ตัวเดียว — green test บน Raft จึงเป็นคำกล่าวอ้าง correctness ที่ เท็จ
C — ดีเทอร์มินิสซึมคือวินัย: seed คงที่พิมพ์ออกมาเป็น repro handle (12774923733135906520), single-scheduler, BTreeMap ไม่ใช่ HashMap (RandomState สุ่มลำดับต่อ process), และ ทุก loop ที่อาจค้างมี hard budget มิฉะนั้น harness จะ โกหก (รันแดงซ้ำไม่ได้) หรือ ค้าง (compiler จับ deadlock ไม่ได้ — negative control พิสูจน์ให้เห็นว่า budget ทำงานจริง)
สรุปก่อนไปต่อ
หัวข้อที่มีชื่อว่า “สรุปก่อนไปต่อ”บทนี้สร้าง ออราเคิล ของทั้งคอร์ส: for_all driver ที่ seed ด้วย splitmix64splitmix64PRNG ตัวเล็กเขียนเอง seed ได้ ผลซ้ำได้ 100% — แทน proptest/quickcheck ในแซนด์บ็อกซ์ std ล้วน และคืน seed สำหรับ reproduce เมื่อ property พัง (12774923733135906520); harness ฉีด partitionpartitionเครือข่ายขาด: ข้ามกลุ่มส่งข้อความไม่ถึงกัน — ต้นเหตุของ split-brain ที่ harness ฉีดเข้าไป แบบ single-scheduler ที่เขียนสองฝั่งตอนเครือข่ายขาด, heal, รัน anti-entropy ใต้ hard round budget แล้ว assert convergence + durability ผ่าน 500/500 seed (พร้อม non-vacuity 500/500 split-brain และ negative control ที่ยิง TIMEOUT after 50 rounds จาก merge ที่ไม่ idempotent); และ linearizability checker แบบ Wing-Gong ที่ตอบ true/false/true — ทำเครื่องหมายว่า store แบบ eventual-consistency ของเรา ไม่ linearizable โดย design (H2 -> false) ทุก snippet compile zero-warnings บน Rust 1.97.1 / std ล้วน และรันจบใต้ timeout 60 ไม่มีค้าง รันซ้ำ byte-identical
และความจริงที่บทนี้ยืนยันคือ: ผ่าน 500 seed คือการตรวจแบบมีขอบเขต ไม่ใช่บทพิสูจน์ — นี่คือเส้นแบ่งว่าทำไมสิ่งที่ property-test ได้ (quorum, CRDT, gossip) เราลง code แต่ consensus/Raft ที่ตรวจครบไม่ได้ (FLP 1985) ต้องอยู่ในกล่องไดอะแกรม
บท 8 (capstone): ตอนนี้เรามีทั้งชิ้นส่วน (บท 1–6) และเครื่องมือพิสูจน์ (บท 7) ครบแล้ว บทหน้าเราประกอบทุกอย่างเป็น cluster kaen-kvstore หลาย replica บน std::net — consistent-hash วาง key, quorum + read-repair, version vector ตรวจ conflict, CRDT merge แก้ conflict — แล้วขับด้วย harness ของบทนี้เพื่อ assert “ไม่มี acked write หาย” กับ “ลู่เข้าหลัง heal” ส่วน consensus/Raft จะอยู่ในกล่องไดอะแกรมเท่านั้น ด้วยเหตุผล FLP ที่บทนี้เพิ่งวางไว้
บทนี้อิงต้นทางที่ลงวันที่กำกับ อ่านต่อได้โดยตรง:
- Fischer, Lynch, Paterson — “Impossibility of Distributed Consensus with One Faulty Process” (JACM 32(2), 1985) (เข้าถึง 2026-07-24) — ไม่มี consensus แบบ asynchronous ที่การันตีทั้ง terminate และถูกต้องต่อ scheduler ปฏิปักษ์เมื่อมี node เจ๊งแม้แต่ตัวเดียว: รากฐานว่าทำไม “ผ่าน K seed” ไม่ใช่บทพิสูจน์ และทำไม consensus/Raft เป็นไดอะแกรมเท่านั้น
- Herlihy, Wing — “Linearizability: A Correctness Condition for Concurrent Objects” (TOPLAS 12(3), 1990) (เข้าถึง 2026-07-24) — นิยาม linearizability ที่ checker ในบทนี้ตรวจ: ลำดับรวมที่เคารพเวลาจริงและถูกต้องตาม object
- Gavin Lowe — “Testing for Linearizability” (Wing-Gong search, refined, 2017) (เข้าถึง 2026-07-24) — การ search แบบ backtracking ที่ checker ใช้ พร้อมเทคนิค pruning สำหรับ history ยาว (checker ในบทนี้ทำ history สั้นเพื่อกัน exponential blowup)
- Kyle Kingsbury — Jepsen: distributed-systems safety via fault injection + history checking (เข้าถึง 2026-07-24) — ระเบียบวิธีฉีด fault แล้วตรวจ history ที่ harness ในบทนี้เป็นรุ่นย่อ single-scheduler
- Steele, Lea, Flood — “Fast Splittable Pseudorandom Number Generators” (OOPSLA’14); ค่าคงที่ตาม splitmix64 ของ Vigna (2015) (เข้าถึง 2026-07-24) — PRNG ที่ seed ได้ deterministic เต็มตัว: seed เดียวให้ stream เดียวกันเป๊ะ แหล่งสุ่มของ property test ทั้งคอร์ส
เช็กความเข้าใจ — บทที่ 7
ข้อ 1 / 3ทำไม harness ฉีด partition ถึงต้องมี hard timeout (round budget) เสมอ ทั้งที่ code compile ผ่าน zero-warnings?