จากนาฬิกา Lamport สู่ vector clock — กู้ลำดับเชิงเหตุผลที่ scalar ทำไม่ได้

คุณจบ #21 (rust-from-scratch) กับ #22 (rust-kvstore) มาแล้ว — ในมือคุณมี kaen-kvstore: key-value store บนเครือข่ายที่เป็น node เดียว เขียน SET/GET/DELETE ผ่าน wire protocol ที่ออกแบบเอง, append-only log + hash index, write→fsync→ack, tombstone/compaction และ thread pool ครบแล้ว คอร์สนี้ ต่อยอด ของชิ้นนั้นโดยตรง ไม่สอน Rust ซ้ำและไม่รื้อ store เขียนใหม่ — เราจะ เลื่อน kaen-kvstore จาก node เดียวขึ้นเป็น cluster ที่หลาย replica เก็บสำเนา key เดียวกัน แล้วยังลู่เข้าหาค่าเดียวกันได้แม้เครือข่ายจะขาด

แต่ก่อนจะพูดเรื่อง replica, quorum หรือ CRDT ได้เลย เราติดปัญหาที่เก่าแก่ที่สุดของระบบกระจายก่อน: เมื่อ event เกิดขึ้นคนละเครื่อง เราจะรู้ได้อย่างไรว่าอะไรเกิดก่อนอะไร คำตอบไม่ใช่ “ดูนาฬิกา” — บทนี้วางรากฐาน เวลาเชิงตรรกะ (logical time) ที่ทุกบทหลังจากนี้ต้องยืนอยู่บนมัน: version vector ที่ read-repair (บท 3) และ CRDT (บท 4–5) ใช้ตรวจ conflict ล้วนเป็น vector clock ที่เราสร้างในบทนี้

📦 kaen-kvstore

คอร์สนี้ ต่อยอด repo kaen-kvstore จาก #22 (code ตัวอย่างกำลังจัดทำ) — ตลอด 8 บทเราเลื่อน kaen-kvstore จาก single-node ขึ้นเป็น replicated cluster ด้วย Rust std ล้วน: splitmix64 ที่เขียนเองเป็นแหล่งสุ่มที่ seed ซ้ำได้ 100% + std SipHash (DefaultHasher) — ไม่มี serde, ไม่มี tokio, ไม่มี proptest เลยทั้งคอร์ส THE SCOPE LINE: เราลง code รันจริง เฉพาะส่วนที่ property-test ได้ (logical clock, consistent hashing, quorum, CRDT, anti-entropy, harness ฉีด partition) — ส่วน consensus/Raft ที่ตรวจครบไม่ได้ คงไว้เป็น ไดอะแกรม เท่านั้น บทนี้วางรากฐาน causal ordering (vector clock) ที่บท 3–8 ใช้ซ้ำ และตั้ง precedent ของ honesty spine กับ 🔗 callout อ้างอิงต้นทางให้ทุกบทเดินตาม

toolchain ที่ pin ไว้ + std ที่บทนี้ใช้

ทุก snippet pin ที่ Rust stable 1.97.1 (ออก 2026-07-16) และ edition = “2024” — เช็กเองด้วย rustc --version ได้เสมอ [dependencies] ใน Cargo.toml ว่างเปล่าตลอดคอร์ส — ZERO external crate code ในบทนี้แตะ std เพียง std::collections (HashMap, HashSet) กับ std::cmp (Ordering) เท่านั้น ทุกโปรแกรมในบทนี้ compile แบบ zero-warnings และ รันจริง — เลขทุกตัวที่เห็นด้านล่างคือ output จริงที่ seed ล็อกไว้ รันซ้ำได้ byte-identical

นาฬิกาข้อมือบอกลำดับ event ข้ามเครื่องไม่ได้

สัญชาตญาณแรกของทุกคนคือ “ก็ประทับเวลา (timestamp) ลงทุก event สิ แล้วเรียงตามเวลา” — บน node เดียวมันใช้ได้ แต่พอข้ามเครื่อง มันพังด้วยเหตุผลที่ลึกกว่าที่คิด

นาฬิกาจริงของสองเครื่องไม่มีทางตรงกันเป๊ะ มันไหล (drift) คนละอัตรา ต่างกันได้เป็นหลักมิลลิวินาทีถึงวินาที นั่นคือ clock skew ที่แย่กว่านั้น: ตัว NTP ที่คอยดึงนาฬิกาให้ตรงเอง เดินถอยหลังได้ — เมื่อมันแก้ค่าที่เพี้ยน นาฬิกาอาจกระโดดย้อนกลับ ผลคือเหตุการณ์ที่เกิด ทีหลัง อาจได้ timestamp น้อยกว่า เหตุการณ์ที่เกิดก่อน พูดให้ชัด: ถ้าเครื่อง A ส่งข้อความไปเครื่อง B แล้วเราเทียบ timestamp ดิบๆ เราอาจสรุปว่า ข้อความมาถึงก่อนที่มันจะถูกส่ง — ซึ่งเป็นไปไม่ได้เชิงเหตุผล

