基于上下文精化的并发对象活性的描述及验证

Many programming languages provide concurrent objects (or libraries) to help program multithreading systems. Concurrent objects should satisfy safety and various liveness properties, such as lock-freedom, wait-freedom, starvation-freedom and deadlock-freedom. Recent work has used contextual refinement to characterize safety and those liveness properties, but existing theories and verification techniques for contextual refinement all have serious problems. In particular, the contextual refinements for starvation-freedom and deadlock-freedom are difficult to use in layered verification. Also, existing verification techniques for contextual refinement do not support wait-free, starvation-free or deadlock-free objects. Besides, the lack of Hoare-style axiomatic proof theory makes verification of concurrent objects a very challenging job...In this project we would like to develop new specification theories and verification techniques for contextual refinements for liveness properties of concurrent objects. We plan to develop new contextual refinements to characterize starvation-freedom and deadlock-freedom, which support layered verification. We will also propose new Hoare-style program logics as new proof theories to verify wait-free, starvation-free or deadlock-free objects. We will demonstrate the applicability of our work in real-world concurrent object verification.

大多数编程语言提供并发对象（或并发库）来辅助开发多线程程序。并发对象不仅应满足安全性，还应满足各种活性性质，如无锁性、无等待性、无饥饿性和无死锁性等。人们使用上下文精化关系来刻画安全性和活性性质，但是现有的上下文精化理论和验证技术尚有许多缺陷。具体表现为，对应无饥饿性和无死锁性的上下文精化关系难以在层次化验证中使用，无法验证满足无等待性、无饥饿性或无死锁性的并发对象，以及缺少公理化的证明理论等。. 针对上述不足，本课题研究并发对象的各种活性性质的上下文精化规范及验证技术，在支持层次化验证的要求下，设计新的上下文精化关系来刻画无饥饿性和无死锁性，开发霍尔风格的公理化程序逻辑和证明系统来验证满足无等待性、无饥饿性和无死锁性的并发对象，并将在实际并发对象的验证中检验理论的实用性。

大多数编程语言提供并发对象（或并发库）来辅助开发多线程程序。并发对象不仅应满足安全性，还应满足各种活性性质，如无锁性、无等待性、无饥饿性和无死锁性等。人们使用上下文精化关系来刻画安全性和活性性质，但是现有的上下文精化理论和验证技术尚有许多缺陷。具体表现为，对应无饥饿性和无死锁性的上下文精化关系难以在层次化验证中使用，无法验证满足无等待性、无饥饿性或无死锁性的并发对象，缺少公理化的证明理论等。..针对上述不足，本课题研究并发对象的各种活性性质的上下文精化规范及验证技术。在支持层次化验证的要求下，设计公平调度下的上下文精化关系来刻画无饥饿性和无死锁性，并为二者设计不同的抽象操作。开发霍尔风格的公理化程序逻辑LiLi来验证满足无等待性、无饥饿性和无死锁性的并发对象，并将该程序逻辑应用于验证若干经典并发算法，其中首次形式化验证了锁耦合链表算法的无饥饿性，以及乐观链表算法和惰性链表算法的无死锁性。此外，针对带有部分方法（partial methods）的并发对象，首次提出“部分无饥饿性”和“部分无死锁性”这两种新的进展性定义，为它们对应的精化关系给出了新的抽象操作，扩展程序逻辑LiLi以支持对这两种新进展性性质的验证，并验证TAS locks和ticket locks分别满足部分无死锁性和部分无饥饿性。