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 softwar...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.展开更多
基金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.
