【作者】 梁红瑾；

【导师】 冯新宇； 邵中；

【作者基本信息】 中国科学技术大学 ， 计算机软件与理论， 2014， 博士

【摘要】 许多程序验证问题都可以被归结为精化验证,即证明一个较具体的程序不会比一个较抽象的程序产生更多的行为。本文发掘了在并发环境下精化验证的应用场景,并提出若干种可以支持这些精化应用实例的验证技术。具体来说,本文在理解和验证并发程序精化方面做出了如下贡献。首先,本文提出了一种基于依赖/保证的模拟关系RGSim,作为并发程序精化的通用验证手段。这一新颖的模拟关系将线程和并发环境之间的交互作为参数,从而获得可组合性,支持模块化验证。同时,它将精化应用中对并发环境的特定前提参数化,因而具有较好的灵活性和实用性。我们应用RGSim验证了并发环境下的几种程序优化。此外,我们还将并发垃圾收集器的验证归结为精化验证,并提出一种基于RGSim的通用验证框架。使用这一框架,我们验证了Boehm等人提出的并发的标记-清扫垃圾收集算法。其次,本文提出了一种霍尔风格的程序逻辑,用于高效地、模块化地验证并发对象的线性一致性。这是并发程序精化验证的一种重要应用。作为该程序逻辑的一部分,我们提出了一种轻量的辅助代码插桩机制。我们的程序逻辑支持可线性化点不固定的并发算法,这些算法的验证难度很大。具体包括：使用帮助机制的无锁算法(如HSY栈),可线性化点依赖未来不确定执行的算法(如懒惰集合算法),以及同时有这两种特性的算法(如RDCSS算法)。我们还扩展了模拟关系RGSim以支持可线性化点不固定的程序,新的模拟关系保证了我们的程序逻辑的可靠性,它可以蕴涵一种上下文精化关系,该精化关系与线性一致性等价。我们应用这一程序逻辑验证了12个著名的并发算法,其中两个算法已经在Java并发包java.util.concurrent中使用。最后,本文展示了一个用精化关系刻画并发对象完整正确性(包括线性一致性以及各种进展性性质)的统一框架。我们证明了对于满足线性一致性的并发对象,每种进展性性质等价于一种特定的对终止性敏感的上下文精化关系。我们用上下文精化关系统一了并发对象的线性一致性和所有常见的进展性性质,包括无等待性、无锁性、无阻碍性、无饥饿性和无死锁性。根据这一结果,对于任何使用并发对象操作的客户端程序,我们可以模块化地验证该客户端程序的安全性和终止性。另一方面,它也告诉我们,有希望借鉴已有的验证上下文精化的技术来同时验证线性一致性和进展性性质。更多还原

【Abstract】 Many verification problems can be reduced to refinement verification, i.e., proving that a concrete program has no more behaviors than a more abstract program. This dis-sertation explores the applications of refinement verification of concurrent programs, and proposes compositional verification techniques that support these applications. It makes several contributions to understanding and verifying concurrent program refine-ment.First, it shows a Rely-Guarantee-based Simulation (RGSim) as a general proof technique for concurrent program refinement. The novel simulation relation is param-eterized with the interference between threads and their parallel environments. It is compositional and supports modular verification. RGSim can incorporate the assump-tions about environments made by specific refinement applications, thus is flexible and practical. We apply RGSim to reason about optimizations in parallel contexts. We also reduce the verification of concurrent garbage collectors (GCs) to refinement verifica-tion, and propose a general GC verification framework based on RGSim. Using the framework, we verify the Boehm et al. concurrent mark-sweep GC algorithm.Second, it shows a Hoare-style program logic for modular and effective verifica-tion of linearizability of concurrent objects, which is an important application of con-current program refinement verification. Our logic with a lightweight instrumentation mechanism supports objects with non-fixed linearization points (LPs), including the most challenging ones that use the helping mechanism to achieve lock-freedom (as in HSY elimination-based stack), or have LPs depending on unpredictable future execu-tions (as in the lazy set algorithm), or involve both features (as in the RDCSS algo-rithm). We generalize RGSim with the support for non-fixed LPs as the meta-theory of our logic, and show it implies a contextual refinement which is equivalent to lineariz-ability. Using our logic we successfully verify12well-known algorithms, two of which are in the java. util. concurrent package.Finally, it shows a unified framework that characterizes the full correctness (i.e., linearizability and progress properties) of concurrent objects via contextual refinements. We prove that for linearizable objects, each progress property is equivalent to a certain form of termination-sensitive contextual refinement. The framework unifies lineariz-ability and all the five most common progress properties:wait-freedom, lock-freedom, obstruction-freedom, starvation-freedom, and deadlock-freedom. It enables modular verification of safety and liveness properties of client programs, and also makes it pos-sible to borrow ideas from existing proof methods for contextual refinements to verify linearizability and a progress property together.更多还原