แนวปฏิบัติของ Amazon Web Services ในด้านความถูกต้องของระบบ

 (cacm.acm.org)
2 คะแนน โดย GN⁺ 2025-05-31 | 1 ความคิดเห็น | แชร์ทาง WhatsApp
  • Amazon Web Services(AWS) ให้ความสำคัญกับ ความถูกต้อง ของบริการเป็นค่านิยมหลัก และผสานระเบียบวิธีเชิงรูปนัยหลายรูปแบบเข้ากับกระบวนการพัฒนา
  • ผ่าน เครื่องมือระบุข้อกำหนดเชิงรูปนัย เช่น TLA+ และภาษา P ทำให้ค้นพบบั๊กที่ละเอียดอ่อนได้ตั้งแต่เนิ่น ๆ และยังคงรักษาความน่าเชื่อถือได้แม้ทำการเพิ่มประสิทธิภาพอย่าง大胆
  • AWS ยังใช้งาน ระเบียบวิธีเชิงรูปนัยแบบน้ำหนักเบา อย่างแพร่หลาย เช่น property-based testing, deterministic simulation และ continuous fuzzing
  • ผ่าน เครื่องมือฉีดความล้มเหลว อย่าง Fault Injection Service จึงสามารถทำให้การตรวจสอบความน่าเชื่อถือเป็นอัตโนมัติได้ รวมถึงในสถานการณ์ที่เกิดความขัดข้องจริง
  • แม้ อุปสรรคด้านการเรียนรู้ และความซับซ้อนของเครื่องมือจะยังคงมีอยู่ แต่การแพร่หลายของ AI และเครื่องมืออัตโนมัติน่าจะช่วยผลักดันการใช้งานให้กว้างขึ้น

กลยุทธ์ของ AWS ในการรับประกันความถูกต้องของระบบ

Amazon Web Services(AWS) มีเป้าหมายในการให้บริการที่มี ความน่าเชื่อถือสูง ซึ่งลูกค้าสามารถไว้วางใจได้อย่างเต็มที่
เพื่อสิ่งนี้ AWS มุ่งรักษามาตรฐานด้าน ความปลอดภัย ความคงทน ความสมบูรณ์ และความพร้อมใช้งาน โดยวางแนวคิดเรื่อง ความถูกต้องของระบบ ไว้เป็นแกนกลาง

นับตั้งแต่กรณีศึกษาการประยุกต์ใช้ระเบียบวิธีเชิงรูปนัยของ AWS ที่ได้รับการแนะนำใน Communications of the ACM เมื่อปี 2015 แนวทางนี้ก็มีบทบาทสำคัญต่อการดำเนินงานที่ประสบความสำเร็จของบริการหลักต่าง ๆ

แกนสำคัญคือ TLA+ ซึ่งเป็น ภาษาระบุข้อกำหนดเชิงรูปนัย ที่พัฒนาโดย Leslie Lamport
ประสบการณ์ของ AWS ในการนำ TLA+ มาใช้ ช่วยให้สามารถระบุบั๊กเล็กละเอียดที่การทดสอบแบบเดิมตรวจจับไม่ได้ในช่วงต้นของการพัฒนา
นอกจากนี้ แม้จะดำเนินการ เพิ่มประสิทธิภาพ อย่างจริงจัง ก็ยังสามารถรับประกันเสถียรภาพและความน่าเชื่อถือได้ผ่านการตรวจสอบเชิงรูปนัย

เมื่อ 15 ปีก่อน AWS ยังอยู่ในระดับพื้นฐาน เช่น unit test ตอน build และ integration test แบบจำกัด แต่หลังจากนั้นก็ได้ครอบคลุมทั้งแนวทางเชิงรูปนัยและกึ่งรูปนัยอย่างกว้างขวาง
การเปลี่ยนแปลงนี้ช่วยไม่เพียงเรื่องความถูกต้องเท่านั้น แต่ยังช่วยในการตรวจสอบการเพิ่มประสิทธิภาพทั้งระดับสูงและต่ำ เพิ่มความเร็วในการพัฒนา และลดต้นทุน

ที่ AWS ไม่ได้จำกัดอยู่แค่ formal proof และ model checking แบบเดิมเท่านั้น แต่ยังนับรวม property-based testing, fuzzing, runtime monitoring ไว้ในขอบเขตของระเบียบวิธีเชิงรูปนัยด้วย