Lamport ชี้ในปี 1978 ว่าปัญหาที่แท้จริงไม่ใช่ “เวลา” แต่คือ ลำดับ — และลำดับที่เราสนใจจริงๆ คือลำดับ เชิงเหตุผล (causal): event a เกิดก่อน b ในความหมายที่ มีผล ก็ต่อเมื่อ a อาจส่งผล ถึง b ได้ ความสัมพันธ์นี้เรียกว่า happens-before เขียนแทนด้วย a → b นิยามด้วยกฎง่ายๆ สามข้อ: (1) ถ้า a กับ b อยู่ node เดียวกันและ a มาก่อน แล้ว a → b; (2) ถ้า a คือการส่งข้อความและ b คือการรับข้อความนั้น แล้ว a → b; (3) transitive — ถ้า a → b และ b → c แล้ว a → c คู่ที่ ไม่ เชื่อมกันด้วยกฎเหล่านี้เลยคือ concurrent (เขียน a ‖ b) — ไม่ใช่ว่ามันเกิดพร้อมกันตามเวลาจริง แต่คือ ไม่มีทางที่ตัวหนึ่งจะรู้เรื่องอีกตัว

ประเด็นคือ happens-before เป็น partial order (ลำดับบางส่วน) ไม่ใช่ total order — บางคู่เทียบกันไม่ได้เลย และนั่นคือคือหัวใจ เราต้องการนาฬิกาเชิงตรรกะที่ เคารพ ความเป็น partial order นี้ ไม่ใช่บดมันให้แบนเป็นเส้นเดียว

นาฬิกา Lamport: เวลาเชิงตรรกะที่การันตี “ทางเดียว”

ก้าวแรกของ Lamport คือ Lamport clock — ตัวนับ integer ตัวเดียว (scalar) ต่อ node กฎมีแค่สองข้อ: ทุก event ในเครื่อง (รวมการส่ง) ให้ tick คือบวกหนึ่ง; เวลารับข้อความที่พก timestamp msg มา ให้ตั้งค่าเป็น max(local, msg) + 1 การ max ดึงให้ผู้รับ “ก้าวนำ” ผู้ส่งเสมอ

// Lamport scalar clock: tick on a local event; on receive, L = max(local, msg)+1.
// Guarantee (one-way): a -> b  =>  L(a) < L(b).
// Limitation: the converse is FALSE -- L(a) < L(b) does not imply a -> b,
// because a scalar imposes a TOTAL order and cannot express concurrency.
#[derive(Clone, Copy, Debug)]
struct LamportClock {
    t: u64,
}

impl LamportClock {
    fn new() -> Self {
        Self { t: 0 }
    }
    fn event(&mut self) -> u64 {
        self.t += 1;
        self.t
    }
    fn recv(&mut self, msg: u64) -> u64 {
        self.t = self.t.max(msg) + 1;
        self.t
    }
}

fn main() {
    let mut p = LamportClock::new();
    let mut q = LamportClock::new();

    // Causal chain P: p1 (send) ; Q receives it as r.
    let p1 = p.event(); // 1, P sends a message stamped 1
    let r = q.recv(p1); // max(0,1)+1 = 2, so p1 -> r and L(p1)=1 < L(r)=2. GOOD.
    println!("causal link: L(p1)={p1} < L(r)={r}  (p1 -> r holds)");
    assert!(p1 < r, "a->b must imply L(a)<L(b)");

    // Now an event on P that is CONCURRENT with r (no message links them).
    let p2 = p.event(); // 2
    println!("concurrent pair: L(p2)={p2}, L(r)={r}  (p2 and r have NO causal path)");

    // Scalar clock still forces a numeric comparison between concurrent events.
    // Here they tie at 2; a real system breaks ties by node id to get a total
    // order -- but that order is arbitrary, NOT causal. And in the general case
    // L(x) < L(y) can hold for a concurrent pair, falsely suggesting x -> y.
    println!("scalar clock yields a TOTAL order; it CANNOT flag p2 || r as concurrent.");
    println!("=> need vector clocks to recover the causal PARTIAL order.");
}

รันจริงบน musl ได้ผลตามนี้:

causal link: L(p1)=1 < L(r)=2  (p1 -> r holds)
concurrent pair: L(p2)=2, L(r)=2  (p2 and r have NO causal path)
scalar clock yields a TOTAL order; it CANNOT flag p2 || r as concurrent.
=> need vector clocks to recover the causal PARTIAL order.

สิ่งที่ Lamport clock การันตี คือกฎ ทางเดียว: ถ้า a → b แล้ว L(a) < L(b) เสมอ (Lamport, CACM 1978) — ในตัวอย่าง p1 → r จริง และได้ L(p1)=1 < L(r)=2 สมจริง กฎนี้มีประโยชน์มาก: ถ้าเห็น L(a) ≥ L(b) เรามั่นใจได้ว่า a ไม่ได้ เกิดก่อน b

