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

项目名称： 基于上下文精化的并发对象活性的描述及验证

项目编号： No.61502442

项目类型： 青年科学基金项目

立项/批准年度： 2016

项目学科： 自动化技术、计算机技术

项目作者： 梁红瑾

作者单位： 中国科学技术大学苏州研究院

项目金额： 19万元

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

中文关键词： 程序验证；并发；活性；精化；程序逻辑

英文摘要： 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.

英文关键词： Program Verification;Concurrency;Liveness;Refinement;Program Logic