并行数据结构的I/O自动机模拟验证方法

理论计算机科学电子笔记137（2005）93-110www.elsevier.com/locate/entcs并行数据结构的仿真实现罗伯特·科尔文1，2 西蒙·多尔蒂3林赛·格罗夫斯4惠灵顿维多利亚大学数学、统计和计算机科学学院新西兰惠灵顿摘要我们描述了一种基于两个输入/输出自动机（IOA）之间的模拟来验证并发数据结构的方法，对规范和实现进行建模。我们解释了我们如何使用这种方法在机械验证一个简单的无锁堆栈实现使用正向模拟，并简要讨论了我们的经验，验证其他三个无锁算法，都需要使用反向模拟。关键词：并发，无锁算法，线性化，I/O自动机，仿真1介绍数据结构的并发实现被设计为允许多个进程同时对数据结构执行操作。为了证明这种实现的正确性，我们必须证明这些操作的原子步骤的所有可能的交织将产生正确的结果。线性性[11]被广泛接受为并发数据结构的适当正确性标准，但似乎并没有广泛用于机械证明。1我们感谢Sun Microsystems的财务支持，以及Mark Moir对本文的有益评论。2电子邮件：Robert. mcs.vuw.ac.nz3 电子邮件：Simon. mcs.vuw.ac.nz4电子邮件：Lindsay. mcs.vuw.ac.nz1571-0661 © 2005由Elsevier B. V.出版，CC BY-NC-ND许可下开放获取。doi：10.1016/j.entcs.2005.04.02694R. Colvin等人/理论计算机科学电子笔记137（2005）93在本文中，我们提出了一种证明并发数据结构线性化的方法，该方法基于两个输入/输出Au- tomata（IOA）[14]之间的模拟，一个模拟抽象数据类型规范，一个模拟实现。我们已经使用这种方法在机械验证几个无锁的数据结构实现使用比较和交换（CAS）作为他们唯一的同步机制。在第2节中，我们介绍了线性化。在第3节中，我们介绍了IOA并定义了前向和后向模拟。在第4节和第5节中，我们展示了如何从抽象数据结构规范构造抽象IOA，以及如何从数据结构实现的代码构造具体IOA，并通过为并发堆栈构造抽象和具体IOA来说明这两种构造。在第6节中，我们讨论并发堆栈实现的验证。在第7节中，我们简要讨论了我们使用这种方法验证（和纠正/改进）其他三个无锁算法的经验，所有这些算法都需要使用反向模拟。第8章我们得出了结论。2线性度并发系统由一组有限的进程组成，每个进程执行一系列涉及一组有限的共享对象的操作。非正式地说，如果对象上的每个操作都可以理解为在其调用和完成之间的某个时刻瞬间发生，并且其在该时刻的行为与相应的顺序数据类型的规范一致，则共享对象是可线性化的这个想法在[11]中被形式化，通过根据与共享对象上的操作的调用和响应相对应的事件序列对并发系统进行建模我们写X。opp（args）表示进程p调用对象X上的参数args的操作op，和X。respp（res）表示进程p从对象X上的操作返回响应resp和结果res。响应匹配涉及同一进程和同一对象的前一个调用，前提是没有涉及该进程的中间事件。顺序历史是匹配的调用-响应对（表示已完成的操作）的序列，可能以不匹配的调用（表示未完成或挂起的操作）结束。一个对象X的序列指定是一个只涉及对象X的预定闭历史集。一个连续的历史H是合法的，如果每个对象子历史H|X，通过把H限制在涉及X的事件中而得到，属于X的序列规范。一个历史H在使得a

下载后可阅读完整内容，剩余1页未读，立即下载