并发数据结构的运行时验证技术

理论计算机科学电子笔记113（2005）163-179www.elsevier.com/locate/entcs并发数据结构塞尔达·塔西兰KoZarcUniversity，Istanbul，Turrkey沙兹·卡迪尔美国微软研究院摘要我们提出了一种运行时技术，用于检查数据结构的并发实现是否符合具有原子操作的高级可执行规范。该技术包括两个阶段。在第一阶段，实现代码被插装，以便将有关其执行的信息记录到日志中。在第二阶段，验证线程与实现并发运行，并使用记录的信息来检查执行是否符合高级规范。我们特别注意减少运行时分析对并发特性和实现性能的影响。我们目前正在将我们的技术应用于Boxwood [1]，这是B-link树数据结构的分布式实现保留字：验证、并发数据结构、精化、原子性1介绍对于可以由并发应用程序线程访问的数据结构实现，验证高级可执行规范的细化比单独的属性验证更彻底。在这项工作中，我们提出了一种在运行时检查细化的技术使用静态技术证明精化需要对实现的整个状态空间进行推理对于大多数重要的系统来说，遍历每个实现状态都是不可行或不可能的。要将定理证明技术应用于精化证明，必须设计并证明关于程序状态的表示不变量。这是一个令人沮丧的和COM-1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.01.028164S. Tasiran，S.Qadeer/Electronic Notes in Theoretical Computer Science 113（2005）163昂贵的任务。此外，当在开发过程中对实现进行修改时，不变量也可能需要修改和重新证明。因此，对于实际的程序，静态地检查细化是不可行的。组合方法已经被探索用于将精化检查划分为更小的、计算上可管理的子问题。虽然有很好的研究理论的组合推理，模块化证明的细化是难以在实践中进行。当在设计的组件上应用验证工具时，需要设计和验证组件环境的抽象模型这些环境假设和接口规范可能在设计描述中没有明确说明，因此可能需要猜测和验证。此外，随着程序的发展，证明子任务的协调是困难和容易出错的。在运行时检查细化减少了所需的计算和人力资源。由于只检查测试用例执行路径上的状态，而不是整个状态空间，因此计算量大大减少。验证设计的组件所需的人力资源减少，因为组件作为实际程序实现的一部分运行，并且所有执行都是组件环境的自然合法执行。因此，不需要设计或验证环境模型，即，组件的测试存根。这些优势促使我们将运行时细化检查作为一种验证范式进行研究我们使用状态转换系统为并发数据结构的实现和规范提供语义。第2节形式化了状态转移系统和我们的精化概念。我们在第3节中描述的多重集的并发实现上说明了我们的运行时验证技术。第4节和第5节介绍了我们在运行时检查细化的技术。我们将在第6节讨论相关工作，并在第7节总结。2预赛2.1状态转移系统我们专注于并发访问的数据结构的实现写在面向对象的语言。该数据结构提供了许多操作，每个操作都被实现为一个方法。当有必要将这些方法与只能由数据结构内部访问的方法区分开来时，我们将它们称为公共方法。多个应用程序线程可以并发地发出对方法的调用，并且可以交叉执行方法的部分以获得更好的在本文中，域TidS. Tasiran，S.Qadeer/Electronic Notes in Theoretical Computer Science 113（2005）163165×的1一个2表示线程标识符的集合。Tid是两个不相交的集合Tidapp和Tidds的并集。setTid 应用程序包含调用数据结构提供的公共方法的应用程序线程的标识符。集合Tidds包含用于执行数据结构内部任务的实现中的工作线程的标识符。我们使用状态转换系统作为程序的形式语义通常，状态转移系统是元组（V，S，s0，δ）：• V是程序变量的集合。例如，这些变量包括线程之间共享的堆分配数据以及线程本地堆栈，每个线程一个堆栈。• S是状态的集合。每个状态都是为V中的每个变量分配一个值（正确类型）。•s0∈S是初始状态。• δ是从S动作到S的转换函数，其中动作是系统可以执行的动作的集合。如果δ（s，a）=SJ，则转换系统可以在状态s中执行动作a以将状态改变为SJ。我们表示e suchatransitionnbyys−→asJ。状态转移系统的一个例子是有限方程r=s0−→s1−→阿那伊· · ·−→snfor somen≥0suchthatsi−→si+1for all0≤i

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