GC ตรวจแล้วว่า blob ไม่มี reference จึงตัดสินใจจะลบออกจาก S3 ระหว่างนั้น client อัปโหลด blob ที่มี digest เดิมและ commit reference ใหม่ลง MySQL จากนั้น GC ก็ลบ object ซึ่ง manifest ใหม่กำลังใช้งาน

ทั้งสามขั้นตอนทำงานถูกตามเงื่อนไขของตัวเอง แต่เมื่อนำมาสลับลำดับกัน ระบบกลับลบข้อมูลที่ยังมีชีวิต ปัญหานี้ไม่ได้อยู่ที่ syntax ของภาษาใดภาษาหนึ่ง แต่อยู่ตรงช่องว่างระหว่างเวลาที่ GC ตรวจสอบกับเวลาที่ GC ลงมือลบ รวมถึงการที่ MySQL กับ S3 ไม่มี transaction เดียวครอบทั้งสองระบบ

Depot อธิบายว่า TLC พบ race condition ลักษณะนี้ใน garbage collector ของ Depot Registry หลังจาก tests และ code review ไม่พบ สิ่งที่น่าสนใจสำหรับทีมที่ดูแลระบบ concurrent หรือ distributed จึงไม่ใช่แค่ “AI เขียน TLA+ ได้” แต่คือการใช้ Agent ลดแรงในการเริ่มทำแบบจำลอง แล้วให้มนุษย์รับผิดชอบคำถามที่สำคัญกว่า นั่นคือเราจำลองส่วนที่มีผลต่อความปลอดภัยครบหรือยัง และ invariant ที่ตั้งไว้ตรงกับสิ่งที่ระบบต้องรักษาจริงหรือไม่

Race เกิดขึ้นตรงไหนเมื่อข้อมูลอยู่คนละระบบ

Depot Registry เก็บ bytes ของ blob ไว้ใน S3 ใต้คีย์ blobs/sha256/<digest> แต่เก็บ reference ไว้ใน MySQL เมื่อ client อัปโหลด blob เดิมซ้ำ digest และคีย์จึงเหมือนเดิม ขณะที่การตรวจ reference กับการลบ object ไม่สามารถรวมอยู่ใน transaction เดียวกันได้

ลองแยกเหตุการณ์เป็นลำดับจะเห็นช่องโหว่ชัดขึ้น

1. GC อ่านข้อมูลจาก MySQL แล้วพบว่า blob ไม่มี reference จึงตัดสินใจจะลบ
2. client อัปโหลด blob digest เดิม และ commit reference ใหม่ลง MySQL
3. GC ลบ object ตามคีย์ที่ตรวจไว้ในขั้นแรก ทำให้ manifest ใหม่ชี้ไปยัง object ที่หายไป

ประโยคว่า “ไม่มี reference ตอนตรวจ” จึงไม่ได้แปลว่า “ลบได้อย่างปลอดภัยตอนลงมือ” เพราะ state หรือสถานะของระบบเปลี่ยนไประหว่างสองจังหวะนั้น สิ่งที่เราต้องสำรวจคือ interleaving หรือลำดับสลับกันของหลายกระบวนการ ไม่ใช่ดูความถูกต้องของแต่ละฟังก์ชันแยกจากกัน

คำถามด้านความปลอดภัยของกรณีนี้เขียนให้สั้นได้ว่า manifest ที่ commit แล้วต้องยังเข้าถึง blob data ได้เสมอ ประโยคนี้คือ invariant หรือเงื่อนไขที่ต้องจริงในทุก state ที่ระบบเข้าถึงได้ เมื่อมี invariant ชัด เราจึงถามเครื่องมือได้ว่า transition หรือการเปลี่ยนสถานะชุดใดทำให้เงื่อนไขนี้พัง

Tests รันโค้ดจริง แต่ TLC สำรวจลำดับในแบบจำลอง

Tests กับ model checking ให้หลักฐานคนละแบบ Tests รัน implementation จริงตามข้อมูลนำเข้าและ interleaving ที่ผู้เขียน test จัดไว้ ส่วน TLA+ ใช้อธิบายระบบเป็น state และ transition แล้วให้ TLC ซึ่งเป็น model checker สำรวจ state ที่เข้าถึงได้และลำดับการทำงานที่เป็นไปได้ใน model

