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

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

RIGHTS & PERMISSIONS

Higher Education Press