CRDT แบบ state-based — semilattice, G-Counter, PN-Counter, LWW-Register
บท 3 ทิ้งปัญหาไว้ค้างคาโดยตั้งใจ: quorum แบบ W+R>N การันตีว่าการอ่านจะ เจอ write ล่าสุดเสมอ และ read-repair ตรวจจับ ได้ว่า2 replica มี version vector ที่ concurrent กัน — แต่พอเจอแล้ว มันได้แค่ flag ว่า “นี่คือ conflict” ยัง แก้ ไม่เป็น เมื่อสองลูกค้าเขียน key เดียวกันคนละ replica ในเวลาที่ไม่รู้เรื่องกัน (concurrent) เราจะเลือกค่าปลายทางอย่างไรให้ ทุก replica ลู่เข้าหาค่า เดียวกัน โดยไม่ต้องหยุดรอ coordinate กันก่อน?
คำตอบที่ Amazon Dynamo, Riak และ Cassandra ใช้จริงคือ CRDTCRDTชนิดข้อมูลที่ replica merge กันแล้วลู่เข้าเองโดยไม่ต้อง coordinate — หัวใจคือกฎ merge — ชนิดข้อมูลที่ออกแบบให้ merge ของมัน ลู่เข้าเองโดยพีชคณิต บทนี้เจาะ CRDT ตระกูล state-based (เรียกว่า CvRDT) แล้วสร้างสามชนิดพื้นฐาน — G-Counter, PN-Counter, LWW-Register — บนกฎ semilatticesemilatticeโครงพีชคณิตที่ merge เป็น join: commutative + associative + idempotent → ให้ least-upper-bound เดียวกับที่ merge ของ vector clock ในบท 1 เชื่อฟังอยู่แล้ว นี่ไม่ใช่เรื่องใหม่ทั้งหมด: กฎลู่เข้าที่บทนี้พิสูจน์คือ กฎเดียวกัน กับ element-wise max ที่คุณเขียนไปแล้วในบท 1 — เราแค่ยกมันขึ้นเป็น abstraction ที่ตั้งชื่อได้ และเอาไปประกอบเป็นชนิดข้อมูลจริง
คอร์สนี้ ต่อยอด repo kaen-kvstore จาก #22 (code ตัวอย่างกำลังจัดทำ) — บทนี้สร้าง CRDT ที่บท 5 จะเสียบเข้าไปเป็น ชนิดของ value ใน store โดยตรง (write จะ merge แทน overwrite) ทุก snippet ใช้ Rust std ล้วน: splitmix64 ที่เขียนเองเป็นแหล่งสุ่ม seed ซ้ำได้ 100% + BTreeMap/BTreeSet ที่เรียงลำดับ (canonical bytes) — ไม่มี serde, ไม่มี tokio, ไม่มี proptest ตามเส้น scope ของคอร์ส: CRDT อยู่ ฝั่งซ้าย (property-test ได้จริง) เพราะกฎ semilattice เอ็นนิวเมอเรต/สุ่มตรวจได้ ต่างจาก consensus/Raft ที่คงไว้เป็นไดอะแกรมเท่านั้น
ทุก snippet pin ที่ Rust stable 1.97.1 (ออก 2026-07-16) และ edition = “2024” [dependencies] ใน Cargo.toml ว่างเปล่า — ZERO external crate code ในบทนี้แตะ std เพียง std::collections (BTreeMap, BTreeSet) เท่านั้น ทุกโปรแกรม compile แบบ zero-warnings (-D warnings) และ รันจริง บน musl — เลขทุกตัวด้านล่างคือ output จริงที่ seed ล็อกไว้ รันซ้ำได้ byte-identical
ปัญหา: concurrent write ต้องการค่าปลายทางที่ทุก replica เห็นตรงกัน
หัวข้อที่มีชื่อว่า “ปัญหา: concurrent write ต้องการค่าปลายทางที่ทุก replica เห็นตรงกัน”ลองนึกภาพ shopping cart กระจายบน3 replica ลูกค้ากดเพิ่มของสองครั้งเกือบพร้อมกัน คำขอวิ่งไปคนละ replica เพราะ load balancer — ตอนนี้ replica A เห็น {milk} ส่วน replica B เห็น {bread} ทั้งคู่ ack กลับไปแล้ว ไม่มีใครผิด แล้วค่าจริงของ cart คืออะไร?
ทางเลือกแบบ “ให้ replica คุยกันก่อนแล้วโหวต” คือ consensus — มันถูกต้อง แต่ ต้องหยุดรับ write ระหว่าง partition (ความพร้อมใช้พัง) และเป็นสิ่งที่คอร์สนี้จงใจไม่ลง code (เส้น scope) CRDT เดินอีกทาง: ออกแบบชนิดข้อมูลให้ merge สองสถานะใดๆ ได้ผลลัพธ์ที่ถูกต้องเสมอ ไม่ว่าจะ merge เมื่อไร ลำดับใด ซ้ำกี่ครั้ง ถ้าทำได้ replica ไม่ต้อง coordinate เลย — เขียนได้ตลอดแม้ตอน partition แล้วค่อย merge กันทีหลังตอนเครือข่ายกลับมา ผลลัพธ์รับประกันว่าลู่เข้า
คำถามคือ: merge แบบไหนที่ให้การรับประกันนั้น? คำตอบเป็นทฤษฎีบทพีชคณิตที่คมชัดมาก
ทฤษฎีบท: merge ต้องเป็น join ของ semilattice
หัวข้อที่มีชื่อว่า “ทฤษฎีบท: merge ต้องเป็น join ของ semilattice”Shapiro และคณะ (2011) พิสูจน์ว่า state-based object จะลู่เข้า (ทุก replica ที่เห็นชุด update เดียวกันจบที่ค่าเดียวกัน) ก็ต่อเมื่อ สถานะของมันเป็น join-semilattice และ merge คำนวณ least upper bound (LUB) ของสองสถานะ พูดเป็นภาษา code: merge ต้องมีสมบัติสามข้อ
- commutative —
merge(a, b) == merge(b, a): ลำดับที่ state มาถึงไม่มีผล (เครือข่ายส่งข้อความสลับลำดับ) - associative —
merge(merge(a, b), c) == merge(a, merge(b, c)): การจับกลุ่มไม่มีผล (จะ merge ทีละคู่แบบไหนก็ได้) - idempotent —
merge(a, a) == a: merge สถานะเดิมซ้ำกี่ครั้งก็เท่าเดิม
สามข้อนี้แปลตรงตัวเป็นสามภัยของระบบกระจายที่ถูก ทำให้ไม่มีผล: commutative ลบล้างการ สลับลำดับ, associative ลบล้างการ จับกลุ่มต่างกัน, idempotent ลบล้างการ ส่งซ้ำ/redelivery ผลรวมคือ replica ไม่ต้องประสานงานกันบน write path เลย — คุณสมบัตินี้เรียกว่า Strong Eventual Consistency และมันไม่ต้องใช้ consensus นี่คือ เหตุผลเชิงพีชคณิต ว่าทำไม CRDT ถึงลง code รันจริงได้ในคอร์สนี้ ในขณะที่ Raft ทำไม่ได้: สามกฎนี้สุ่มตรวจได้ แต่ correctness ของ Raft ต่อ adversarial scheduler เอ็นนิวเมอเรตไม่ได้
commutative กับ associative นั้นคนมักเดาถูก แต่ idempotence คือข้อที่แยก CRDT ออกจากตัวนับธรรมดา มันคือสิ่งที่ทำให้ anti-entropyanti-entropyกระบวนการเบื้องหลังที่ให้ replica เทียบสถานะแล้ว sync ส่วนที่ต่างกันจนลู่เข้ากัน (บท 6) ส่งสถานะทั้งก้อนซ้ำๆ ได้อย่างมั่นใจ โดยไม่กลัวนับซ้ำ — ถ้า merge ไม่ idempotent การ retry หนึ่งครั้งก็ทำค่าเพี้ยนถาวร (Shapiro et al. 2011 §3.2)
เราจะเขียนกฎสามข้อนี้เป็น harness เดียว ที่ใช้ซ้ำได้กับ CRDT ทุกชนิด ผ่าน trait:
// A state-based CRDT converges IFF `merge` is a join on a semilattice:// commutative + associative + idempotent (Shapiro et al. 2011).trait Crdt: Clone { fn merge(&self, other: &Self) -> Self; // Semantic equality (implicit-zero aware for counters): two states that // MEAN the same must compare equal even if their maps differ in shape. fn equals(&self, other: &Self) -> bool;}
// one reusable harness that checks the 3 laws over random triplesfn semilattice_laws<T: Crdt>( rng: &mut SplitMix64, cases: u32, mut gen_val: impl FnMut(&mut SplitMix64) -> T,) -> (u32, u32) { let (mut checks, mut violations) = (0u32, 0u32); for _ in 0..cases { let a = gen_val(rng); let b = gen_val(rng); let c = gen_val(rng); // commutative: merge(a,b) == merge(b,a) -> reordering has no effect if !a.merge(&b).equals(&b.merge(&a)) { violations += 1; } checks += 1; // associative: (a|b)|c == a|(b|c) -> grouping has no effect if !a.merge(&b).merge(&c).equals(&a.merge(&b.merge(&c))) { violations += 1; } checks += 1; // idempotent: merge(a,a) == a -> re-delivery / duplication has no effect if !a.merge(&a).equals(&a) { violations += 1; } checks += 1; } (checks, violations)}parameter ที่นี่ชื่อ gen_val ไม่ใช่ gen — ใน edition 2024 คำว่า gen กลายเป็น reserved keyword (สำหรับ gen block) ถ้าตั้งชื่อ field หรือ parameter ว่า gen code จะ compile ไม่ผ่านทันที เป็นกับดักที่เจอจริงในรอบนี้
สังเกตว่า equals เขียนเองไม่ derive — ด้วยเหตุผลเดียวกับ PartialEq ของ vector clock ในบท 1: counter ที่ช่องหายไปหมายถึง 0 โดยปริยาย {0:3} ต้องเท่ากับ {0:3, 1:0} เชิงความหมาย ถ้า derive บน BTreeMap ตรงๆ มันจะบอกว่าต่างกันเพราะจำนวน key ไม่เท่า
G-Counter: ตัวนับเพิ่มอย่างเดียว, merge = max ทีละช่อง
หัวข้อที่มีชื่อว่า “G-Counter: ตัวนับเพิ่มอย่างเดียว, merge = max ทีละช่อง”G-CounterG-Counterตัวนับเพิ่มอย่างเดียว: เวกเตอร์ต่อ node, merge = max ทีละช่อง, ค่า = ผลรวม (grow-only counter) คือ CRDT ที่ง่ายที่สุด: map จาก node → ตัวนับ กฎมีข้อเดียวที่ต้องจำ — แต่ละ node บวกได้เฉพาะช่องของ ตัวเอง ค่ารวมของ counter คือ ผลรวม ทุกช่อง แต่ merge คือ max ทีละช่อง — ไม่ใช่ผลรวม
#[derive(Clone)]struct GCounter { counts: BTreeMap<u64, u64>,}impl GCounter { fn new() -> Self { Self { counts: BTreeMap::new() } } // A node bumps ONLY its own slot -- never anyone else's. fn inc(&mut self, node: u64, by: u64) { *self.counts.entry(node).or_insert(0) += by; } fn value(&self) -> u64 { self.counts.values().sum() }}impl Crdt for GCounter { fn merge(&self, other: &Self) -> Self { let mut out = self.clone(); for (&n, &c) in &other.counts { let e = out.counts.entry(n).or_insert(0); if c > *e { *e = c; // MAX, never SUM: SUM double-counts on re-delivery (not idempotent) } } out } fn equals(&self, other: &Self) -> bool { let mut keys: BTreeSet<u64> = self.counts.keys().copied().collect(); keys.extend(other.counts.keys().copied()); keys.iter().all(|k| { self.counts.get(k).copied().unwrap_or(0) == other.counts.get(k).copied().unwrap_or(0) }) }}ทำไม merge ต้องเป็น max ไม่ใช่ sum? เพราะ sum ไม่ idempotent ลองคิดตาม: node 0 บวกไป 3 ครั้ง ช่องของมันเป็น {0:3} ถ้า anti-entropy ส่งสถานะนี้ให้เพื่อนแล้วเพื่อนตอบกลับสถานะเดิม — ถ้า merge เป็น sum ค่าจะกลายเป็น {0:6} ทั้งที่ node 0 บวกจริงแค่ 3 การส่งซ้ำ (ซึ่งในระบบกระจายเกิด ตลอดเวลา) ทำค่าเพี้ยน max ไม่มีปัญหานี้: max(3, 3) = 3 ส่งซ้ำกี่ครั้งก็เท่าเดิม แต่ละ node เป็นเจ้าของช่องตัวเองคนเดียว ค่าในช่องนั้นจึงเพิ่มขึ้น อย่างเดียว (monotone) — max จึงกู้ค่าล่าสุดของทุกเจ้าของกลับมาได้ครบ นี่คือโครงเดียวกับ vector clock ในบท 1 เป๊ะ (vector clock ที่ grow-only คือ G-Counter map นั่นเอง)
flowchart LR
A["replica A<br/>inc(0,3)<br/>{0:3}"]
B["replica B<br/>inc(1,5)<br/>{1:5}"]
M["merge = max ทีละช่อง<br/>{0:3, 1:5}<br/>value = 3+5 = 8"]
A -->|"ส่ง state ให้ B"| M
B -->|"ส่ง state ให้ A"| M
M -->|"merge ซ้ำ / สลับลำดับ<br/>ก็ได้ 8 เท่าเดิม"| M
คำบรรยายภาพ: replica A กับ B ต่างบวกช่องของตัวเอง แล้ว merge เข้าหากันทั้งสองทิศ — merge = max ทีละช่อง ให้ {0:3, 1:5} ค่ารวม 8 เท่ากันทั้งสองฝั่ง; ลำดับที่ merge และการ merge ซ้ำ (idempotent) ไม่มีผลต่อ 8
PN-Counter: บวก-ลบได้ ด้วย G-Counter สองตัว
หัวข้อที่มีชื่อว่า “PN-Counter: บวก-ลบได้ ด้วย G-Counter สองตัว”G-Counter บวกได้อย่างเดียว จะให้ลบ (เช่นลดจำนวนสินค้าใน cart) ไม่ได้ — ถ้าอนุญาตให้ค่าในช่องลดลง max จะ “กิน” การลดหายไป (max ระหว่างค่าเก่าที่มากกว่ากับค่าใหม่ที่น้อยกว่า จะได้ค่าเก่า) ทางแก้แบบ CRDT คลาสสิกคือ PN-Counter: เก็บ G-Counter สองตัว — P สำหรับยอดบวกสะสม, N สำหรับยอดลบสะสม — ค่าจริงคือ P.sum − N.sum ทั้งสองตัวยังเป็น grow-only (การลบ = เพิ่ม ยอดในตัวนับ N) กฎ semilattice จึงสืบทอดมาฟรีๆ
#[derive(Clone)]struct PNCounter { p: GCounter, // increments n: GCounter, // decrements}impl PNCounter { fn new() -> Self { Self { p: GCounter::new(), n: GCounter::new() } } fn inc(&mut self, node: u64, by: u64) { self.p.inc(node, by); } fn dec(&mut self, node: u64, by: u64) { self.n.inc(node, by); } fn value(&self) -> i64 { self.p.value() as i64 - self.n.value() as i64 }}impl Crdt for PNCounter { fn merge(&self, other: &Self) -> Self { Self { p: self.p.merge(&other.p), n: self.n.merge(&other.n) } } fn equals(&self, other: &Self) -> bool { self.p.equals(&other.p) && self.n.equals(&other.n) }}merge แค่ merge ตัว P กับ N แยกกัน — เพราะ CRDT ประกอบกันได้ (compose): product ของ2 semilattice ก็ยังเป็น semilattice จุดที่ห้ามพลาดคือ ห้ามอนุญาต by ที่เป็นลบใน inc — ถ้าปล่อยให้ยอดในช่อง P ลดลงได้ max จะกลืนมันหาย ต้องบังคับว่า inc เข้า P, dec เข้า N เท่านั้น
รัน property test: กฎ semilattice บน 3000 triples ต่อชนิด
หัวข้อที่มีชื่อว่า “รัน property test: กฎ semilattice บน 3000 triples ต่อชนิด”ตอนนี้เอา G-Counter กับ PN-Counter ป้อนเข้า semilattice_laws seed ล็อกที่ 0xDEADBEEF (G-Counter) และ 0x12345678 (PN-Counter) อย่างละ 3000 triples — แต่ละ triple ตรวจ 3 กฎ = 9000 checks ต่อชนิด:
fn main() { // worked examples let mut a = GCounter::new(); a.inc(0, 3); // replica on node 0 -> {0:3} let mut b = GCounter::new(); b.inc(1, 5); // replica on node 1 -> {1:5} let g = a.merge(&b).merge(&a); // merge both ways + a DUPLICATE delivery println!("G-Counter merge {{0:3}} | {{1:5}} (+ dup) -> value={}", g.value());
let mut pn = PNCounter::new(); pn.inc(0, 4); pn.inc(1, 6); pn.dec(0, 4); // +4 +6 -4 println!("PN-Counter +4 +6 -4 -> value={}", pn.value());
let cases = 3000u32; let mut rng_g = SplitMix64::new(0xDEADBEEF); let (gc, gv) = semilattice_laws(&mut rng_g, cases, |r| random_gcounter(r, 5, 6)); let mut rng_p = SplitMix64::new(0x12345678); let (pc, pv) = semilattice_laws(&mut rng_p, cases, |r| random_pncounter(r, 5, 6)); println!("G-Counter seed=0xdeadbeef : checks={gc} violations={gv}"); println!("PN-Counter seed=0x12345678 : checks={pc} violations={pv}"); assert_eq!(gv, 0); assert_eq!(pv, 0); println!("ALL SEMILATTICE LAWS HOLD.");}รันจริงบน musl:
G-Counter merge {0:3} | {1:5} (+ dup) -> value=8PN-Counter +4 +6 -4 -> value=6--- semilattice laws (comm/assoc/idem), 3000 triples each ---G-Counter seed=0xdeadbeef : checks=9000 violations=0PN-Counter seed=0x12345678 : checks=9000 violations=0ALL SEMILATTICE LAWS HOLD.worked example ยืนยันความหมาย: G-Counter {0:3} merge {1:5} แล้ว merge {0:3} ซ้ำอีกครั้ง (จำลอง redelivery) ได้ค่า 8 เท่าเดิม — idempotence ทำงานจริง; PN-Counter บวก 4 บวก 6 ลบ 4 ได้ 6 ถูกต้อง และกฎทั้งสามผ่านทุก triple: 9000 checks, 0 violations ต่อชนิด
negative control: harness ที่ปริ้นต์ 0 ได้อย่างเดียวคือ harness ที่ไร้ค่า
หัวข้อที่มีชื่อว่า “negative control: harness ที่ปริ้นต์ 0 ได้อย่างเดียวคือ harness ที่ไร้ค่า”test ที่ผ่านเสมอไม่ได้พิสูจน์อะไร — มันอาจจะ ตรวจไม่เจอ อะไรเลยก็ได้ เราจึงต้องรัน negative control อย่างน้อยหนึ่งครั้ง: สลับ merge ของ G-Counter จาก max เป็น sum (bug คลาสสิก) แล้วดูว่า harness จับได้ไหม sum ยัง commutative และ associative แต่ ไม่ idempotent:
#[derive(Clone)]struct BadCounter { counts: BTreeMap<u64, u64> }impl Crdt for BadCounter { fn merge(&self, other: &Self) -> Self { let mut out = self.clone(); for (&n, &c) in &other.counts { *out.counts.entry(n).or_insert(0) += c; // SUM: merge(a,a) DOUBLES -> not idempotent } out } // equals identical to GCounter's ...}// ... run BadCounter through the SAME semilattice_laws harness, seed 0xDEADBEEF:--- negative control: G-Counter with merge = SUM (wrong) ---BadCounter seed=0xdeadbeef : checks=9000 violations=2952harness CAUGHT the broken merge (2952 violations) -> the check has teeth.2952 จาก 9000 — ทุก violation คือ triple ที่ merge(a, a) != a (idempotence พัง) การเห็นเลขนี้มากกว่า 0 คือหลักฐานว่า harness มีฟัน จริง ถ้ามันปริ้นต์ 0 ให้ทั้งของถูกและของผิด มันก็ไม่ได้ตรวจอะไรเลย — จำนวน violation ที่แน่นอน (2952) ขึ้นกับ generator และ seed ที่ pin ไว้ จึงรันซ้ำได้เท่าเดิมทุกครั้ง
LWW-Register: ts สูงสุดชนะ + tie-break ที่ต้อง deterministic
หัวข้อที่มีชื่อว่า “LWW-Register: ts สูงสุดชนะ + tie-break ที่ต้อง deterministic”counter ทั้งสองด้านบน ไม่เสียข้อมูล — ทุก inc ถูกนับครบ แต่บางครั้งเราอยาก แทนที่ ค่า ไม่ใช่สะสม (เช่นเก็บ “ที่อยู่ล่าสุดของผู้ใช้”) นั่นคืองานของ LWW-RegisterLWW-Registerรีจิสเตอร์ค่าเดียวที่ timestamp สูงสุดชนะ — ทิ้ง write ที่ concurrent (lossy โดย design) (last-writer-wins): เก็บค่าเดียวพร้อม timestamp, merge = เลือกตัวที่ ts สูงกว่า ฟังดูตรงไปตรงมา แต่มีกับดักลึก
ปัญหาคือ ts อย่างเดียว ไม่เป็น total order — 2 replica ประทับ ts เดียวกันได้สบายๆ (นาฬิกาหยาบ หรือ logical clock ชนกัน) ถ้า merge เจอ ts เท่ากันแล้วไม่มีกฎตัดสินที่ deterministic มันจะเลือกคนละค่าบนคนละ replica → merge ไม่ commutative → ไม่ลู่เข้า ทางแก้คือทำ tuple (ts, node, val) ให้เป็น total order เต็ม โดยใช้ node id (และค่าเป็นด่านสุดท้าย) เป็น tie-break:
#[derive(Clone)]struct Lww { ts: u64, node: u64, val: Vec<u8>,}impl Crdt for Lww { fn merge(&self, other: &Self) -> Self { // Tuple/Vec<u8> lexicographic Ord IS the total order. The tie can only // happen when the two are byte-identical, so the pick is deterministic // and commutative either way. if (self.ts, self.node, &self.val) >= (other.ts, other.node, &other.val) { self.clone() } else { other.clone() } } fn equals(&self, other: &Self) -> bool { self.ts == other.ts && self.node == other.node && self.val == other.val }}หัวใจคือบรรทัด (self.ts, self.node, &self.val) >= (...): Rust เทียบ tuple แบบ lexicographic ให้ฟรี และ Vec<u8> เทียบแบบ byte lexicographic — 3 field รวมกันจึงเป็น total order จริง ไม่มีทางเสมอเว้นแต่ทั้งก้อนเท่ากันเป๊ะ merge จึงเลือกตัวเดิมเสมอไม่ว่าเรียงลำดับ argument แบบไหน = commutative
รัน (seed 0x0C0FFEE0, 3000 triples):
LWW concurrent {red@n0, blue@n1} -> "blue" (the other write is SILENTLY LOST)--- LWW-Register semilattice laws, 3000 triples ---LWW seed=0x0c0ffee0 : checks=9000 violations=0ALL SEMILATTICE LAWS HOLD (tie-break makes merge a real total-order join).worked example: 2 write concurrent ประทับ ts=7 เท่ากัน — red จาก node 0, blue จาก node 1 tie-break ด้วย node id: 1 > 0 → blue ชนะ และ red ถูกทิ้งเงียบๆ นี่คือจุดที่ต้องพูดตรง: LWW lossy โดย design — มันไม่ได้ แก้ conflict แต่ เลือกฝ่ายชนะแล้วโยนอีกฝ่ายทิ้ง (Kleppmann, DDIA ch5) เหมาะกับข้อมูลที่ “ค่าล่าสุดคือความจริง” (last-seen presence, config flag) แต่ถ้าเอาไปใช้กับ cart หรือ balance คุณจะ เสีย order ที่ลูกค้ากดจริง เงียบๆ โดยไม่มี error งานแบบนั้นต้องใช้ PN-Counter (นับครบ) หรือ OR-SetOR-Setเซ็ต add-wins: ทุก add ติด tag ไม่ซ้ำ, remove ลบได้เฉพาะ tag ที่เห็นแล้ว → re-add ที่ concurrent รอด ที่บท 5 จะสร้าง (add-wins ไม่ทิ้ง concurrent add)
Thread A — Rust พิสูจน์ความถูกต้อง “ในเครื่องเดียว” ไม่ใช่ “แบบกระจาย”: property test 9000 checks/ชนิด คือ ออราเคิล ของสมบัติลู่เข้า และมันคือการ ตรวจแบบมีขอบเขต ไม่ใช่บทพิสูจน์ — ผ่าน 3000 triples แปลว่าสำรวจเฉพาะสถานะที่ splitmix64 สุ่มไปถึง กฎ semilattice นั้นพิสูจน์ได้ทางคณิตศาสตร์ (Shapiro 2011) แต่ code implementation ของเราตรวจด้วยการสุ่ม negative control (2952 violations) คือหลักประกันว่า harness มีฟัน
Thread B — เส้น scope: CRDT อยู่ ฝั่งซ้าย (ลง code รันจริง) เพราะสามกฎ comm/assoc/idem สุ่มตรวจได้ตรงๆ ต่างจาก consensus/Raft ที่ state space ของ partition/reorder ระเบิดจนเอ็นนิวเมอเรตไม่ได้ — จึงคงเป็นไดอะแกรมในบท 8
Thread D — นี่คือกลไกจริงของ Dynamo/Riak/Cassandra: G-Counter/PN-Counter/LWW-Register คือ CRDT ที่ระบบเหล่านี้ใช้จริง (Cassandra ใช้ LWW เป็น default conflict resolution) — เราสอนตรงตามต้นฉบับ Shapiro et al. 2011 ที่สเกล toy บน kaen-kvstore ไม่ใช่ของกุขึ้นเพื่อสอน
สรุปก่อนไปต่อ
หัวข้อที่มีชื่อว่า “สรุปก่อนไปต่อ”บทนี้แก้ปัญหาที่บท 3 ทิ้งไว้: concurrent write ที่ read-repair ตรวจเจอ แต่ แก้ไม่เป็น CRDTCRDTชนิดข้อมูลที่ replica merge กันแล้วลู่เข้าเองโดยไม่ต้อง coordinate — หัวใจคือกฎ merge แบบ state-based (CvRDT) แก้ด้วยพีชคณิต — ทฤษฎีบท Shapiro et al. 2011: replica ลู่เข้าหาค่าเดียวกัน ก็ต่อเมื่อ merge เป็น join ของ semilatticesemilatticeโครงพีชคณิตที่ merge เป็น join: commutative + associative + idempotent → ให้ least-upper-bound คือ commutative (ลบล้างการสลับลำดับ) + associative (ลบล้างการจับกลุ่ม) + idempotent (ลบล้างการส่งซ้ำ) → Strong Eventual Consistency ไม่ต้องใช้ consensus เราสร้างสามชนิดบนกฎเดียวกับ element-wise max ของ vector clock ในบท 1: G-CounterG-Counterตัวนับเพิ่มอย่างเดียว: เวกเตอร์ต่อ node, merge = max ทีละช่อง, ค่า = ผลรวม (แต่ละ node บวกช่องตัวเอง, merge = max ทีละช่อง, ค่า = ผลรวม — max ไม่ใช่ sum เพราะ sum ไม่ idempotent), PN-Counter (G-Counter สองตัว P−N, ห้าม inc ค่าลบ), LWW-RegisterLWW-Registerรีจิสเตอร์ค่าเดียวที่ timestamp สูงสุดชนะ — ทิ้ง write ที่ concurrent (lossy โดย design) (ts สูงสุดชนะ + tie-break (ts, node, val) ที่ deterministic — lossy โดย design ทิ้ง concurrent write ที่แพ้เงียบๆ) property test splitmix64 ยืนยันกฎทั้งสาม 9000 checks/0 violations ต่อชนิด และ negative control (merge = sum) โดน harness จับได้ 2952 ครั้ง — พิสูจน์ว่าการตรวจมีฟันจริง ทุก snippet compile zero-warnings บน Rust 1.97.1 / edition 2024 / std ล้วน
บท 5 เราเอา CRDT ไปเสียบเป็น ชนิดของ value จริงใน kaen-kvstore: เราจะสร้าง OR-SetOR-Setเซ็ต add-wins: ทุก add ติด tag ไม่ซ้ำ, remove ลบได้เฉพาะ tag ที่เห็นแล้ว → re-add ที่ concurrent รอด (add-wins ที่ ไม่ ทิ้ง concurrent add แบบ LWW) แล้วเก็บมันเป็น value ที่ write จะ merge แทน overwrite — โดยเข้ารหัสด้วย wire format length-prefixed จาก #22 (ไม่ใช้ serde) ทำให้ convergence พิสูจน์ได้ถึงระดับ byte
บทนี้อิงต้นทางที่ลงวันที่กำกับ อ่านต่อได้โดยตรง:
- Shapiro, Preguiça, Baquero, Zawirski — “A Comprehensive Study of Convergent and Commutative Replicated Data Types” (INRIA RR-7687, 2011) (เข้าถึง 2026-07-24) — ทฤษฎีบทหลักของบทนี้: state-based object ลู่เข้า ก็ต่อเมื่อ merge เป็น join ของ join-semilattice (comm/assoc/idem) ที่คำนวณ LUB; นิยาม G-Counter, PN-Counter และบทบาทของ idempotence ต่อ anti-entropy (§3.2)
- Martin Kleppmann — “Designing Data-Intensive Applications”, ch5 Replication (2017) (เข้าถึง 2026-07-24) — LWW เก็บ write ที่ timestamp สูงสุดและ ทิ้ง concurrent write อย่างเงียบๆ (lossy โดย design); concurrent write ต้องการ LWW หรือ CRDT เพื่อเลือกค่า; CRDT เป็น stack จริงของ Dynamo-style stores
เช็กความเข้าใจ — บทที่ 4
ข้อ 1 / 3ทำไม merge ของ G-Counter ต้องเป็น max ทีละช่อง ไม่ใช่ผลรวม (sum)?