A Program Logic for Concurrent Objects under Fair Scheduling

作者：Liang Hongjin^*; Feng Xinyu^*

来源：ACM Sigplan Notices, 2016, 51(1): 385-399.

DOI：10.1145/2837614.2837635

• Theory
• Verification
• Concurrency
• Progress
• Program Logic
• Rely-Guarantee Reasoning
• Refinement

Existing work on verifying concurrent objects is mostly concerned with safety only, e.g., partial correctness or linearizability. Although there has been recent work verifying lock-freedom of non-blocking objects, much less efforts are focused on deadlock-freedom and starvation-freedom, progress properties of blocking objects. These properties are more challenging to verify than lock-freedom because they allow the progress of one thread to depend on the progress of another, assuming fair scheduling.
We propose LiLi, a new rely-guarantee style program logic for verifying linearizability and progress together for concurrent objects under fair scheduling. The rely-guarantee style logic unifies thread modular reasoning about both starvation-freedom and deadlock freedom in one framework. It also establishes progress-aware abstraction for concurrent objects, which can be applied when verifying safety and liveness of client code. We have successfully applied the logic to verify starvation-freedom or deadlock-freedom of representative algorithms such as ticket locks, queue locks, lock-coupling lists, optimistic lists and lazy lists.

• 出版日期2016-1
• 单位中国科学技术大学; 中国科学技术大学苏州研究院