使用TLA+形式化验证Go并发程序

文章预览

Writing is nature's way of letting you know how sloppy your thinking is - Guindon 在2024年6月份举办的 GopherCon Europe Berlin 2024 [1] 上，一个叫Raghav Roy的印度程序员(听口音判断的)分享了 Using Formal Reasoning to Build Concurrent Go Systems [2] ，介绍了如何使用形式化验证工具 TLA+ [3] 来验证Go并发程序的设计正确性。 TLA+是2013年图灵奖获得者、美国计算机科学家和数学家、分布式系统奠基性大神、 Paxos算法 [4] 和 Latex [5] 的缔造者 Leslie B. Lamport [6] 设计的一种针对数字系统(Digital Systems)的高级(high-level)建模语言，TLA+诞生于1999年，一直低调演进至今。 TLA+不仅可以对系统建模，还可以与模型验证工具，比如：TLC model checker，结合使用，对被建模系统的行为进行全面的验证。我们可以将TLA+看成一种专门用于数字系统建模和验证的 DSL语言 [7] 。 注：TLA是Temporal Logic of Actions的首字母缩写， Temp ………………………………