การปรากฏขึ้นของภาษาโปรแกรม P

ในระยะแรก TLA+ มีข้อดีคือเป็นคำอธิบายเชิงนามธรรมที่ทรงพลัง แต่สำหรับนักพัฒนาจำนวนมาก อุปสรรคในการเริ่มต้นจากการใช้สัญลักษณ์ทางคณิตศาสตร์ยังสูง
ดังนั้น AWS จึงนำ ภาษา P มาใช้ เพื่อมอบแนวทางที่อิง state machine ซึ่งนักพัฒนาคุ้นเคยมากกว่า

ภาษา P ให้แนวทางการสร้างแบบจำลอง state machine สำหรับการออกแบบและวิเคราะห์ระบบกระจาย
เป็นแนวคิดที่คุ้นเคยสำหรับนักพัฒนา Amazon ที่ทำงานกับสถาปัตยกรรม SOA แบบไมโครเซอร์วิส
ตั้งแต่ปี 2019 เป็นต้นมา มีการพัฒนาและดูแลใน AWS ในฐานะโครงการโอเพนซอร์สเชิงกลยุทธ์
ทีมบริการหลักอย่าง Amazon S3, EBS, DynamoDB, Aurora, EC2, IoT ใช้ P เพื่อตรวจสอบความถูกต้องของการออกแบบระบบ

ในช่วงที่ S3 เปลี่ยนไปใช้ read-after-write consistency แบบเข้มแข็ง มีการสร้างแบบจำลองและตรวจสอบโปรโตคอลด้วย P ทำให้สามารถกำจัดบั๊กได้ตั้งแต่ระยะต้นของการออกแบบ และนำการปรับแต่งต่าง ๆ ไปใช้ได้อย่างมั่นใจ

ในปี 2023 ทีม AWS P ได้พัฒนาเครื่องมือ PObserve เพื่อให้สามารถตรวจสอบความถูกต้องของระบบกระจายได้ทั้งในสภาพแวดล้อมการทดสอบและการใช้งานจริง
PObserve สามารถดึง execution log ออกมา และตรวจสอบย้อนหลังได้ว่าการทำงานเป็นไปตามข้อกำหนดหรือไม่ อีกทั้งยังช่วยเชื่อมโยงข้อกำหนดในขั้นออกแบบกับโค้ดที่นำไปใช้งานจริงได้อย่างมีประสิทธิภาพ

การขยายการใช้ระเบียบวิธีเชิงรูปนัยแบบน้ำหนักเบา

Property-based testing

เทคนิคเชิงรูปนัยแบบน้ำหนักเบาที่เป็นตัวแทนมากที่สุดคือ property-based testing
ตัวอย่างเช่น ทีมพัฒนา ShardStore ของ S3 ใช้ property-based testing, code coverage-based fuzzing, fault injection และ counterexample minimization ร่วมกันตลอดทั้งวงจรการพัฒนา
แนวทางนี้เชื่อมโยงกับข้อกำหนดด้านความถูกต้องที่นักพัฒนาเขียนขึ้นโดยตรง และยังช่วยเพิ่มประสิทธิภาพในการดีบักปัญหาอย่างมาก

Deterministic simulation

การทดสอบแบบ deterministic simulation จะรันระบบกระจายในตัวจำลองแบบเธรดเดียว ทำให้สามารถควบคุมองค์ประกอบสุ่มทั้งหมดได้ เช่น scheduling, timing และลำดับของข้อความ
จึงนำไปใช้ได้หลากหลาย ทั้งการทดสอบสถานการณ์ความผิดพลาดและความสำเร็จเฉพาะ การจัดลำดับที่ก่อให้เกิดบั๊ก และการขยาย fuzzing
ด้วยเหตุนี้ การตรวจสอบพฤติกรรมอย่างความหน่วงและความล้มเหลวของระบบจึงทำได้ตั้งแต่ขั้น build และขอบเขตการทดสอบก็ขยายกว้างขึ้น
AWS เปิดเผยโค้ดทดสอบช่วง build time ลักษณะนี้ในโครงการโอเพนซอร์ส shuttle และ turmoil