แต่ บทกลับเป็นเท็จ — L(a) < L(b) ไม่ได้ แปลว่า a → b ในตัวอย่างเดียวกัน p2 กับ r เป็น concurrent (ไม่มีข้อความเชื่อมกัน) แต่ scalar clock ก็ยังยัดให้ทั้งคู่มีค่าเทียบกันได้ — ที่นี่บังเอิญเสมอกันที่ 2 ในกรณีทั่วไป L(x) < L(y) อาจเป็นจริงสำหรับคู่ concurrent ด้วยซ้ำ ทำให้เข้าใจผิดว่า x → y ต้นตอของข้อจำกัดนี้คือ scalar หนึ่งค่า บังคับให้เกิด total order เสมอ — มันบดลำดับ partial ของ happens-before ให้แบนเป็นเส้นเดียว ข้อมูลว่า “คู่นี้เทียบกันไม่ได้” หายไปตั้งแต่ตอนบันทึกลงตัวนับตัวเดียว

vector clock: จับ causality ให้ครบถ้วน

ทางแก้คือเก็บ ตัวนับต่อ node แทนตัวเดียว — vector clock คือ map จาก node_id → counter โดยที่ key ที่หายไปหมายถึง 0 โดยปริยาย (สำคัญมาก จะอธิบายต่อ) กฎขยับจากของ Lamport ตรงๆ: event ในเครื่องให้ tick เฉพาะช่องของ ตัวเอง; เวลารับข้อความให้ merge ก่อนแล้วค่อย tick ช่องตัวเอง โดย merge คือเอา element-wise max ทีละช่องเหนือ union ของ key ทั้งสองฝั่ง

code ต่อไปนี้คือหัวใจของทั้งคอร์ส — SplitMix64 (แหล่งสุ่ม seed ได้ที่ใช้ซ้ำทุกบท) กับ VectorClock:

use std::cmp::Ordering;
use std::collections::HashMap;

// ---------- splitmix64: seed-reproducible PRNG (pure std, no crates) ----------
struct SplitMix64 {
    state: u64,
}
impl SplitMix64 {
    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
    }
}

// ---------- VectorClock: node_id -> counter; a MISSING entry means 0 ----------
#[derive(Clone, Debug)]
struct VectorClock {
    entries: HashMap<u64, u64>,
}

impl VectorClock {
    fn new() -> Self {
        Self { entries: HashMap::new() }
    }
    fn get(&self, node: u64) -> u64 {
        *self.entries.get(&node).unwrap_or(&0)
    }
    // Local event at `node`: bump this node's own component.
    fn tick(&mut self, node: u64) {
        *self.entries.entry(node).or_insert(0) += 1;
    }
    // LUB / join: element-wise max over the union of node ids.
    fn merge(&self, other: &Self) -> Self {
        let mut out = self.clone();
        for (&n, &c) in &other.entries {
            let e = out.entries.entry(n).or_insert(0);
            if c > *e {
                *e = c;
            }
        }
        out
    }
    // Deliver a message carrying clock `msg` at receiver `node`: join then tick.
    fn receive(&mut self, msg: &Self, node: u64) {
        *self = self.merge(msg);
        self.tick(node);
    }
    fn union_keys(&self, other: &Self) -> Vec<u64> {
        let mut ks: Vec<u64> = self.entries.keys().copied().collect();
        for k in other.entries.keys() {
            if !self.entries.contains_key(k) {
                ks.push(*k);
            }
        }
        ks
    }
}

tick ใช้ += ธรรมดา (ไม่ใช่ wrapping_add) โดยตั้งใจ — นาฬิกาเชิงตรรกะ ห้าม วน (wrap) ถ้ามันวนกลับเป็น 0 ได้ ลำดับเหตุผลจะพังทันที ต่างจากตัว hash ในบท 2 ที่จงใจให้ล้นได้

ทำไมต้องเขียน `PartialEq`/`PartialOrd` เอง — และทำไม derive คือ bug

นี่คือจุดที่คนพลาดกันมากที่สุด ถ้าคุณเผลอ #[derive(PartialEq)] บน VectorClock ที่หลังบ้านเป็น HashMap มันจะเทียบว่า 2 map มี key-value ตรงกันเป๊ะไหม — แต่นั่น ผิดความหมายของ vector clock เพราะ {a:1} ต้อง เท่ากับ {a:1, b:0} (ช่องที่หายไป = 0 โดยปริยาย) derived eq จะบอกว่ามันไม่เท่ากันเพราะจำนวน key ต่างกัน เราจึงต้องเขียนเองให้เทียบทุก key ใน union โดยถือ key ที่ขาด = 0 ผ่าน get:

