Back to Search
Start Over
A program logic for obstruction-freedom.
- Source :
- Frontiers of Computer Science; Dec2024, Vol. 18 Issue 6, p1-16, 16p
- Publication Year :
- 2024
-
Abstract
- 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. [ABSTRACT FROM AUTHOR]
Details
- Language :
- English
- ISSN :
- 20952228
- Volume :
- 18
- Issue :
- 6
- Database :
- Complementary Index
- Journal :
- Frontiers of Computer Science
- Publication Type :
- Academic Journal
- Accession number :
- 174517816
- Full Text :
- https://doi.org/10.1007/s11704-023-2774-9