Abstract
On shared memory multiprocessors, synchronization often turns out to be a performance bottleneck and the source of poor fault-tolerance. Lock-free algorithms can do without locking mechanisms, and are therefore desirable. Lock-free algorithms are hard to design correctly, however, even when apparently straightforward. We formalize Herlihy’s methodology [13] for transferring a sequential implementation of any data structure into a lock-free synchronization by means of synchronization primitives Load-linked (LL)/store-conditional (SC). This is done by means of a reduction theorem that enables us to reason about the general lock-free algorithm to be designed on a higher level than the synchronization primitives. The reduction theorem is based on refinement mapping as described by Lamport [10] and has been verified with the higher-order interactive theorem prover PVS. Using the reduction theorem, fewer invariants are required and some invariants are easier to discover and easier to formulate.
The lock-free implementation works quite well for small objects. However, for large objects, the approach is not very attractive as the burden of copying the data can be very heavy. We propose two enhanced lock-free algorithms for large objects in which slower processes don’t need to copy the entire object again if their attempts fail. This results in lower copying overhead than in Herlihy’s proposal.
Chapter PDF
Similar content being viewed by others
keywords & Phrases
References
Bershad, B.: Practical Considerations for Non-Blocking Concurrent Objects. In: Proceedings of the 13th International Conference on Distributed Computing Systems (May 1993)
Jensen, E.H., Hagensen, G.W., Broughton, J.M.: A new approach to exclusive data access in shared memory multiprocessors. Technical Report UCRL-97663, Lawrence Livemore National Laboratory (November 1987)
Clarke, E., Grumberg, O., Long, D.: Model checking and abstraction ACM Transactions on Programming Languages and Systems 16(5) (January 1994)
Barnes, G.: A method for implementing lock-free data structures. In: Proceedings of the 5th ACM symposium on Parallel Algorithms & Architecture (June 1993)
Massalin, H., Pu, C.: A Lock-free Multiprocessor OS Kernel. Technical Report CUCS-005-91, Columbia University (1991)
Gao, H., Groote, J.F., Hesselink, W.H.: Efficient almost wait-free parallel accessible dynamic hashtables. Technical Report CS-Report 03-03, Eindhoven University of Technology, The Netherlands (2003); To appear in the proceedings of IPDPS (2004)
de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.): REX 1989. LNCS, vol. 430. Springer, Heidelberg (1990)
LaMarca, A.: A Performance Evaluation of Lock-free Synchronization Protocols. In: proceedings of the thirteenth symposium on priniciples of distributed computing (1994)
Lamport, L.: The Temporal Logic of Actions. ACM Transactions on Programming Languages and Systems 16(3), 872–923 (1994)
Abadi, M., Lamport, L.: The existence of refinement mappings. Theoretical Computer Science 2(82), 253–284 (1991)
Moir, M.: Practical Implementations of Non-Blocking Synchronization primitives. In: Proceedings of the sixteenth symposium on principles of Distributed computing, Santa Barbara, CA (1997)
Herlihy, M.P.: A methodology for implementing highly concurrent objects. ACM Transactions on Programming Languages and Systems 15, 745–770 (1993)
Herlihy, M., Luchangco, V., Moir, M.: The Repeat Offender Problem: A Mechanism for Supporting Dynamic-Sized, Lock-Free Data Structures. In: Proceedings of the 16th International Symposium on DIStributed Computing (2002)
Luchangco, V., Moir, M., Shavit, N.: Nonblocking k-compare-single-swap. In: Proceedings of the Fifteenth Annual ACM Symposium on Parallel Algorithms, pp. 314-323 (2003)
Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, Heidelberg (1992)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gao, H., Hesselink, W.H. (2004). A Formal Reduction for Lock-Free Parallel Algorithms. In: Alur, R., Peled, D.A. (eds) Computer Aided Verification. CAV 2004. Lecture Notes in Computer Science, vol 3114. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-27813-9_4
Download citation
DOI: https://doi.org/10.1007/978-3-540-27813-9_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22342-9
Online ISBN: 978-3-540-27813-9
eBook Packages: Springer Book Archive