// Semantic equality: equal on every component (implicit zeros included), so
// {a:1} == {a:1, b:0}. Derived PartialEq on the HashMap would get this WRONG.
impl PartialEq for VectorClock {
    fn eq(&self, other: &Self) -> bool {
        self.union_keys(other).iter().all(|&k| self.get(k) == other.get(k))
    }
}
impl Eq for VectorClock {}

// happens-before PARTIAL order:
//   a < b  (a -> b)  iff  a[k] <= b[k] for all k AND a != b
//   a || b (concurrent) iff neither a <= b nor b <= a  -> partial_cmp is None
impl PartialOrd for VectorClock {
    fn partial_cmp(&self, other: &Self) -> Option<Ordering> {
        let (mut lt, mut gt) = (false, false);
        for k in self.union_keys(other) {
            let (a, b) = (self.get(k), other.get(k));
            if a < b {
                lt = true;
            }
            if a > b {
                gt = true;
            }
        }
        match (lt, gt) {
            (false, false) => Some(Ordering::Equal),
            (true, false) => Some(Ordering::Less),
            (false, true) => Some(Ordering::Greater),
            (true, true) => None, // concurrent
        }
    }
}

partial_cmp นี่แหละคือสิ่งที่ Lamport clock ทำไม่ได้ มันไล่ทุก key ใน union แล้วดูว่ามีช่องไหนที่ฝั่งซ้าย น้อยกว่า (lt) และมีช่องไหนที่ มากกว่า (gt) หรือไม่ ผลลัพธ์แยกได้สี่ทาง: ไม่มีทั้งคู่ = Equal; มีแต่ lt = Less (คือ a → b); มีแต่ gt = Greater; มีทั้งคู่ = None = concurrent จุดตายที่ต้องระวัง: partial_cmp ที่ให้ผลเป็น total เสมอ (เช่นไปคืน Some(Less) แทน None ในกรณี (true, true)) จะทำลายการตรวจจับ concurrency ทั้งหมด — คุณจะได้ scalar clock กลับมาในคราบ vector

ตัวอย่างเดินเรื่อง: กู้ concurrency ที่ scalar ทำหล่น

เอาสถานการณ์เดิมจากหัวข้อ Lamport มารันด้วย vector clock: P ส่ง p1, Q รับเป็น r, แล้ว P ทำ p2 โดยไม่รู้เรื่อง r:

    // P sends p1; Q receives -> r; P then does p2 concurrently with r.
    let mut p = VectorClock::new();
    let mut q = VectorClock::new();
    p.tick(0); // p1  => {0:1}
    let p1_msg = p.clone();
    q.receive(&p1_msg, 1); // r => {0:1, 1:1}
    p.tick(0); // p2  => {0:2}
    let r = q.clone();
    println!("p1 -> r ?      {:?}", p1_msg.partial_cmp(&r)); // Some(Less)
    println!("p2 vs r  ?     {:?}", p.partial_cmp(&r)); // None => concurrent (correct!)
    assert_eq!(p1_msg.partial_cmp(&r), Some(Ordering::Less));
    assert_eq!(p.partial_cmp(&r), None);

p1 -> r ?      Some(Less)
p2 vs r  ?     None

p1 = {0:1} เทียบกับ r = {0:1, 1:1} ได้ Some(Less) — vector clock ยืนยัน p1 → r เหมือน Lamport ส่วน p2 = {0:2} เทียบกับ r = {0:1, 1:1}: ช่อง 0 ฝั่ง p2 มากกว่า (2 > 1) แต่ช่อง 1 ฝั่ง r มากกว่า (1 > 0) — มีทั้ง lt และ gt จึงได้ None = concurrent นี่คือสิ่งที่ scalar ทำหล่นไป: มันบอกได้ตรงๆ ว่า p2 กับ r เทียบกันไม่ได้

นี่คือ ทฤษฎีบท Fidge–Mattern (Fidge 1988 / Mattern 1989): vector clock จับ causality ได้ ครบถ้วนพอดี — a → b ก็ต่อเมื่อ V(a) < V(b) และ a ‖ b ก็ต่อเมื่อ เวกเตอร์ทั้งสองเทียบกันไม่ได้ (incomparable) ไม่ใช่แค่ทางเดียวอย่าง Lamport แต่เป็น isomorphism — เวกเตอร์เก็บโครง partial order ของ happens-before ไว้ทั้งดุ้น

sequenceDiagram
    participant P as โพรเซส P
    participant Q as โพรเซส Q
    Note over P: p1 — tick(0) → V={0:1}
    P->>Q: ส่งข้อความพก V={0:1}
    Note over Q: r — merge แล้ว tick(1) → V={0:1, 1:1}
    Note over P: p2 — tick(0) → V={0:2} (P ยังไม่รู้เรื่อง r)
    Note over P,Q: p1 → r (มีลูกศรเชื่อม) แต่ p2 ‖ r (ไม่มีเส้นเหตุผลถึงกัน)