ความต่างนี้สำคัญกับ race condition เพราะ test อาจครอบคลุมลำดับปกติและกรณีขอบที่ทีมคิดถึงแล้ว แต่ลำดับของ background workers, request และการตอบกลับจากหลายระบบเพิ่มจำนวนทางเลือกอย่างรวดเร็ว TLC ไม่ได้รัน Go, SQL หรือ S3 จริง มันสำรวจ interleaving ในแบบจำลองย่อที่เราเขียนขึ้น

ตรงนี้เป็นทั้งจุดแข็งและขอบเขตของวิธี แบบจำลองต้องเล็กพอให้ TLC สำรวจได้ แต่ต้องรักษาความสัมพันธ์ที่ทำให้คำถามด้านความปลอดภัยมีความหมาย หาก model ตัดรายละเอียดสำคัญทิ้ง ผลที่ได้ก็อาจบอกเพียงว่าแบบจำลองปลอดภัย ไม่ได้บอกว่าระบบจริงปลอดภัย

Depot รายงานว่า model ของ GC ซึ่งครอบคลุม concurrent pushers, กระบวนการ GC ในสองโดเมน, counter reconciler และ counter drift สำรวจ 14,290,224 states ในเวลาราว 21 นาที พร้อมตรวจ safety invariants 10 รายการและ liveness properties 2 รายการ ตัวเลขนี้เป็นผลของ model และ environment ที่ Depot ใช้ ไม่ใช่ตัวเลขสำหรับประเมินเวลาของระบบอื่น

เรียน TLA+ เท่าที่ต้องใช้เพื่อตั้งคำถามให้ถูก

คุณไม่จำเป็นต้องเริ่มจากการจำภาษา TLA+ ทั้งชุด ตัวอย่าง wallet แบบย่อช่วยให้เห็นวิธีคิดได้เร็วกว่า สมมติยอดเงินเริ่มที่ 10 และ client สองตัวต้องการถอนคนละ 8 โดยไม่มี lock ทั้ง A และ B ตรวจยอด 10 แล้วผ่านเงื่อนไขถอน จากนั้น A หัก 8 จากยอดปัจจุบันจนเหลือ 2 ส่วน B ซึ่งผ่านการตรวจจากค่าเดิมแล้วก็หัก 8 จากยอดปัจจุบันอีกครั้ง ยอดจึงลงไปที่ -6 และทำลาย invariant ต่อไปนี้

NoOverdraft == balance >= 0

ในสเปก TLA+ เครื่องหมาย /\ หมายถึง “และ” ส่วน \/ หมายถึง “หรือ” ตัวแปรที่มี prime เช่น balance' หมายถึงค่าของตัวแปรใน state ถัดไป รายละเอียดเท่านี้ก็พอให้เริ่มอ่าน transition และดูว่าเงื่อนไขใดเปลี่ยนค่าอะไร

สิ่งที่ยากกว่าการอ่านเครื่องหมายคือการเลือก abstraction หรือรายละเอียดที่แบบจำลองจะเก็บไว้ กรณีของ Depot ใช้ blob digest เดียว เพราะคำถามเฉพาะหน้าคือ GC อาจลบ blob ที่ manifest ต้องใช้หรือไม่ invariant ManifestNeedsData จึงตรวจว่าเมื่อมี manifest ที่ commit แล้ว ชุด S3 versions ต้องไม่ว่าง

ขอบเขตนี้ใช้ตอบคำถามของ model ตัวอย่างได้ แต่ยังไม่ได้ตรวจว่า version ที่เหลืออยู่ตรงกับ digest ของแต่ละ manifest หากขยายแบบจำลองให้มีหลาย digest เราต้องผูก S3 version เข้ากับ digest ที่ manifest อ้างถึง มิฉะนั้น invariant อาจยังผ่านเพียงเพราะมี version ของ blob คนละตัวเหลืออยู่

นี่คือเหตุผลที่การเขียน invariant ให้ดูน่าเชื่อยังไม่พอ ทีมต้องถามต่อว่าเงื่อนไขนั้นวัดสิ่งที่ต้องการรักษาจริงหรือไม่ และ model เก็บความสัมพันธ์ที่จำเป็นต่อการวัดไว้ครบหรือยัง

ให้ Agent ร่างสเปก แต่อย่าให้ Agent นิยามความถูกต้องแทนทีม

Depot อธิบายว่า Agent อ่าน implementation ซึ่งรวม Go transactions, SQL และ S3 calls แล้วช่วยแปลเป็น spec วิธีนี้ลดต้นทุนการเริ่มต้นได้มาก โดยเฉพาะทีมที่เข้าใจระบบของตัวเองแต่ยังไม่คล่อง TLA+

