A program logic for obstruction-freedom

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.

Graphical abstract

Keywords

verification / program logic / progress properties / obstruction-freedom / concurrent objects

Zhao-Hui Li is a PhD candidate in the School of Computer Science and Technology at University of Science and Technology of China, China. He obtained his BS degree in computer science from the University of Science and Technology of China, China in 2014. His research interests are in programming languages and formal methods, with a focus on the verification of concurrent programs

Xin-Yu Feng is a professor in Department of Computer Science at Nanjing University, China. He obtained his PhD degree in computer science from Yale University, USA in 2007, ME and BS degrees in computer science from Nanjing University, China in 2002 and 1999, respectively. His research interests are on theories of programming languages and formal program verification

References

[1] Lamport L . Proving the correctness of multiprocess programs. IEEE Transactions on Software Engineering, 1977, SE-3( 2): 125–143

[2] Herlihy M P, Wing J M . Linearizability: a correctness condition for concurrent objects. ACM Transactions on Programming Languages and Systems, 1990, 12( 3): 463–492

[3] Herlihy M, Shavit N. The Art of Multiprocessor Programming. Amsterdam: Morgan Kaufmann, 2008

[4] Liang H, Feng X. Modular verification of linearizability with non-fixed linearization points. In: Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation. 2013, 459−470

[5] da Rocha Pinto P, Dinsdale-Young T, Gardner P. TaDA: a logic for time and data abstraction. In: Proceedings of the 28th European Conference on Object-Oriented Programming. 2014, 207−231

[6] Jung R, Swasey D, Sieczkowski F, Svendsen K, Turon A, Birkedal L, Dreyer D . Iris: monoids and invariants as an orthogonal basis for concurrent reasoning. ACM SIGPLAN Notices, 2015, 50( 1): 637–650

[7] da Rocha Pinto P, Dinsdale-Young T, Gardner P, Sutherland J. Modular termination verification for non-blocking concurrency. In: Proceedings of the 25th European Symposium on Programming. 2016, 176−201

[8] Liang H, Feng X, Shao Z. Compositional verification of termination-preserving refinement of concurrent programs. In: Proceedings of the Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). 2014, 65

[9] Liang H, Feng X. A program logic for concurrent objects under fair scheduling. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 2016, 385−399

[10] Guerraoui R, Henzinger T A, Jobstmann B, Singh V. Model checking transactional memories. In: Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation. 2008, 372−382

[11] Abdulla P, Dwarkadas S, Rezine A, Shriraman A, Zhu Y. Verifying safety and liveness for the FlexTM hybrid transactional memory. In: Proceedings of 2013 Design, Automation & Test in Europe Conference & Exhibition. 2013, 785−790

[12] Gotsman A, Cook B, Parkinson M, Vafeiadis V. Proving that non-blocking algorithms don’t block. In: Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 2009, 16−28

[13] Herlihy M . Wait-free synchronization. ACM Transactions on Programming Languages and Systems, 1991, 13( 1): 124–149

[14] Fraser K. Practical lock-freedom. No. UCAM-CL-TR-579. University of Cambridge, Computer Laboratory, 2004

[15] Herlihy M, Luchangco V, Moir M. Obstruction-free synchronization: double-ended queues as an example. In: Proceedings of the 23rd International Conference on Distributed Computing Systems. 2003, 522−529

[16] Saha A, Chatterjee A, Pal N, Ghosh A, Chaki N. A lightweight implementation of obstruction-free software transactional memory. In: Chaki R, Saeed K, Choudhury S, Chaki N, eds. Applied Computation and Security Systems. New Delhi: Springer, 2014, 67−84

[17] Ghosh A, Chaki N. Design of a new OFTM algorithm towards abort-free execution. In: Proceedings of the 9th International Conference on Distributed Computing and Internet Technology. 2013, 255−266

[18] Tabba F, Moir M, Goodman J R, Hay A W, Wang C. NZTM: nonblocking zero-indirection transactional memory. In: Proceedings of the 21st Annual Symposium on Parallelism in Algorithms and Architectures. 2009, 204−213

[19] Marathe V J, Scherer III W N, Scott M L. Adaptive software transactional memory. In: Proceedings of the 19th International Symposium on Distributed Computing. 2005, 354−368

[20] Guerraoui R, Ruppert E . Anonymous and fault-tolerant shared-memory computing. Distributed Computing, 2007, 20( 3): 165–177

[21] Bouzid Z, Raynal M, Sutra P . Anonymous obstruction-free (n, k)-set agreement with n-k+1 atomic read/write registers. Distributed Computing, 2018, 31( 2): 99–117

[22] Fraser K, Harris T . Concurrent programming without locks. ACM Transactions on Computer Systems, 2007, 25( 2): 5

[23] Moir M S, Luchangco V M, Herlihy M. Obstruction-free data structures and mechanisms with separable and/or substitutable contention management mechanisms: US09052944B2. 2005–04-15

[24] Fich F E, Luchangco V, Moir M, Shavit N. Obstruction-Free algorithms can be practically wait-free. In: Proceedings of the 19th International Conference on Distributed Computing. 2005, 78−92

[25] Liang H, Hoffmann J, Feng X, Shao Z. Characterizing progress properties of concurrent objects via contextual refinements. In: Proceedings of the 24th International Conference on Concurrency Theory. 2013, 227−241

[26] Liang H, Feng X . Progress of concurrent objects with partial methods. Proceedings of the ACM on Programming Languages, 2017, 2( POPL): 20

[27] Li Z H, Feng X Y . Verifying contextual refinement with ownership transfer. Journal of Computer Science and Technology, 2021, 36( 6): 1342–1366

[28] Hoffmann J, Marmar M, Shao Z. Quantitative reasoning for proving lock-freedom. In: Proceedings of the 28th Annual ACM/IEEE Symposium on Logic in Computer Science. 2013, 124−133

[29] Liang H, Feng X . Progress of concurrent objects. Foundations and Trends^® in Programming Languages, 2020, 5( 4): 282–414

[30] Filipović I, O’Hearn P, Rinetzky N, Yang H. Abstraction for concurrent objects. Theoretical Computer Science, 2010, 411(51−52): 4379−4398

Acknowledgements

This work was supported by the National Natural Science Foundation of China (Grant No. 61632005).

Competing interests

The authors declare that they have no competing interests or financial conflicts to disclose.

Supplementary information

The supplementary information is available online at https://journal.hep.com.cn and https://link.springer.com.

RIGHTS & PERMISSIONS

2024 Higher Education Press