คำบรรยายภาพ: เส้นเหตุผล vs เหตุการณ์ที่ concurrent — p1 → r เชื่อมด้วยลูกศรข้อความ (V(p1) < V(r)), ส่วน p2 ห้อยอยู่บนเส้นเวลาของ P โดยไม่มีเส้นเหตุผลถึง r: scalar แยกไม่ออก (ยัดให้เทียบกันได้เสมอ), vector แยกออก (คืน None)

merge คือ join ของ semilattice (LUB) — กฎที่บท 3–8 ใช้ซ้ำ

ย้อนกลับไปดู merge: มันคือ element-wise max เหนือ union ของ key เท่านั้นเอง แต่ operation นี้มีโครงสร้างพีชคณิตที่ทรงพลัง มันคือ join ของ semilattice — คือ least upper bound (LUB) ของสองสถานะ และมันมีสมบัติสามข้อที่จะเป็นหัวใจของทั้งคอร์ส:

commutative — merge(a, b) == merge(b, a): ลำดับที่ merge ไม่มีผล
associative — merge(merge(a, b), c) == merge(a, merge(b, c)): การจับกลุ่มไม่มีผล
idempotent — merge(a, a) == a: merge ซ้ำกี่ครั้งก็เท่าเดิม

สามข้อนี้แปลว่า ลำดับการส่ง, การส่งซ้ำ, การส่งซ้อน ล้วนไม่มีผลต่อค่าปลายทาง — replica ที่เห็นชุดข้อความเดียวกัน (ไม่ว่าลำดับใด) จะลู่เข้าหาสถานะเดียวกันเสมอ โดยไม่ต้อง coordinate กันเลย พูดอีกอย่าง grow-only vector clock มีโครงเหมือน G-Counter map เป๊ะ นี่คือ กฎลู่เข้าเดียวกับ CRDT ที่บท 4–5 จะสร้างบนมัน และเป็นเหตุผลว่าทำไม read-repair (บท 3) ถึงเอา LUB มาเขียนกลับได้อย่างปลอดภัย เราจะพิสูจน์สามกฎนี้ด้วย code ในหัวข้อถัดไป

property test: พิสูจน์กฎ semilattice + ทฤษฎีบท Fidge–Mattern

การเขียน distributed algorithm ให้ “ดูเหมือนถูก” นั้นง่าย — มัน compile ผ่านและเดโมสวย แต่ subtle bug ซ่อนได้ทน เราจึงใช้ property test: สุ่ม input เป็นพันๆ ชุดด้วย splitmix64 (seed คงที่ = รันซ้ำได้ 100%) แล้ว ยืนยันสมบัติ ทุกชุด ไม่ใช่เช็คแค่ตัวอย่างเดียว

ชุดแรก: กฎ semilattice ทั้งสาม + upper-bound + การตรวจ LUB แบบ ไม่เป็นสุญญากาศ seed ล็อกที่ 0xDDD_C0FFEE, 5 node, 3000 เคส:

fn random_clock(rng: &mut SplitMix64, n_nodes: u64, max_c: u64) -> VectorClock {
    let mut vc = VectorClock::new();
    for node in 0..n_nodes {
        match rng.below(4) {
            0 => {}                                   // leave absent (implicit 0)
            1 => { vc.entries.insert(node, 0); }      // explicit 0 (eq must handle)
            _ => { vc.entries.insert(node, rng.below(max_c + 1)); }
        }
    }
    vc
}

fn main() {
    // ... worked example above ...

    let seed: u64 = 0xDDD_C0FFEE;
    let mut rng = SplitMix64::new(seed);
    let (n_nodes, max_c, cases) = (5u64, 6u64, 3000u32);
    let (mut comm, mut assoc, mut idem, mut ub) = (0u32, 0u32, 0u32, 0u32);
    let (mut least_qualified, mut least_probes) = (0u32, 0u32);

    for _ in 0..cases {
        let a = random_clock(&mut rng, n_nodes, max_c);
        let b = random_clock(&mut rng, n_nodes, max_c);
        let c = random_clock(&mut rng, n_nodes, max_c);

        assert!(a.merge(&b) == b.merge(&a), "commutativity failed");
        comm += 1;
        assert!(a.merge(&b).merge(&c) == a.merge(&b.merge(&c)), "associativity failed");
        assoc += 1;
        assert!(a.merge(&a) == a, "idempotency failed");
        idem += 1;

        // upper bound: m >= a and m >= b (never concurrent with an input)
        let m = a.merge(&b);
        assert!(a <= m && b <= m, "merge is not an upper bound");
        ub += 1;

        // LEAST upper bound (honest conditional): draw random candidates; for any
        // candidate d that HAPPENS to be a common upper bound of {a,b}, m must
        // divide it (m <= d). Count how many candidates actually qualified so the
        // test cannot pass vacuously.
        for _ in 0..3 {
            let d = random_clock(&mut rng, n_nodes, max_c + 3); // wider => more qualify
            least_probes += 1;
            if a <= d && b <= d {
                assert!(m <= d, "merge is not the LEAST upper bound");
                least_qualified += 1;
            }
        }
    }
    // ... prints, then: assert!(least_qualified > 0) ...
}