อย่างไรก็ตาม input ที่ดีกว่าโค้ดก้อนใหญ่คือ sequence diagram ที่ทีมตรวจแล้ว แผนภาพบังคับให้เราแยกผู้กระทำ จุดอ่าน จุดเขียน และ transaction boundary ออกจากรายละเอียด implementation ที่ไม่เกี่ยวกับคำถาม เมื่อทีมเห็น interleaving เดียวกันแล้ว จึงส่งแผนภาพให้ Agent ช่วยร่าง state, transition และ invariant

แบ่งหน้าที่ให้ชัดดังนี้

เริ่มตรวจจาก invariant ที่อ่านเป็นภาษาคนได้ เช่น “manifest ที่ commit แล้วต้องมี blob data” จากนั้นค่อยอ่าน transitions แบบ white-box เพื่อดูว่าแต่ละขั้นในสเปกตรงกับระบบหรือไม่ วิธีนี้ทำให้ทีมจับจุดผิดของความหมายได้ก่อนเสียเวลาแต่ง syntax ให้สวย

Counterexample เปลี่ยนข้อสงสัยให้เป็นงานออกแบบระบบ

เมื่อ TLC พบว่า invariant พัง มันจะให้ counterexample trace หรือลำดับเหตุการณ์ที่พา model ไปถึง state ที่ผิด อย่าเพิ่งตีความ trace ว่าเป็นคำตัดสินว่าระบบจริงมีบั๊ก ให้นำ trace กลับมาวาดเป็น sequence diagram แล้วตรวจทีละ transition

trace ทั้งลำดับเกิดใน implementation ได้จริงหรือไม่ แต่ละ transition มี precondition ครบหรือไม่ ขอบเขต transaction ตรงกันหรือไม่ model ยอมให้เหตุการณ์ที่ระบบห้ามไว้หรือเปล่า และ model ลืมเงื่อนไขที่ implementation บังคับใช้อยู่หรือไม่ คำตอบจะพาไปสู่หนึ่งในสองทาง คือแก้ design เพราะ trace เปิดเผย race จริง หรือแก้ model เพราะ abstraction ไม่ตรงกับระบบ

ในกรณี GC ของ Depot trace นำไปสู่แนวคิด การลบแบบมี version ID เป็นรั้ว ระบบเปิด S3 versioning เพื่อให้การอัปโหลดคีย์เดิมสร้าง version ใหม่ GC บันทึก version ID ที่เห็นตอนตรวจ แล้วลบเฉพาะ version นั้นแทนการลบทั้งคีย์

สมมติ GC เห็น v1 ก่อน ขณะเดียวกัน concurrent push สร้าง v2 และ commit reference ใหม่ เมื่อ GC กลับมาลบ มันจะลบเฉพาะ v1 ส่วน v2 ที่ manifest ใหม่อ้างถึงยังอยู่ Depot อธิบายว่า versioning ในกรณีนี้ทำหน้าที่เป็น delete fence ไม่ได้มีไว้เพื่อเก็บประวัติ blob กลไกนี้อธิบายเฉพาะ design ที่ GC จับ version ID ตรงกับ object ที่ตรวจและใช้งาน S3 versioning ตามที่กล่าวมา ไม่ใช่คำรับรองว่าการเปิด versioning เพียงอย่างเดียวทำให้ GC ทุกระบบปลอดภัย

อย่ารวม undercount กับ overcount เป็นปัญหาเดียวกัน

อีกส่วนของ model จำลอง reference counter ที่อาจคลาดเคลื่อน ระบบเพิ่ม counter ก่อนเริ่มงานและชดเชยด้วย decrement เมื่อทำงานล้มเหลว แต่หาก process crash ก่อนชดเชยเสร็จ reconciler ต้องเข้ามาซ่อมค่า

ใน PlusCal กระบวนการ DriftInjector ทำให้ counter ลดลงหรือเพิ่มขึ้นภายใต้งบที่กำหนด แล้ว TLC สำรวจทั้งสองทางเลือกแบบ nondeterministic พร้อม interleave เหตุการณ์เหล่านั้นกับ pushers, GC workers และ reconciler

ผลกระทบสองด้านไม่เท่ากัน Depot ระบุว่า overcount ทำให้ GC ช้าลงเพราะระบบคิดว่ายังมี reference มากกว่าความจริง ส่วน undercount อันตรายกว่า เพราะ GC อาจมอง blob ที่ยังถูกอ้างถึงว่าเป็น garbage แล้วลบข้อมูลจริง

ด้วยเหตุนี้ Depot จึงเสนอว่า ก่อน destructive step ระบบควรนับ physical link rows ใหม่แทนการเชื่อ stale counter ข้อเสนอนี้เกิดจากโครงสร้าง counter และ link rows ของระบบดังกล่าว ทีมอื่นควรนำหลักคิดกลับไปถามระบบตัวเองว่า ข้อมูลสรุปใดมีโอกาสคลาดเคลื่อน และก่อนลบจริงมีแหล่งข้อมูลพื้นฐานใดให้ตรวจซ้ำได้

Workflow ทดลองกับ flow เดียวโดยไม่ต้องจำลองทั้งระบบ

เลือก flow ที่ความเสียหายชัดและมีหลายกระบวนการแย่งกันทำงานก่อน ไม่ต้องยกทั้ง architecture มาเขียนเป็นสเปก ขั้นตอนทดลองรอบแรกทำได้ดังนี้

1. เลือก candidate หนึ่งจุด มองหา competing processes, transaction boundary ที่ซับซ้อน, worker ที่แข่งกันตามเวลา หรือการทำงานข้ามหลายระบบโดยไม่มี shared transaction งาน CRUD ทั่วไปที่อยู่ใน transaction เดียวมักไม่ใช่จุดเริ่มที่คุ้มที่สุด
2. วาด interleaving จากระบบจริง ระบุ actor, read, write, commit, retry และ destructive step ให้เห็นว่าเหตุการณ์ใดสลับตำแหน่งกันได้ แล้วให้ทีมที่ดูแล flow ช่วย review
3. ตัด model ให้เหลือคำถามเดียว เก็บเฉพาะ state และ transition ที่มีผลต่อความเสียหาย หากตัดความสัมพันธ์บางอย่างออก ให้บันทึกชัดว่า invariant จะไม่ครอบคลุมกรณีใด
4. เขียน invariant เป็นประโยคสั้น ระบุสิ่งที่ต้องจริงเสมอ เช่น “ทุก manifest ที่ commit แล้วต้องเข้าถึง blob ที่อ้างถึงได้” ประโยคนี้ควรชัดก่อนเริ่มเขียน TLA+
5. ให้ Agent ช่วยร่างสเปก TLA+ ใช้ sequence diagram ที่ผ่าน review เป็น input แล้วตรวจตัวแปร transitions และ invariant กับ implementation อีกครั้ง
6. รัน TLC และอ่าน trace เมื่อ invariant พัง ให้เปลี่ยน counterexample trace เป็น sequence diagram เพื่อให้ developer ที่ไม่รู้ TLA+ ช่วยตรวจได้
7. ตัดสินใจจากความตรงกับระบบจริง หาก trace ทั้งลำดับเกิดได้จริงภายใต้ precondition, transaction boundary และข้อบังคับของ implementation ให้แก้ design แล้วเพิ่ม tests รองรับกรณีนั้น หาก trace อาศัยพฤติกรรมที่ implementation ไม่อนุญาต ให้แก้ model และรันใหม่

จุดเริ่มที่ดีไม่ใช่คำถามว่า “Agent เขียน TLA+ เก่งแค่ไหน” แต่คือ “มี destructive flow จุดใดที่ความถูกต้องขึ้นกับจังหวะข้าม transaction หรือข้ามระบบ” เมื่อทีมเลือกคำถามได้เฉพาะพอ Agent จะช่วยแปลงความเข้าใจเป็นสเปกได้เร็วขึ้น และ TLC จะช่วยไล่ลำดับในขอบเขตที่ทีมกำหนด

คุณค่าของกระบวนการนี้จึงอยู่ที่วงจรตรวจทานร่วมกัน: คนกำหนดสิ่งที่ต้องจริง Agent ช่วยร่าง model TLC หา trace และคนย้อน trace กลับไปหา implementation อีกครั้ง วงจรนี้ไม่ได้แทน tests หรือ code review แต่เติมมุมที่เครื่องมือสองอย่างนั้นมักไม่ได้สำรวจครบ นั่นคือเหตุการณ์จากหลายกระบวนการที่แต่ละขั้นดูถูกต้อง แต่เมื่อสลับลำดับกันกลับทำให้ invariant พัง

ที่มา: Improving system safety with Temporal Logic of Actions (TLA+), Depot · อ่านต่อ: หน้าพูดคุยบทความบน Lobsters