A program logic for obstruction-freedom  

作　　者：Zhao-Hui LI Xin-Yu FENG 

机构地区：[1]School of Computer Science and Technology,University of Science and Technology of China,Hefei 230026,China [2]Department of Computer Science and Technology,Nanjing University,Nanjing 210023,China [3]State Key Laboratory for Novel Software Technology,Nanjing University,Nanjing 210023,China

出　　处：《Frontiers of Computer Science》2024年第6期85-100,共16页计算机科学前沿（英文版）

基　　金：the National Natural Science Foundation of China(Grant No.61632005)。

摘　　要：Though obstruction-free progress property is weaker than other non-blocking properties including lock-freedom and wait-freedom,it has advantages that have led to the use of obstruction-free implementations for software transactional memory(STM)and in anonymous and fault-tolerant distributed computing.However,existing work can only verify obstruction-freedom of specific data structures(e.g.,STM and list-based algorithms).In this paper,to fill this gap,we propose a program logic that can formally verify obstruction-freedom of practical implementations,as well as verify linearizability,a safety property,at the same time.We also propose informal principles to extend a logic for verifying linearizability to verifying obstruction-freedom.With this approach,the existing proof for linearizability can be reused directly to construct the proof for both linearizability and obstruction-freedom.Finally,we have successfully applied our logic to verifying a practical obstruction-free double-ended queue implementation in the first classic paper that has proposed the definition of obstruction-freedom.

关 键 词：VERIFICATION program logic progress properties obstruction-freedom concurrent objects 

分 类 号：TP311.1[自动化与计算机技术—计算机软件与理论]