Continuous fuzzing

continuous fuzzing โดยเฉพาะการสร้างอินพุตจำนวนมากบนพื้นฐานของ code coverage มีประสิทธิภาพต่อการตรวจสอบความถูกต้องของระบบในขั้น integration test
ตัวอย่างเช่น ในการพัฒนา Aurora Limitless Database มีการทำ fuzzing กับ SQL query และ transaction เพื่อยืนยันความถูกต้องของตรรกะการแบ่งพาร์ทิชัน โดยสร้าง schema, dataset และ query แบบสุ่มจำนวนมาก
ผลลัพธ์จะถูกเปรียบเทียบกับพฤติกรรมของเอนจินแบบ non-sharded หรือแนวทางอย่าง SQLancer
การผสาน fuzzing กับ fault injection ช่วยตรวจสอบคุณสมบัติหลักของฐานข้อมูล เช่น atomicity, consistency, isolation
transaction ที่สร้างอัตโนมัติและคุณสมบัติบางอย่าง เช่น isolation จะถูกรับประกันผ่านการตรวจสอบย้อนหลังจาก execution history

การฉีดความขัดข้องผ่าน Fault Injection Service

ในปี 2021 AWS เปิดตัว Fault Injection Service(FIS) เพื่อให้ลูกค้าสามารถทดลองสถานการณ์ข้อบกพร่องได้อย่างรวดเร็ว ทั้งในสภาพแวดล้อมจริงหรือสภาพแวดล้อมทดสอบ เช่น API error, การหยุดชะงักของ I/O และความขัดข้องของอินสแตนซ์
แนวทางนี้ช่วยทั้งการตรวจสอบความพร้อมใช้งานของสถาปัตยกรรมและความสามารถในการฟื้นตัวจากความขัดข้อง ลดช่องว่างจากความหนาแน่นของบั๊กที่สูงในกรณี error และค้นพบปัญหาร้ายแรงที่มีแนวโน้มเกิดขึ้นได้ล่วงหน้า

FIS ถูกใช้อย่างกว้างขวางทั้งโดยลูกค้า AWS และภายใน Amazon เอง ตัวอย่างเช่น เฉพาะในกระบวนการเตรียม Prime Day ก็มีการดำเนินการทดลองถึง 733 ครั้ง

การฉีดข้อผิดพลาดจะยิ่งมีประสิทธิภาพมากขึ้นเมื่อใช้ร่วมกับข้อกำหนดเชิงรูปนัย
เมื่อเขียนพฤติกรรมที่คาดหวังเป็นข้อกำหนดเชิงรูปนัยแล้วนำผลจากการก่อให้เกิดข้อบกพร่องจริงมาเทียบกัน ก็สามารถจับข้อผิดพลาดได้มากกว่าการตรวจสอบเพียง log หรือ metric แบบเดิม

เมตาสเถียรภาพและพฤติกรรมเกิดใหม่ของระบบ

ในระบบกระจาย มีกรณีเพิ่มขึ้นที่ระบบตกอยู่ในสถานะผิดปกติแบบ “ไม่สามารถกู้คืนได้ด้วยตัวเอง” (metastable) จากปัจจัยอย่างภาระงานที่มากเกินไปหรือแคชหมด
ในสถานะนี้ การลดโหลดลงอย่างเดียวไม่เพียงพอให้ระบบกลับมาทำงานปกติ และโดยทั่วไปก็รับมือยากกว่ากรณีข้อผิดพลาดทั่วไป
ตรรกะ retry-timeout ส่วนใหญ่ก็เป็นสาเหตุหนึ่งของปรากฏการณ์นี้เช่นกัน

ข้อกำหนดเชิงรูปนัยแบบเดิมมักเน้นที่ safety และ liveness แต่ metastability จำเป็นต้องพิจารณาพฤติกรรมเกิดใหม่หลากหลายรูปแบบที่นอกเหนือจากนั้น
AWS อาศัยแบบจำลองข้อกำหนดอย่าง TLA+ และ P เพื่อทำ discrete event simulation และวิเคราะห์อย่างเป็นระบบแม้กระทั่งคุณลักษณะเชิงความน่าจะเป็น เช่น ความเป็นไปได้ในการบรรลุ SLA ด้านประสิทธิภาพ และการกระจายของความหน่วง