--- splitmix64 property test (seed=0xdddc0ffee, 3000 cases) ---
commutative  merge(a,b)==merge(b,a)            : 3000/3000 PASS
associative  (a|b)|c == a|(b|c)               : 3000/3000 PASS
idempotent   merge(a,a)==a                    : 3000/3000 PASS
upper bound  a<=merge & b<=merge              : 3000/3000 PASS
least u.b.   m<=d for every common upper bound : 440 qualifying of 9000 probes PASS
ALL semilattice/LUB laws hold on 3000 random clocks.

สังเกตบรรทัดสุดท้าย: จาก 9000 candidate ที่สุ่มมา มีแค่ 440 ตัวที่ เข้าเงื่อนไข เป็น common upper bound ของ {a, b} จริง (แล้ว m ≤ d ทุกตัว) การพิมพ์ least_qualified ออกมาแล้ว assert!(least_qualified > 0) คือการกันไม่ให้ test ผ่านแบบสุญญากาศ — ถ้าไม่มี candidate ไหนเข้าเงื่อนไขเลย if ข้างในจะไม่เคยรัน แล้ว “PASS” จะไม่มีความหมาย 440 คือหลักฐานว่าเราได้ตรวจ LUB จริงๆ

ชุดที่สองคือ gold standard: causality.rs สร้าง ground-truth ancestor set แยกต่างหากจากตัว clock แล้วเทียบทฤษฎีบท Fidge–Mattern บน ทุกคู่ที่เรียงลำดับ มันจำลอง execution แบบสุ่ม 60 รอบ (per-run seed = 0xA11CE*(run+1)+0x5EED) แต่ละรอบ 60 event บน 4 node แล้วสำหรับทุกคู่ (i, j) ตรวจว่าคำตอบของ clock (partial_cmp) ตรงกับ ground truth (i อยู่ในเซ็ตบรรพบุรุษของ j ไหม) หรือไม่:

// A recorded event: the node it ran on, its VC snapshot after, and the GROUND-TRUTH
// set of event indices that causally precede it (built independently of the VC).
struct Event { vc: VectorClock, ancestors: HashSet<usize> }

fn simulate(seed: u64, n_nodes: u64, steps: usize) -> Vec<Event> {
    let mut rng = SplitMix64::new(seed);
    let mut clocks: Vec<VectorClock> = (0..n_nodes).map(|_| VectorClock::new()).collect();
    let mut last_on_node: Vec<Option<usize>> = vec![None; n_nodes as usize];
    let mut inflight: Vec<(usize, VectorClock)> = Vec::new(); // (send event idx, clock)
    let mut log: Vec<Event> = Vec::new();

    for _ in 0..steps {
        let p = rng.below(n_nodes);
        // If messages are waiting, sometimes deliver one (random order = interleaving).
        let do_recv = !inflight.is_empty() && rng.below(2) == 0;
        let mut anc: HashSet<usize> = HashSet::new();
        if let Some(prev) = last_on_node[p as usize] {
            anc.extend(log[prev].ancestors.iter().copied());
            anc.insert(prev);                            // program-order ancestry
        }
        if do_recv {
            let pick = rng.below(inflight.len() as u64) as usize;
            let (s_idx, msg) = inflight.swap_remove(pick);
            clocks[p as usize].receive(&msg, p);
            anc.extend(log[s_idx].ancestors.iter().copied());
            anc.insert(s_idx);                           // message-order ancestry
        } else {
            clocks[p as usize].tick(p);
        }
        let idx = log.len();
        // 50% of local events also send a message carrying the current clock.
        if !do_recv && rng.below(2) == 0 {
            inflight.push((idx, clocks[p as usize].clone()));
        }
        last_on_node[p as usize] = Some(idx);
        log.push(Event { vc: clocks[p as usize].clone(), ancestors: anc });
    }
    log
}

หัวใจอยู่ที่ ancestors สร้างจากกฎ happens-before ตรงๆ (program order + message order + transitive closure) โดยไม่แตะ vector clock เลย — มันคือ oracle อิสระ แล้ว main ก็เทียบทุกคู่:

    for i in 0..log.len() {
        for j in 0..log.len() {
            if i == j { continue; }
            let causal = log[j].ancestors.contains(&i);        // ground truth: e_i -> e_j
            let ord = log[i].vc.partial_cmp(&log[j].vc);
            let vc_before = ord == Some(Ordering::Less);
            assert_eq!(causal, vc_before, ...);                // Fidge-Mattern, both ways
            assert_ne!(ord, Some(Ordering::Equal), ...);       // distinct events, distinct VC
            if !log[j].ancestors.contains(&i) && !log[i].ancestors.contains(&j) {
                assert_eq!(ord, None, ...);                    // concurrent <=> incomparable
                n_conc += 1;
            }
            if causal { n_before += 1; }
        }
    }

