เมื่อ AWS ประสบปัญหาวงจรบริการล่มอย่างรุนแรงในเดือนตุลาคม 2023 รายงานการวิเคราะห์เหตุการณ์หลังจากเกิดปัญหา (post-mortem) ที่เผยแพร่โดยละเอียดได้เปิดเผยข้อผิดพลาดเชิงเงื่อนไขการแข่งขัน (race condition) ที่ซับซ้อนในระบบจัดการ DNS ของพวกเขา แม้ว่าทีมวิศวกรของ AWS จะมีประวัติความน่าเชื่อถือที่น่าประทับใจ แต่เหตุการณ์นี้ก็แสดงให้เห็นว่ายังไงระบบที่ทันสมัยที่สุดก็สามารถตกเป็นเหยื่อของบั๊กที่เกี่ยวข้องกับการทำงานพร้อมกันได้ ชุมชนด้านเทคนิคต่างวิเคราะห์อย่างกว้างขวางถึงสิ่งที่ผิดพลาดและว่าวิธีการตรวจสอบอย่างเป็นทางการ (formal verification) จะสามารถป้องกันความล้มเหลวนี้ได้หรือไม่
ส่วนประกอบสำคัญในเหตุการณ์ DNS ของ AWS:
- DNS Planner: สร้างแผน DNS
- DNS Enactor: นำแผนไปใช้กับ Route 53 (3 อินสแตนซ์กระจายอยู่ตาม availability zones)
- Route 53 Service: เว็บเซอร์วิส DNS ของ Amazon
- Race Condition: enactor ที่เร็วกว่าจะนำแผนใหม่ไปใช้และทำความสะอาดแผนเก่า ในขณะที่ enactor ที่ช้ากว่ายังคงใช้แผนเก่าอยู่
อคติจากการมองย้อนกลับในการออกแบบระบบ
ผู้แสดงความคิดเห็นจำนวนมากตั้งข้อสังเกตว่าเงื่อนไขการแข่งขันเฉพาะเจาะจงนี้ — ซึ่งกระบวนการหนึ่งลบแผน DNS ที่ยังใช้งานอยู่ที่กระบวนการอื่นกำลังใช้อยู่ — ดูเหมือนจะชัดเจนเมื่อมองย้อนกลับ มีผู้ใช้หนึ่งคนอธิบายความรู้สึกนี้ได้อย่างแม่นยำ: เงื่อนไขคงที่ (invariant) นั้นชัดเจนในย้อนหลัง แต่มันแทบจะไม่ใช่สิ่งที่เห็นได้ชัดตั้งแต่แรก นี่แสดงให้เห็นถึงความท้าทายพื้นฐานในการออกแบบระบบแบบกระจาย (distributed systems): ความล้มเหลวที่ดูเรียบง่ายหลังจากเกิดขึ้นแล้วนั้นยากอย่างยิ่งที่จะคาดการณ์ล่วงหน้าในช่วงการพัฒนา ปัญหาคุณสมบัติ (qualification problem) ตามที่ผู้ใช้ท่านหนึ่งอ้างอิงไว้ เตือนเราว่าเราไม่สามารถระบุโหมดความล้มเหลวที่มีศักยภาพทั้งหมดล่วงหน้าได้ ไม่ว่าเราจะวิเคราะห์อย่างละเอียดถี่ถ้วนเพียงใด
ขีดจำกัดในทางปฏิบัติของวิธีการที่เป็นทางการ
การอภิปรายเปิดเผยความเห็นที่แตกต่างอย่างลึกซึ้งเกี่ยวกับคุณค่าของเครื่องมือการตรวจสอบอย่างเป็นทางการ เช่น TLA+ และ model checkers บางคนแย้งว่าเครื่องมือเหล่านี้สร้างแบบฝึกหัดทางวิชาการที่ขาดจากการเขียนโปรแกรมในโลกแห่งความเป็นจริง เนื่องจากต้องมีการแปลด้วยมือระหว่างโมเดลและโค้ดจริง คนอื่น ๆ โต้แย้งว่า Amazon ได้ใช้วิธีการที่เป็นทางการแบบเบา (lightweight formal methods) ในการผลิตอย่างประสบความสำเร็จมาหลายปีแล้ว ซึ่งอาจป้องกันความล้มเหลวมากมายที่เราไม่เคยเห็น การอภิปรายหลักอยู่ที่ว่าประโยชน์ของการค้นพบบั๊กที่ซับซ้อนมีค่ามากกว่าต้นทุนของการรักษาโมเดลระบบแยกกันหรือไม่
「ปัญหาของ TLA+ คือมันเป็นเครื่องมือที่ไม่เกี่ยวข้องโดยสิ้นเชิงกับการเขียนโปรแกรมจริง และแม้ทุกอย่างจะทำถูกต้อง มันก็ไม่ได้ป้องกันไม่ให้การเปลี่ยนแปลงโค้ดในภายหลังทำลายโมเดล」
เครื่องมือ Formal Verification ที่ถูกกล่าวถึง:
- Spin model checker พร้อมภาษา Promela
- TLA+
- Alloy (alloytools.org)
- Lean, F*, Dafny (เครื่องมือ verification ที่สามารถสร้างโค้ดได้)
 |