ความจำเป็นของ formal proof

ในบางกรณีของ ขอบเขตความปลอดภัย (สิทธิ์, virtualization เป็นต้น) จำเป็นต้องมีหลักฐานพิสูจน์ในระดับคณิตศาสตร์ ไม่ใช่เพียงการทดสอบ

ตัวอย่างเช่น ภาษา policy สำหรับสิทธิ์ Cedar ที่ AWS นำมาใช้ในปี 2023 ได้รับการปรับให้เหมาะกับการพิสูจน์อัตโนมัติและการตรวจสอบเชิงรูปนัยบนพื้นฐานของ Dafny อีกทั้งยังเปิดให้ผู้ใช้ทั้งหมดสามารถตรวจสอบได้ด้วยตนเองผ่านโค้ดสาธารณะและกระบวนการแก้ไขที่ชัดเจน
รวมถึง key property ของขอบเขตความปลอดภัยใน Firecracker VMM ก็มีการดำเนินการพิสูจน์ด้วย เครื่องมือวิเคราะห์โค้ด Rust อย่าง Kani

ในลักษณะนี้ AWS ใช้ formal model และ specification อย่างกว้างขวางในหลายช่วงเวลา ทั้งการออกแบบ การนำไปใช้ การปฏิบัติงาน และการพิสูจน์ เพื่อรับประกันความถูกต้องของซอฟต์แวร์และขยายคุณค่าให้ทั้งองค์กรและลูกค้า

ผลลัพธ์เพิ่มเติมที่เกินกว่าความถูกต้อง

ระเบียบวิธีเชิงรูปนัยมีบทบาทสำคัญอย่างมากทั้งต่อ ความน่าเชื่อถือและการปรับปรุงประสิทธิภาพ
ตัวอย่างเช่น มีการตรวจสอบ commit protocol ของ Aurora ด้วย P และ TLA+ เพื่อลด network roundtrip ขณะเดียวกันก็ยังคงรับประกันความปลอดภัย
ในการเพิ่มประสิทธิภาพอัลกอริทึมเข้ารหัส RSA สำหรับ ARM Graviton 2 ก็มีการพิสูจน์ความถูกต้องทางคณิตศาสตร์ของการแปลงใน HOL Light จนได้ผลลัพธ์เชิงปฏิบัติจริงคือ ประสิทธิภาพดีขึ้นและต้นทุนโครงสร้างพื้นฐานลดลงพร้อมกัน

ความท้าทายและโอกาสในอนาคต

ตลอด 15 ปีที่ผ่านมา AWS ได้ขยายการประยุกต์ใช้ระเบียบวิธีเชิงรูปนัย/กึ่งรูปนัยในภาคอุตสาหกรรมอย่างมาก แต่ก็ยังมีปัญหาเรื่อง อุปสรรคในการนำมาใช้ อยู่จริง ทั้งเส้นโค้งการเรียนรู้ ความจำเป็นต้องใช้ผู้เชี่ยวชาญ และลักษณะเชิงวิชาการของเครื่องมือ
แม้แต่ property-based testing และ deterministic simulation ก็ยังเป็นเรื่องไม่คุ้นเคยสำหรับนักพัฒนาจำนวนมาก
อุปสรรคด้านการศึกษามีอยู่ตั้งแต่ระดับปริญญาตรี ทำให้การเผยแพร่เครื่องมือและระเบียบวิธี รวมถึงการนำไปใช้จริงในงาน ยังดำเนินไปอย่างช้า ๆ
คุณลักษณะเกิดใหม่ของระบบขนาดใหญ่ เช่น metastability ก็ยังอยู่ในระยะเริ่มต้นของการวิจัย

ในอนาคตคาดว่า AI/โมเดลภาษาขนาดใหญ่ จะช่วยสนับสนุนการเขียน formal model และ specification ทำให้ผู้ปฏิบัติงานเข้าถึงได้ง่ายขึ้นอย่างก้าวกระโดดในระยะเวลาไม่นาน

บทสรุป

