research-article

Open access

Proving the Correctness of Nonblocking Data Structures: So you’ve decided to use a nonblocking data structure, and now you need to be certain of its correctness. How can this be achieved?

Author:

Mathieu DesnoyersAuthors Info & Claims

Queue, Volume 11, Issue 5

Pages 30 - 43

https://doi.org/10.1145/2488364.2490873

Published: 15 May 2013 Publication History

All formats PDF

Abstract

Nonblocking synchronization can yield astonishing results in terms of scalability and realtime response, but at the expense of verification state space.

References

[1]

Alglave, J., Maranget, L., Sarkar, S., Sewell, P. 2011. Litmus: running tests against hardware. In Proceedings of the 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems: 41-44; http://dl.acm.org/citation.cfm?id=1987389.1987395.

Digital Library

[2]

ARM. 2010. ARM Architecture Reference Manual; http://infocenter.arm.com/help/index.jsp?topic=/com.arm.doc.set.architecture/index.html.

[3]

Baier, C., Katoen, J. 2008. Principles of Model Checking. Cambridge: MIT Press; http://books.google.ca/books?id=nDQiAQAAIAAJ.

Digital Library

[4]

Bergan, T., Anderson, O., Devietti, J., Ceze, L., Grossman, D. 2010. Coredet: a compiler and runtime system for deterministic multithreaded execution. ACM SIGARCH Computer Architecture News 38(1): 53-64; http://doi.acm.org/10.1145/ 1735970.1736029.

Digital Library

[5]

Bernstein, P., Shipman, D., Wong, W. 1979. Formal aspects of serializability in database concurrency control. IEEE Transactions on Software Engineering 5(3): 203-216.

Digital Library

[6]

Burnim, J., Elmas, T., Necula, G., Sen, K. 2012. CONCURRIT: testing concurrent programs with programmable state-space exploration. In Proceedings of the 4th Usenix Conference on Hot Topics in Parallelism: 16-16; http://dl.acm.org/citation.cfm?id=2342788.2342804.

Digital Library

[7]

Clarke, E., Grumberg, O., Peled, D. 1999. Model checking. Cambridge: MIT Press; http://books.google.ca/books?id=Nmc4wEaLXFEC.

Digital Library

[8]

Click, C. 2007. A lock-free hash table. JavaOne Conference.

[9]

Corbet, J. 2006. The kernel lock validator. LWN; http://lwn.net/Articles/185666/.

[10]

Desnoyers, M. 2009. Low-impact operating system tracing. Ph.D. dissertation. Ecole Polytechnique de Montreal; http://www.lttng.org/pub/thesis/desnoyers-dissertation-2009-12.pdf.

[11]

Desnoyers, M., McKenney, P. E., Dagenais, M. R. Forthcoming. Multicore systems modeling for formal verification of parallel algorithms. Operating Systems Review.

[12]

Desnoyers, M., McKenney, P. E., Stern, A. S., Dagenais, M. R., Walpole, J. 2012. User-level implementations of read-copy-update. IEEE Transactions on Parallel and Distributed Systems 23(2): 375-382.

Digital Library

[13]

Drusinsky, D. 2011. Modeling and Verification Using UML Statecharts. Elsevier Science; http://books.google.ca/books?id=JMz-SWTfgiAC.

[14]

Ferrante, J., Ottenstein, K. J., Warren, J. D. 1987. The program dependence graph and its use in optimization. ACM Transactions on Programming Languages and Systems 9(3): 319-349; http://doi.acm.org/10.1145/24039.24041.

Digital Library

[15]

Gosling, J., Joy, B., Steele, G. L., Jr., Bracha, G., Buckley, A. 2013. The Java Language Specification, Java SE 7 Edition. Pearson Education; http://books.google.ca/books?id=2RYN9exiTnYC.

Digital Library

[16]

Gotsman, A., Cook, B., Parkinson, M., Vafeiadis, V. 2009. Proving that nonblocking algorithms don't block. In Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages: 16-28; http://doi.acm.org/10.1145/1480881.1480886.

Digital Library

[17]

Gotsman, A., Rinetzky, N., Yang, H. 2013. Verifying concurrent memory reclamation algorithms with grace. In European Symposium on Programming. Rome, Italy: Springer.

Digital Library

[18]

Haas, A., Kirsch, C. M., Lippautz, M., Payer, H. 2012. How FIFO is your concurrent FIFO queue? In Proceedings of the Workshop on Relaxing Synchronization for Multicore and Manycore Scalability.

Digital Library

[19]

Herlihy, M. 1991. Wait-free synchronization. ACM Transactions on Programming Languages and Systems 13(1): 124-149; http://doi.acm.org/10.1145/114005.102808.

Digital Library

[20]