--- Fidge-Mattern theorem check over random interleavings ---
runs=60  nodes=4  events/run=60
ordered pairs checked : 212400
  causal (e_i -> e_j) : 63346  -> all matched VC strict-less
  concurrent pairs    : 85708  -> all matched VC = None
VC partial order == happens-before, on every pair. PASS.

212,400 คู่ (60 รอบ × 60 event × 59) ผ่านทุกคู่: 63,346 คู่ที่เป็น causal ตาม ground truth → clock คืน Some(Less) ทุกตัว; 85,708 คู่ที่ concurrent → clock คืน None ทุกตัว; และไม่มี event สองตัวที่ต่างกัน share เวกเตอร์เดียวกันเลย ทฤษฎีบท Fidge–Mattern จับต้องได้ใน code ที่รันจริง ไม่ใช่แค่คำกล่าวอ้าง

ราคาของความแม่นยำ: O(N) — และเส้น scope

ความแม่นยำนี้มีราคา Charron-Bost พิสูจน์ในปี 1991 ว่า ไม่มีนาฬิกาเชิงตรรกะที่ใช้ integer น้อยกว่า N ตัวแล้วยังจับ happens-before ของระบบ N โพรเซสได้ครบ — พูดง่ายๆ vector clock ที่ยาว N ช่องนั้น เล็กที่สุดเท่าที่เป็นไปได้ ถ้าอยากได้ causality เป๊ะๆ ย่อไม่ได้อีกแล้ว บน cluster ที่ node เข้า-ออกเรื่อยๆ เวกเตอร์จะโตไม่หยุด

ระบบจริง (Dynamo, Riak) จึงใช้ version vector ที่ key ด้วย ผู้เขียน (ไม่ใช่ทุก node) แล้ว prune ทิ้งช่องเก่าเมื่อ causally stable — เราจะ เอ่ยถึง มันในบท 3–5 แต่ บทนี้ยึดเส้น scope ชัด: เราลง code vector clock ที่ property-test ได้จริง (แบบเต็ม N ช่อง ตรงตามทฤษฎี) ส่วน pruning ของ real store เป็น การกล่าวถึง เท่านั้น และ consensus ไม่แตะในคอร์สนี้เลย — เหตุผลอยู่ใน callout ถัดไป

honesty spine 4 เส้น ที่ทั้งคอร์สยึด (บทนี้ตั้ง precedent ครบทั้งสี่)

A — Rust พิสูจน์ความถูกต้อง “ในเครื่องเดียว” ไม่ใช่ “แบบกระจาย”: borrow checker การันตีว่าไม่มี data race ใน process เดียว แต่มัน มองไม่เห็น การสลับลำดับข้อความ, partition, หรือ clock skew — vector clock ที่ subtle-wrong ก็ยัง compile ผ่านและเดโมสวยได้ property test กับ harness (บท 7) คือ “ออราเคิล” ของสมบัติแบบกระจาย และมันคือการ ตรวจแบบมีขอบเขต ไม่ใช่บทพิสูจน์ (FLP 1985) — ผ่าน 212,400 คู่แปลว่าสำรวจเฉพาะ interleaving ที่ seed เดินไปถึง ไม่ใช่ทุกความเป็นไปได้

B — เส้น scope: สิ่งที่ เอ็นนิวเมอเรตหรือ property-test ได้ (logical clock, quorum arithmetic, กฎ semilattice) เราลง code รันจริง; ส่วน consensus/Raft ที่ ตรวจครบไม่ได้ (state space ของ partition/reorder ระเบิด) คงไว้เป็น กล่องไดอะแกรม เท่านั้น — บทนี้อยู่ฝั่งซ้ายของเส้นทั้งบท

C — ดีเทอร์มินิสซึมคือวินัย: seed คงที่ (0xDDD_C0FFEE) + single-scheduler + พิมพ์ seed ออกมาเป็น repro handle มิฉะนั้น test จะ โกหก (รันแดงซ้ำไม่ได้) เราใช้ splitmix64 เขียนเองแทน proptest และจะใช้ BTreeMap แทน HashMap ตรงที่ลำดับ iteration ป้อน logic (บทหลัง)

D — นี่คือกลไกจริงของ Dynamo/Cassandra/Riak: vector/version vector + quorum + CRDT + Merkle + gossip คือ stack จริงของ Amazon Dynamo — เราสอน ตรงตามต้นฉบับ ที่สเกล toy บน kaen-kvstore ไม่ใช่ของกุขึ้นเพื่อสอน

สรุปก่อนไปต่อ

บทนี้วางรากฐาน เวลาเชิงตรรกะ ของทั้งคอร์ส: นาฬิกา wall-clock บอกลำดับ event ข้ามเครื่องไม่ได้ (skew + NTP เดินถอยหลัง → “มาถึงก่อนถูกส่ง”) เราจึงหันไปหา happens-before ที่เป็น partial order; Lamport clock แบบ scalar การันตีทางเดียว a → b ⇒ L(a) < L(b) แต่บทกลับเป็นเท็จเพราะ scalar บังคับ total order แยก concurrent ไม่ออก; vector clock ที่เก็บตัวนับต่อ node (key หาย = 0) จับ causality ครบตามทฤษฎีบท Fidge–Mattern — a → b ก็ต่อเมื่อ V(a) < V(b), concurrent ก็ต่อเมื่อ incomparable; merge = element-wise max = join ของ semilattice (LUB) ที่ commutative/associative/idempotent — กฎลู่เข้าเดียวกับ CRDT ที่บท 3–8 ใช้ซ้ำ; เราต้องเขียน PartialEq/PartialOrd เองเพราะ derive บน HashMap เป็น bug (implicit-zero) และ partial_cmp ต้องคืน None ให้ concurrent ไม่ใช่ยัด Some; ราคาคือ O(N) (Charron-Bost) ย่อกว่านี้ไม่ได้ ทุก snippet compile zero-warnings บน Rust 1.97.1 / edition 2024 / std ล้วน และรันได้เลขตามที่เห็น

บท 2 เราวางข้อมูลลง cluster: ตอนนี้เรารู้แล้วว่าจะ เรียงลำดับ เหตุการณ์ข้าม node อย่างไร บทหน้าเราจะถามว่า key แต่ละตัว ควรอยู่ node ไหน — ด้วย consistent hashing + virtual node ที่ทำให้เพิ่ม node ใหม่แล้วย้าย key แค่ ~1/(N+1) ไม่ใช่ทั้ง cluster โดยใช้ std DefaultHasher (SipHash) ที่เราจะพูดความจริงเรื่อง hash-sensitivity กันตรงๆ

🔗 อ้างอิงต้นทางของบทนี้

บทนี้อิงต้นทางที่ลงวันที่กำกับ อ่านต่อได้โดยตรง:

Leslie Lamport — “Time, Clocks, and the Ordering of Events in a Distributed System” (CACM, 1978) (เข้าถึง 2026-07-24) — ต้นกำเนิดของ happens-before และ scalar clock: a → b ⇒ C(a) < C(b) เป็นจริงทางเดียว บทกลับเป็นเท็จ (scalar บังคับ total order แยก concurrent ไม่ได้)
Colin Fidge — “Logical Time in Distributed Computing Systems” (IEEE Computer 24(8), 1991) (เข้าถึง 2026-07-24) — บทความที่เข้าถึงง่ายซึ่งนำเสนอผลพาร์เชียลออร์เดอร์ปี 1988 ของ Fidge เอง: vector clock จับ partial order ได้ครบ a → b ก็ต่อเมื่อ V(a) < V(b) (ต้นฉบับคือ Fidge, Proc. 11th Australian Computer Science Conf., 1988)
Friedemann Mattern — “Virtual Time and Global States of Distributed Systems” (1989) (เข้าถึง 2026-07-24) — นิยาม vector clock อิสระคู่ขนานกับ Fidge; ครึ่งอีกส่วนของ isomorphism ที่บทนี้พิสูจน์ด้วย code
Bernadette Charron-Bost — “Concerning the size of logical clocks in distributed systems” (IPL 39(1), 1991) (เข้าถึง 2026-07-24) — ไม่มีนาฬิกาเชิงตรรกะที่ใช้ integer น้อยกว่า N ตัวแล้วยังจับ happens-before ของระบบ N โพรเซสได้ครบ (ที่มาของ O(N))

เช็กความเข้าใจ — บทที่ 1

ข้อ 1 / 3

ทำไมนาฬิกา Lamport แบบ scalar ถึงบอกไม่ได้ว่า event สองตัวเป็น concurrent?

จาก​นาฬิกา Lamport สู่ vector clock — กู้​ลำดับ​เชิง​เหตุผล​ที่ scalar ทำ​ไม่​ได้

นาฬิกา​ข้อ​มือ​บอก​ลำดับ event ข้าม​เครื่อง​ไม่​ได้

นาฬิกา Lamport: เวลา​เชิง​ตรรกะ​ที่​การันตี “ทาง​เดียว”

vector clock: จับ causality ให้​ครบถ้วน

ทำไม​ต้อง​เขียน PartialEq/PartialOrd เอง — และ​ทำไม derive คือ bug

ตัวอย่าง​เดิน​เรื่อง: กู้ concurrency ที่ scalar ทำ​หล่น

merge คือ join ของ semilattice (LUB) — กฎ​ที่​บท 3–8 ใช้​ซ้ำ

property test: พิสูจน์​กฎ semilattice + ทฤษฎีบท Fidge–Mattern

ราคา​ของ​ความ​แม่นยำ: O(N) — และ​เส้น scope

สรุป​ก่อน​ไป​ต่อ