|---|
| บล็อกโพสต์ที่ให้ข้อมูลเกี่ยวกับการจำลอง race conditions ที่ทำให้ AWS ล่มผ่านเครื่องมือ model checking |
สมมติฐานตามเวลาและความล้มเหลวที่หลีกเลี่ยงไม่ได้
วิศวกรผู้มีประสบการณ์หลายคนชี้ไปที่ประเด็นที่ลึกยิ่งกว่า: ระบบที่พึ่งพาสมมติฐานตามเวลานั้นถูกกำหนดให้ล้มเหลวในที่สุด ไม่ว่าจะเป็นการสมมติว่ากระบวนการจะเสร็จสิ้นภายในกรอบเวลาที่กำหนด หรือว่าการดำเนินการล้างข้อมูลจะไม่รบกวนการดำเนินการที่กำลังทำงานอยู่ การพึ่งพาตามเวลานี้สร้างระบบที่เปราะบาง ผู้ใช้ท่านหนึ่งระบุว่าพบบั๊กที่เกิดจากช่วงหมดเวลา (timeouts) ที่ไม่จำเป็นซ้ำแล้วซ้ำเล่า และสรุปว่าการมีอยู่ของช่วงหมดเวลานั้น โดยเนื้อแท้แล้ว คือ บั๊ก ไม่ใช่คุณลักษณะ (feature) มุมมองนี้ท้าทายแนวปฏิบัติพื้นฐานทางวิศวกรรมที่หลายคนยอมรับกันมา
รูปแบบความล้มเหลวทั่วไปที่มีการพูดถึง:
- Time-of-Check to Time-of-Use (TOCTOU)
- การพึ่งพา timeout
- กระบวนการทำความสะอาดที่รบกวนการทำงานที่กำลังดำเนินอยู่
- Network partitions ที่ทำให้เกิดความล่าช้าที่ไม่คาดคิด
พลวัตขององค์กรในวิศวกรรมความน่าเชื่อถือ
นอกเหนือจากการอภิปรายทางเทคนิคแล้ว ผู้แสดงความคิดเห็นยังเน้นย้ำถึงปัจจัยด้านมนุษย์และองค์กร วิศวกรที่สร้างระบบที่แข็งแกร่งและไม่เคยล้มเหลยมักได้รับความสนใจน้อยกว่าผู้ที่แก้ไขความล้มเหลวที่โดดเด่นได้อย่างน่าทึ่ง สิ่งนี้สร้างแรงจูงใจที่บิดเบี้ยวซึ่งงานด้านความน่าเชื่อถืออาจถูกมองคุณค่าน้อยเกินไป ดังที่ผู้ใช้ท่านหนึ่งระบุว่า นักดับเพลิงโค้ดได้รับความสนใจทั้งหมด แต่พวกเขาก็เป็นคนที่ราดน้ำมันเบนซินลงบนโครงสร้างมาก่อนหน้านั้น นี่ชี้ให้เห็นว่าการเปลี่ยนแปลงทางวัฒนธรรมอาจมีความสำคัญไม่น้อยไปกว่าการปรับปรุงทางเทคนิคสำหรับการสร้างระบบที่น่าเชื่อถือ
การวิเคราะห์ AWS outage โดยใช้ model checkers เป็นมากกว่าแบบฝึกหัดหลังเกิดปัญหา — มันแสดงให้เห็นว่าวิธีการที่เป็นทางการสามารถช่วยให้วิศวกรใช้เหตุผลเกี่ยวกับระบบที่ซับซ้อนได้อย่างไร แม้จะไม่มีความรู้ภายในระบบอย่างสมบูรณ์ ในขณะที่ชุมชนยังคงถกเถียงถึงคุณค่าในทางปฏิบัติของเครื่องมือเหล่านี้ เหตุการณ์นี้ก็ทำหน้าที่เป็นเครื่องเตือนใจว่าระบบแบบกระจายต้องการการป้องกันหลายชั้น: การออกแบบอย่างระมัดระวัง การทดสอบที่ครอบคลุม การตรวจสอบขณะทำงาน (runtime monitoring) และบางครั้งก็รวมถึงการตรวจสอบอย่างเป็นทางการ (formal verification) ด้วย เมื่อระบบเติบโตซับซ้อนมากขึ้น เครื่องมือที่เราใช้ทำความเข้าใจระบบเหล่านั้นก็ต้องพัฒนาตามไปด้วย
อ้างอิง: Reproducing The AWS Outage Race Condition With A Model Checker
 |
|---|
| การจำลองสถานการณ์ race condition ของ DNS ใน AWS ที่แสดงการโต้ตอบระหว่างกระบวนการต่างๆ ในระบบกระจาย |