การสร้างซอฟต์แวร์ที่แข็งแกร่งและปลอดภัยจำเป็นต้องมีวิธีการหลากหลายในการรับประกันความถูกต้องของระบบ
AWS ได้นำมาใช้แบบครอบคลุม ไม่เพียงเทคนิคการทดสอบมาตรฐาน แต่ยังรวมถึง model checking, fuzzing, property-based testing, การทดสอบฉีดความขัดข้อง, deterministic/event-based simulation และการตรวจสอบ execution history
ข้อกำหนดและระเบียบวิธีเชิงรูปนัยทำหน้าที่เป็น test oracle ที่สำคัญในกระบวนการพัฒนาของ AWS และได้กลายเป็นหนึ่งในด้านที่ควรลงทุนแล้ว จากการพิสูจน์ผลเชิงปฏิบัติและเชิงเศรษฐกิจเรียบร้อย

บทความที่เกี่ยวข้อง

1 ความคิดเห็น

 
GN⁺ 2025-05-31
ความเห็นบน Hacker News

  • อยากพูดถึงแนวทางการทดสอบแบบ deterministic simulation ที่ AWS ใช้รันระบบแบบกระจายอยู่บนซิมูเลเตอร์เธรดเดียว พร้อมควบคุมปัจจัยที่ไม่เป็น deterministic ทั้งหมด เช่น การจัดตารางเธรด จังหวะเวลา และลำดับการส่งข้อความ จากนั้นก็เขียนเทสต์ให้ตรงกับสถานการณ์ความล้มเหลวหรือความสำเร็จเฉพาะทาง โดยให้เฟรมเวิร์กทดสอบเป็นผู้ควบคุมความไม่เป็น deterministic ในระบบ นักพัฒนาสามารถระบุลำดับเฉพาะที่เคยทำให้เกิดบั๊กได้ ตัว scheduler ยังขยายไปสู่การ fuzz ลำดับ หรือแม้แต่สำรวจทุกลำดับที่เป็นไปได้ก็ได้ เลยสงสัยว่ามีไลบรารีโอเพนซอร์สที่ทำแบบนี้โดยไม่ผูกกับภาษาไหม แนวคิดคืออยากได้เครื่องมือมิดเดิลแวร์ที่ทำให้เรื่องอย่าง networking, storage ภายในคอนเทนเนอร์กลายเป็น "deterministic" ได้ในตอนทดสอบ antithesis แทบจะทำหน้าที่นี้อยู่แล้ว แต่ยังไม่เคยเห็นในโลกโอเพนซอร์ส ถึงจะพอแก้ได้ระดับหนึ่งด้วยการ stub I/O ถ้าเขียนเทสต์ดีพอ แต่ก็ไม่มีอะไรการันตีว่าทุกคนจะเขียนเทสต์ดี เลยมองว่าถ้ามี deterministic ในชั้นที่สูงกว่าแอปพลิเคชันก็น่าจะดี อีกด้านหนึ่งก็หวังว่า AI จะได้ฉายแสงกับงานทดสอบจริง ๆ แกนสามด้านคือ prompt (ข้อกำหนด)-การเขียนเทสต์-AI-โค้ดที่รันจริง น่าจะประกบกันได้อย่างเหมาะสม และหวังว่า AI จะทำให้ formal verification เข้าถึงง่ายขึ้น จนโลกซอฟต์แวร์มีความเข้มงวดมากขึ้นอีกขั้น

    • การทำให้เทคนิค deterministic simulation testing (DST) แพร่หลายมีอุปสรรคอยู่สองข้อ หนึ่งคือที่ผ่านมา ระบบทั้งหมดต้องไปรันอยู่บน simulation framework เฉพาะโดยตรงและแทบไม่มี dependency อื่น สองคือถ้าการสร้างและการสำรวจ input อ่อน เทสต์จะดูเหมือนผ่านหมดทั้งที่ไม่ได้ตรวจสอบอะไรจริงจัง antithesis พยายามแก้ทั้งสองปัญหานี้ แต่ก็ยังยากอยู่มาก ยังไม่ค่อยมีที่ไหนที่มีวิธีชัดเจนในการเอา determinism ไปใช้กับซอฟต์แวร์อะไรก็ได้ โครงการ Hermit ของ Facebook ก็เคยพยายามทำ deterministic Linux userspace แต่สุดท้ายก็ยุติไป คอมพิวเตอร์แบบ deterministic เป็นรากฐานทางเทคนิคที่มีประโยชน์มากนอกเหนือจากงานทดสอบ และคิดว่าสักวันคงมีใครเปิดโอเพนซอร์สมันออกมา

    • คิดว่าการเอา QEMU มารันในโหมด emulation 100% แบบ single-thread เพื่อให้ได้เครื่องที่ deterministic นั้นค่อนข้างทำได้ไม่ยากนัก แต่สิ่งที่อยากได้จริง ๆ คือการรันแบบ deterministic ที่ "ควบคุมได้" ซึ่งยากกว่ามาก ถ้าจะทำให้หลายโปรเซสทำงานตามสถานการณ์ที่กำหนด โดยเฉพาะในระดับ CPU และ OS scheduler จะยากมาก การสร้างสภาพแวดล้อมที่ไม่ผูกกับภาษาใดภาษาหนึ่งก็ยาก และยังโดนรายละเอียดจุกจิกรบกวนได้ง่าย ผมเองก็เคยทำระบบง่าย ๆ ที่บังคับ JVM threads หลายตัวให้เดินแบบ lockstep ณ จุดพฤติกรรมบางช่วง โดยจัดการ I/O และเวลาของระบบผ่านการ stub และการควบคุม ทำให้ทดสอบปฏิสัมพันธ์หลายรูปแบบระหว่างคอมโพเนนต์แบบ asynchronous, ความล้มเหลวของ I/O, การ retry ฯลฯ ได้ และจับบั๊กชวนปวดหัวก่อนขึ้น production ได้ แต่ที่ทำได้นั้นเป็นเพียงการทำให้บางจุด synchronization เรียบง่ายลง ไม่ใช่การควบคุมทั้งระบบ และ data race ทั่วไปที่เกิดจากการ sync พลาดก็มักจับด้วยวิธีนี้ได้ยาก

    • ขอแชร์ เอกสารทางการเรื่องวิธีทดสอบของ FoundationDB และ วิดีโอบรรยายบน YouTube

    • ถ้าเป็นภาษาที่ดีบักด้วย gdb ได้ แนะนำโปรเจกต์ https://rr-project.org/

    • จำได้ว่าเคยดูการบรรยายของ Joe Armstrong เรื่องการใช้ property testing เพื่อทดสอบ Dropbox

  • ผมคิดว่า S3 เป็นหนึ่งในซอฟต์แวร์ที่เจ๋งที่สุดเท่าที่เคยเห็น และการที่เมื่อหลายปีก่อน S3 เพิ่ม strong read-after-write consistency ให้ทั้งระบบได้ ก็เป็นสุดยอดของ software engineering จริง ๆ ลิงก์บล็อกโพสต์

    • ผมเคยทำงานกับส่วน lifecycle ของ S3 โดยตรง ช่วงนั้นพอดีกับตอนที่ทีม index กำลังออกแบบสถาปัตยกรรมใหม่เพื่อให้ได้ consistency นี้ ต่อให้มองจากภายนอก S3 จะน่าทึ่งอยู่แล้ว แต่ภายในนั้นทั้งตัว implementation และโครงสร้างองค์กรก็น่าประทับใจเกินคาดมาก

    • จริง ๆ แล้ว Google Cloud Storage มีฟีเจอร์นี้ (strong consistency) มาก่อน S3 นานพอสมควร โดยรวมแล้วให้ความรู้สึกว่า GCS เป็นผลิตภัณฑ์ที่เป็นระบบกว่าและทำมาดีกว่าเล็กน้อย

  • เห็นด้วยกับตัวเลข 92% (ความขัดข้องของคลัสเตอร์ส่วนใหญ่เริ่มจากความล้มเหลวเล็กน้อย) ปัญหาส่วนมากไม่ใช่อุบัติเหตุใหญ่โตหวือหวา แต่เป็นการ retry เรื่อง "เล็กน้อย" ที่ค่อย ๆ สะสม state ไปเรื่อย ๆ จนสุดท้ายระเบิดเป็นเหตุขัดข้องใหญ่ตอนตีสอง การทุ่มเวลาเชิงวิศวกรรมให้กับความล้มเหลวที่มองไม่เห็นชัดจึงสำคัญมาก

    • นี่อาจเป็นผลของ "survivorship bias" คือปัญหาใหญ่ ๆ ถูกแก้จนไม่เกิดซ้ำแล้ว เลยเหลือแต่ปัญหาเล็กที่ดูไม่อันตรายซึ่งบางครั้งกลับก่อเหตุขัดข้องใหญ่ได้

  • คิดว่าเป็นบทความที่น่าสนใจมาก การใช้ state machine ในการสร้าง infrastructure control plane เป็นสิ่งจำเป็น ผมไม่แน่ใจว่าจำเป็นต้องใช้ P ไหม พวกเราก็สร้าง infrastructure control plane ด้วย Ruby มานานกว่า 13 ปีแล้ว และมันทำงานได้ยอดเยี่ยม บล็อกแชร์ประสบการณ์ที่เกี่ยวข้อง

  • มีเรื่องสงสัยเกี่ยวกับภาษา P ก่อนหน้านี้เหมือน Microsoft เคยใช้ P สร้างโค้ด C สำหรับ runtime ของ Windows USB stack และใช้งานจริง แต่ตอนนี้ดูเหมือนจะไม่ได้ใช้มันสร้างโค้ดสำหรับ production แล้ว ผมเคยถามไว้ใน Hacker News เหมือนกัน ลิงก์คำถาม ถ้าโค้ดที่ generate มาเอาเข้า kernel ได้ ก็น่าจะใช้ได้แน่ในสภาพแวดล้อมคลาวด์ที่เงื่อนไขผ่อนคลายกว่านั้นมาก

    • Coyote ที่ใช้ใน Azure ดูเหมือนเป็นวิวัฒนาการของ P# และ P# ก็เหมือนจะวิวัฒนาการมาจาก P อีกที ลิงก์บทความ poolmanager-coyote

  • ในมุมของคนที่ไม่ได้มาจาก AWS และไม่คุ้นกับ TLA+ หรือ P ผมว่าถ้ามีตัวอย่างระดับ "hello world" สักหน่อยก็น่าจะเข้าใจง่ายขึ้น อย่างน้อยจากบทความอย่างเดียวมันให้ความรู้สึกเหมือนเป็นกระบวนการที่ทรมาน และอดคิดไม่ได้ว่าปัญหาแบบนี้น่าจะจัดการได้ด้วยการออกแบบกับการทดสอบที่ดีพออยู่แล้ว ถ้ามีตัวอย่างง่าย ๆ ก็น่าจะช่วยให้ตัดสินได้มากขึ้นว่ามันทำอะไรจริง ๆ

    • มีตัวอย่างเดโม TLA+ แบบเร็ว ๆ ที่ผมชอบมาก ลิงก์ gist มันเป็นโมเดลที่หลายเธรดเพิ่มค่าตัวนับร่วมกันแบบไม่เป็น atomic และเมื่อตรวจสอบ property ก็จะเจอ race condition บั๊กแบบนี้ในทางปฏิบัติค้นเจอด้วยการทดสอบอย่างเดียวได้ยากมาก แน่นอนว่า spec ของ TLA+ ส่วนใหญ่ซับซ้อนกว่านี้มาก แต่ตัวอย่างนี้ดีสำหรับการจับข้อผิดพลาดพื้นฐาน

    • ผมเคยลองใช้ TLA เอง และรู้สึกผิดหวังที่เครื่องมือแบบกราฟิกไม่ค่อยสอดคล้องกับ tutorial เท่าไร ทั้งที่ตัว TLA เองผมอยากใช้มาก และชอบงานของ Lamport มานานแล้ว ตั้งแต่ LaTeX ไปจนถึงงานวิจัย

    • สมมติฐานของการใช้ formal methods ก็คือ แค่การทดสอบอย่างเดียวไม่มีทางจับทุกปัญหาได้ทั้งหมดอยู่แล้ว

    • ขอแนะนำ รีโพซิทอรี GitHub ของ TLA+ Examples ควรเริ่มจากอะไรเรียบง่ายอย่างปัญหา DieHard

    • การทดสอบพิสูจน์ความถูกต้องของ implementation ต่ออินสแตนซ์เฉพาะของปัญหา แต่ formal verification พิสูจน์กับทั้งคลาสของปัญหา ตัวอย่างเช่น ฟังก์ชันที่คืนค่า anagram การทดสอบจะตรวจได้แค่บางคู่คำ แต่ถ้าจะพิสูจน์ว่าถูกต้องสำหรับทุกคู่คำ ก็ต้องใช้ formal verification และกรณีอย่าง undefined behavior หรือบั๊กในไลบรารีจำนวนมากก็มักถูกเจอได้ก็ในกระบวนการ formal verification เท่านั้น

  • พอเห็นการกล่าวถึง "เทคนิคกึ่งฟอร์มอลแบบเบา เช่น property-based testing, fuzzing, runtime monitoring" ก็รู้สึกว่าการนับ property-based testing กับ fuzzing เป็นส่วนย่อยของ formal methods นั้นพอได้ แต่การนับ runtime monitoring เข้าไปเป็นเทคนิคกึ่งฟอร์มอลด้วยอาจจะเกินไปหน่อย

    • ถ้าเป็น runtime monitoring ที่ใช้เครื่องมืออย่าง PObserve ก็ถือเป็นเทคนิคกึ่งฟอร์มอลได้พอสมควร เพียงแต่ควรแยกจากระบบ alarm หรือ metrics ทั่วไป

  • เมื่อก่อนผมเคยมีปฏิสัมพันธ์กับ Leslie Lamport ผ่านงานอย่างบทความเรื่อง Buridan's Principle เป็นต้น วันนี้เพิ่งได้รู้อะไรเกี่ยวกับ TLA+ และ PlusCal เพิ่มจากหน้าเว็บของเขา หน้าตัวอย่าง Peterson การที่เขานำคณิตศาสตร์มาใช้กับการเขียนโปรแกรม เป็นผู้บุกเบิกด้านระบบ concurrent และยังสร้างภาษาออกแบบระบบ (TLA+) ที่ AWS และที่อื่น ๆ ใช้งานอยู่ มันดูเป็นเรื่องที่เป็นธรรมชาติมาก อยากให้คนที่สร้าง distributed systems ใช้สิ่งที่ Lamport สร้างกันมากกว่านี้ ในระบบขนาดใหญ่นั้นการพิสูจน์ความถูกต้องสำคัญมาก

    • การแปลงโค้ดเดิมให้เป็นสเปก TLA+ นั้น Claude Opus (Extended Thinking) ใช้งานได้ดีมาก ผมเคยใช้มันช่วยหาบั๊กได้หลายตัวในโปรเจกต์ Rust และการตรวจสอบคอมโพเนนต์แกนกลางของ C++ โมเดลอื่นมักสะดุดเรื่องไวยากรณ์และตรรกะของสเปก แต่ Opus ทำได้ลื่นไหลกว่ามาก

    • ไม่ใช่แค่ระบบขนาดใหญ่เท่านั้น แม้แต่ยูทิลิตีเล็กแต่สำคัญอย่าง SSH หรือ terminal ซึ่งคนใช้กันทั่วโลก ก็ได้ประโยชน์มากจากการพิสูจน์ความถูกต้องเช่นกัน

    • สำหรับคำว่า "พิสูจน์ความถูกต้องของระบบ" นั้น ในความเป็นจริงพิสูจน์ได้ไม่ทั้งหมด ตัว model checker บอกได้เพียงว่าสเปกที่กำหนดไว้สอดคล้องกับคุณสมบัติภายใน state space ที่จำกัดเท่านั้น

  • ส่วนตัวอยากรู้ว่ามีใครเคยใช้ FIS กับการทดลองใน distributed service จริงไหม กำลังพิจารณาเอามาใช้ แต่ยังไม่มีประสบการณ์ทำการทดลองขนาดใหญ่ด้วยตัวเอง

  • สงสัยว่า Promela กับ SPIN เป็นภาษาระดับสูงกว่าที่บทความพูดถึงหรือเปล่า

    • ในฐานะคนที่เคยใช้ Promela ทำงานกับ distributed systems มา ผมรู้สึกว่ามันไม่ได้เหมาะกับสายงานนี้ตรง ๆ นัก แม้จะมีไอเดียที่น่าสนใจอยู่บ้าง แต่ก็อาจคุ้มที่จะกลับไปดูอีกครั้ง