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).
To fill this gap, Li Zhao-Hui and Professor Feng Xin-Yu published their research in Frontiers of Computer Science co-published by Higher Education Press and Springer Nature.
They proposed a program logic that can formally verify obstruction-freedom of practical implementations, as well as verify linearizability(a safety property), at the same time. They also proposed 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, they have successfully applied the logic to verifying a practical obstruction-free double-ended queue implementation in the first classic paper that has proposed the definition of obstruction-freedom.
In the research, they found it inevitable to encounter thorny problems if they treated obstruction-freedom as a traditional progress property and verified it by proving “something good will eventually happen”. To solve this issue, inspired by the method of verifying safety properties, they adopted a straightforward approach by proving “some bad thing never happens”. More specifically, by the definition of obstruction-freedom, they found it allows divergences caused by infinite interference but does not allow divergences caused by finite interference. Therefore, they can prove obstruction-freedom by preventing divergences caused by finite interference. To verify that no such divergences exist, they designed a simple approach that requires only the addition of a side-condition (a sequential total-correctness judgment) in the standard while rule.
For the future direction, they would like to automate the verification of obstruction-freedom. Because they have proposed informal principles to extend an existing logic verifying linearizability to the verification of obstruction-freedom, they plan to extend an automating tool verifying linearizability to that of obstruction-freedom.
DOI: 10.1007/s11704-023-2774-9