并发数据结构验证：基于I/O自动机的模拟方法

"本文主要探讨了并行数据结构的I/O自动机模拟验证方法，重点关注无锁算法的并发实现和线性化证明。作者通过使用输入/输出自动机（IOA）之间的模拟来验证并发数据结构，这种方法既适用于规范建模，也适用于实现建模。" 在并发编程中，数据结构的并行实现允许多个进程同时操作，其正确性的证明通常涉及到证明所有可能的操作交织都会产生正确的结果。线性化是一种常用的标准，它确保并发操作看起来像是按某种特定顺序（即线性顺序）执行的。然而，尽管线性化被广泛接受，但在实际的机械验证过程中并未得到广泛应用。 本文提出的验证方法基于输入/输出自动机（IOA）的前向和后向模拟。IOA是一种模型，可以用来描述系统的行为，特别是在处理并发和交互时。前向模拟用于证明实现自动机的行为至少与规范自动机的行为一样好，而后向模拟则用于证明实现的行为不比规范的更差。这种方法已被应用于使用比较和交换（CAS）操作的几个无锁数据结构实现的机械验证。 文章详细介绍了线性化的概念，并逐步阐述了如何构建抽象和具体的IOA。首先，从抽象数据类型规范出发构建抽象IOA，然后从数据结构实现的代码创建具体IOA。通过一个并发堆栈的例子，作者展示了如何应用这两种构造方法。在案例研究中，他们验证了一个并发堆栈的实现，这有助于理解并行数据结构的正确性证明过程。 此外，作者还分享了他们在验证其他三个无锁算法时的经验，这些算法的验证需要用到后向模拟。这表明，尽管前向模拟对于许多情况是足够的，但在某些复杂的情况下，后向模拟是必不可少的，因为它能够检测到规范和实现之间的潜在不匹配。 总结来说，这篇文章提供了一种基于IOA模拟的并发数据结构验证技术，特别关注了无锁算法的正确性证明。通过实例和经验分享，它强调了线性化和模拟在并发编程验证中的重要性，并指出这种方法有助于发现和修复潜在的并发错误。