Herlihy, M. P., Wing, J. M. 1990. Linearizability: a correctness condition for concurrent objects. ACM Transactions on Programming Languages and Systems 12(3): 463-492; http://doi.acm.org/10.1145/78969.78972.

Digital Library

[21]

Holzmann, G. J. 1997. The model checker Spin. IEEE Transactions on Software Engineering 23(5): 279-295.

Digital Library

[22]

IBM. 2010. Power ISA Version 2.06 Revision B; http://www.power.org/resources/reading/.

[23]

Intel Corporation. 2011. Intel 64 and IA-32 Architectures Software Developer's Manual: Instruction Set Reference, A-Z; http://download.intel.com/products/processor/manual/325383.pdf.

[24]

International Organization for Standardization. 2011. Programming languages - C++, ISO/IEC 14882:2011.

[25]

Kirsch, C. M., Lippautz, M., Payer, H. 2012. Fast and scalable k-fifo queues. University of Salzburg, Salzburg, Austria. Technical Report 2012-04.

[26]

Michael, M. M. 2004. Hazard pointers: safe memory reclamation for lock-free objects. IEEE Transactions on Parallel and Distributed Systems 15(6): 491-504; http://ieeexplore.ieee.org/xpl/articleDetails.jsp?tp=&arnumber=1291819&queryText%3Dhazard+pointers.

Digital Library

[27]

Michael, M. M., Scott, M. L. 1996. Simple, fast, and practical nonblocking and blocking concurrent queue algorithms. In Proceedings of the 15th Annual ACM Symposium on Principles of Distributed Computing: 267-275; http://doi.acm.org/10.1145/248052.248106.

Digital Library

[28]

MIPS Technologies Inc. 2012. MIPS Architecture for Programmers, Volume II: The MIPS64 Instruction Set.

[29]

Olszewski, M., Ansel, J., Amarasinghe, S. 2009. Kendo: efficient deterministic multithreading in software. ACM SIGPLAN Notices 44(3): 97-108; http://dl.acm.org/citation.cfm?id=1508256.

Digital Library

[30]

Sarkar, S., Sewell, P., Alglave, J., Maranget, L., Williams, D. 2011. Understanding Power multiprocessors. ACM SIGPLAN Notices 46(6): 175-186; http://doi.acm.org/10.1145/1993316.1993520.

Digital Library

Cited By

Changwoo Min Young Ik Eom (2015)Integrating Lock-Free and Combining Techniques for a Practical and Scalable FIFO QueueIEEE Transactions on Parallel and Distributed Systems10.1109/TPDS.2014.233300726:7(1910-1922)Online publication date: 1-Jul-2015
https://dl.acm.org/doi/10.1109/TPDS.2014.2333007

Index Terms

Proving the Correctness of Nonblocking Data Structures: So you’ve decided to use a nonblocking data structure, and now you need to be certain of its correctness. How can this be achieved?

Recommendations

Transactional Composition of Nonblocking Data Structures
PPoPP '23: Proceedings of the 28th ACM SIGPLAN Annual Symposium on Principles and Practice of Parallel Programming

We introduce nonblocking transaction composition (NBTC), a new methodology for atomic composition of nonblocking operations on concurrent data structures. Unlike previous software transactional memory (STM) approaches, NBTC leverages the linearizability ...
Transactional Composition of Nonblocking Data Structures
SPAA '23: Proceedings of the 35th ACM Symposium on Parallelism in Algorithms and Architectures

This paper introduces nonblocking transaction composition (NBTC), a new methodology for atomic composition of nonblocking operations on concurrent data structures. Unlike previous software transactional memory (STM) approaches, NBTC leverages the ...
A Transactional Correctness Tool for Abstract Data Types

Transactional memory simplifies multiprocessor programming by providing the guarantee that a sequential block of code in the form of a transaction will exhibit atomicity and isolation. Transactional data structures offer the same guarantee to concurrent ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Queue

Queue Volume 11, Issue 5

Concurrency

May 2013

60 pages

ISSN:1542-7730

EISSN:1542-7749

DOI:10.1145/2488364

Issue’s Table of Contents

Copyright © 2013 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 15 May 2013

Published in QUEUE Volume 11, Issue 5

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Research-article
Popular
Refereed

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

1
Total Citations
View Citations
39,707
Total Downloads

Downloads (Last 12 months)2,594
Downloads (Last 6 weeks)336

Reflects downloads up to 19 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Changwoo Min Young Ik Eom (2015)Integrating Lock-Free and Combining Techniques for a Practical and Scalable FIFO QueueIEEE Transactions on Parallel and Distributed Systems10.1109/TPDS.2014.233300726:7(1910-1922)Online publication date: 1-Jul-2015
https://dl.acm.org/doi/10.1109/TPDS.2014.2333007

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Magazine Site

View this article on the magazine site (external)

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents