research-article

CDSchecker: checking concurrent data structures written with C/C++ atomics

Authors:

Brian DemskyAuthors Info & Claims

ACM SIGPLAN Notices, Volume 48, Issue 10

Pages 131 - 150

https://doi.org/10.1145/2544173.2509514

Published: 29 October 2013 Publication History

Abstract

Writing low-level concurrent software has traditionally required intimate knowledge of the entire toolchain and often has involved coding in assembly. New language standards have extended C and C++ with support for low-level atomic operations and a weak memory model, enabling developers to write portable and efficient multithreaded code.

Developing correct low-level concurrent code is well-known to be especially difficult under a weak memory model, where code behavior can be surprising. Building reliable concurrent software using C/C++ low-level atomic operations will likely require tools that help developers discover unexpected program behaviors.

In this paper we present CDSChecker, a tool for exhaustively exploring the behaviors of concurrent code under the C/C++ memory model. We develop several novel techniques for modeling the relaxed behaviors allowed by the memory model and for minimizing the number of execution behaviors that CDSChecker must explore. We have used CDSChecker to exhaustively unit test several concurrent data structure implementations on specific inputs and have discovered errors in both a recently published C11 implementation of a work-stealing queue and a single producer, single consumer queue implementation.

References

[1]

http://stackoverflow.com/questions/8115267/writing-a-spinning-thread-barrier-using-c11-atomics. Oct. 2012.

[2]

ISO/IEC 9899:2011, Information technology - programming languages - C.

[3]

ISO/IEC 14882:2011, Information technology - programming languages - C++.

[4]

http://www.justsoftwaresolutions.co.uk/threading/. Dec. 2012.

[5]

http://cbloomrants.blogspot.com/2011/07/07-18-11-mcs-list-based-lock_18.html. Oct. 2012.

[6]

http://cbloomrants.blogspot.com/2011/07/07-30-11-look-at-some-bounded-queues.html. Oct. 2012.

[7]

https://groups.google.com/forum/#!msg/comp.programming.threads/nSSFT9vKEe0/7eD3ioDg6nEJ. Oct. 2012.

[8]

M. Batty, S. Owens, S. Sarkar, P. Sewell, and T. Weber. Mathematizing C++ concurrency. In Proceedings of the Symposium on Principles of Programming Languages, 2011.

Digital Library

[9]

M. Batty, M. Dodds, and A. Gotsman. Library abstraction for C/C++ concurrency. In Proceedings of the Symposium on Principles of Programming Languages, 2013.

Digital Library

[10]

J. C. Blanchette, T.Weber, M. Batty, S. Owens, and S. Sarkar. Nitpicking C++ concurrency. In Proceedings of the 13th International ACM SIGPLAN Symposium on Principles and Practices of Declarative Programming, 2011.

Digital Library

[11]

H. Boehm. Can seqlocks get along with programming language memory models? In Proceedings of the 2012 ACM SIGPLAN Workshop on Memory Systems Performance and Correctness, 2012.

Digital Library

[12]

H. J. Boehm and S. V. Adve. Foundations of the C++ concurrency memory model. In Proceedings of the 2008 ACM SIGPLAN Conference on Programming Language Design and Implementation, 2008.

Digital Library

[13]

S. Burckhardt, C. Dern, M. Musuvathi, and R. Tan. Line-up: A complete and automatic linearizability checker. In Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation, 2010.

Digital Library

[14]

C. Click. A lock-free hash table. http://www.azulsystems.com/events/javaone_2007/2007_LockFreeHash.pdf, May 2007.

[15]

A. De, A. Roychoudhury, and D. D'Souza. Java memory model aware software validation. In Proceedings of the 8th ACM SIGPLAN-SIGSOFTWorkshop on Program Analysis for Software Tools and Engineering, 2008.

Digital Library

[16]

T. Elmas, S. Qadeer, and S. Tasiran. Goldilocks: A race and transaction-aware Java runtime. In Proceedings of the 2007 ACM SIGPLAN Conference on Programming Language Design and Implementation, 2007.

Digital Library

[17]

D. Engler and K. Ashcraft. RacerX: Effective, static detection of race conditions and deadlocks. In Proceedings of the Nineteenth ACM Symposium on Operating Systems Principles, 2003.

Digital Library

[18]

C. Flanagan and S. N. Freund. FastTrack: Efficient and precise dynamic race detection. In Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation, 2009.

Digital Library

[19]

C. Flanagan and S. N. Freund. Adversarial memory for detecting destructive races. In Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation, 2010.

Digital Library

[20]

C. Flanagan and P. Godefroid. Dynamic partial-order reduction for model checking software. In Proceedings of the Symposium on Principles of Programming Languages, Jan. 2005.

Digital Library

[21]

P. Godefroid. Partial-order methods for the verification of concurrent systems: An approach to the state-explosion problem. Lecture Notes in Computer Science, 1996.

Digital Library

[22]

P. Godefroid. Model checking for programming languages using VeriSoft. In Proceedings of the Symposium on Principles of Programming Languages, 1997.

Digital Library

[23]

G. J. Holzmann. The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley Professional, 1st edition, 2003.

Digital Library

[24]

T. Q. Huynh and A. Roychoudhury. A memory model sensitive checker for C#. In Proceedings of the 14th International Conference on Formal Methods, 2006.

Digital Library

[25]

B. Jonsson. State-space exploration for concurrent algorithms under weak memory orderings. SIGARCH Computer Architecture News, 36(5):65--71, June 2009.

Digital Library

[26]

M. Kuperstein, M. Vechev, and E. Yahav. Automatic inference of memory fences. In Proceedings of the Conference on Formal Methods in Computer-Aided Design, 2010.

Digital Library

[27]

M. Kuperstein, M. Vechev, and E. Yahav. Partial-coherence abstractions for relaxed memory models. In Proceedings of the 2011 ACM SIGPLAN Conference on Programming Language Design and Implementation, 2011.

Digital Library

[28]

L. Lamport. Time, clocks, and the ordering of events in a distributed system. Communications of the ACM, 21(7):558--565, July 1978.

Digital Library

[29]

N. M. Lê, A. Pop, A. Cohen, and F. Zappa Nardelli. Correct and efficient work-stealing for weak memory models. In Proceedings of the 18th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, 2013.

Digital Library

[30]

B. Lucia, L. Ceze, K. Strauss, S. Qadeer, and H. Boehm. Conflict exceptions: Simplifying concurrent language semantics with precise hardware exceptions for data-races. In Proceedings of the 37th Annual International Symposium on Computer Architecture, 2010.

Digital Library

[31]

D. Marino, A. Singh, T. Millstein, M. Musuvathi, and S. Narayanasamy. A case for an sc-preserving compiler. In Proceedings of the 2011 ACM SIGPLAN Conference on Programming Language Design and Implementation, 2011.

Digital Library

[32]

J. M. Mellor-Crummey and M. L. Scott. Synchronization without contention. In Proceedings of the Fourth International Conference on Architectural Support for Programming Languages and Operating Systems, pages 269--278, 1991.

Digital Library

[33]

M. M. Michael and M. L. Scott. Simple, fast, and practical non-blocking and blocking concurrent queue algorithms. In Proceedings of the Fifteenth Annual ACM Symposium on Principles of Distributed Computing, 1996.

Digital Library

[34]

M. Musuvathi, S. Qadeer, P. A. Nainar, T. Ball, G. Basler, and I. Neamtiu. Finding and reproducing Heisenbugs in concurrent programs. In Proceedings of the 8th Symposium on Operating Systems Design and Implementation, 2008.

Digital Library

[35]

S. Park and D. L. Dill. An executable specification and verifier for relaxed memory order. IEEE Transactions on Computers, 48, 1999.

Digital Library

[36]

S. Savage, M. Burrows, G. Nelson, P. Sobalvarro, and T. Anderson. Eraser: A dynamic data race detector for multithreaded programs. ACM Transactions on Computing Systems, 15:391--411, Nov. 1997.

Digital Library

[37]

D. Vyukov. Relacy race detector. http://relacy.sourceforge.net/, 2011 Oct.

[38]

C. Wang, Y. Yang, A. Gupta, and G. Gopalakrishnan. Dynamic model checking with property driven pruning to detect race conditions. ATVA LNCS, (126--140), 2008.

Digital Library

[39]

Y. Yang, X. Chen, G. Gopalakrishnan, and R. M. Kirby. Efficient stateful dynamic partial order reduction. In Proceedings of the 15th International SPIN Workshop on Model Checking Software, 2008.

Digital Library

[40]

Y. Yang, X. Chen, G. Gopalakrishnan, and C. Wang. Automatic discovery of transition symmetry in multithreaded programs using dynamic analysis. In Proceedings of the 16th International SPIN Workshop on Model Checking Software, pages 279--295, 2009.

Digital Library

Cited By

Sun XGupta RBond MLee JPayer H(2024)SSRD: Shapes and Summaries for Race Detection in Concurrent Data StructuresProceedings of the 2024 ACM SIGPLAN International Symposium on Memory Management10.1145/3652024.3665505(68-81)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3652024.3665505
Iorga DWickerson JDonaldson A(2023)Simulating Operational Memory Models Using Off-the-Shelf Program Analysis ToolsIEEE Transactions on Software Engineering10.1109/TSE.2023.332605649:12(5084-5102)Online publication date: 1-Dec-2023
https://dl.acm.org/doi/10.1109/TSE.2023.3326056
Biswas RKakwani DVedurada JEnea CLal A(2021)MonkeyDB: effectively testing correctness under weak isolation levelsProceedings of the ACM on Programming Languages10.1145/34855465:OOPSLA(1-27)Online publication date: 15-Oct-2021
https://dl.acm.org/doi/10.1145/3485546
Show More Cited By

Index Terms

CDSchecker: checking concurrent data structures written with C/C++ atomics
1. Software and its engineering
  1. Software organization and properties
    1. Software functional properties
      1. Formal methods
        Model checking
2. Theory of computation
  1. Logic
    1. Verification by model checking
  2. Semantics and reasoning
    1. Program reasoning
      1. Program verification

Recommendations

A Practical Approach for Model Checking C/C++11 Code

Writing low-level concurrent software has traditionally required intimate knowledge of the entire toolchain and often has involved coding in assembly. New language standards have extended C and C++ with support for low-level atomic operations and a weak ...
CDSchecker: checking concurrent data structures written with C/C++ atomics
OOPSLA '13: Proceedings of the 2013 ACM SIGPLAN international conference on Object oriented programming systems languages & applications

Writing low-level concurrent software has traditionally required intimate knowledge of the entire toolchain and often has involved coding in assembly. New language standards have extended C and C++ with support for low-level atomic operations and a weak ...
SATCheck: SAT-directed stateless model checking for SC and TSO
OOPSLA 2015: Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications

Writing low-level concurrent code is well known to be challenging and error prone. The widespread deployment of multi-core hardware and the shift towards using low-level concurrent data structures has moved the problem into the mainstream. Finding bugs ...

Comments

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 48, Issue 10

OOPSLA '13

October 2013

867 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/2544173

Editor:
Mark W. Bailey
Hamilton College, Clinton, NY

Issue’s Table of Contents

OOPSLA '13: Proceedings of the 2013 ACM SIGPLAN international conference on Object oriented programming systems languages & applications
October 2013
904 pages
ISBN:9781450323741
DOI:10.1145/2509136
Co-chair:
Antony Hosking
Purdue University, USA
,
General Chair:
Patrick Eugster
Purdue University, USA
,
Program Chair:
Cristina V. Lopes
University of California, Irvine, USA

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 the author(s) 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: 29 October 2013

Published in SIGPLAN Volume 48, Issue 10

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

103
Total Citations
View Citations
594
Total Downloads

Downloads (Last 12 months)45
Downloads (Last 6 weeks)5

Reflects downloads up to 19 Oct 2024

Other Metrics

View Author Metrics

Citations

Cited By

Sun XGupta RBond MLee JPayer H(2024)SSRD: Shapes and Summaries for Race Detection in Concurrent Data StructuresProceedings of the 2024 ACM SIGPLAN International Symposium on Memory Management10.1145/3652024.3665505(68-81)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3652024.3665505
Iorga DWickerson JDonaldson A(2023)Simulating Operational Memory Models Using Off-the-Shelf Program Analysis ToolsIEEE Transactions on Software Engineering10.1109/TSE.2023.332605649:12(5084-5102)Online publication date: 1-Dec-2023
https://dl.acm.org/doi/10.1109/TSE.2023.3326056
Biswas RKakwani DVedurada JEnea CLal A(2021)MonkeyDB: effectively testing correctness under weak isolation levelsProceedings of the ACM on Programming Languages10.1145/34855465:OOPSLA(1-27)Online publication date: 15-Oct-2021
https://dl.acm.org/doi/10.1145/3485546
Luo WDemsky BSherwood TBerger EKozyrakis C(2021)C11Tester: a race detector for C/C++ atomicsProceedings of the 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems10.1145/3445814.3446711(630-646)Online publication date: 19-Apr-2021
https://dl.acm.org/doi/10.1145/3445814.3446711
Singh SSharma DSharma S(2021)Dynamic Verification of C11 Concurrency over Multi Copy Atomics2021 International Symposium on Theoretical Aspects of Software Engineering (TASE)10.1109/TASE52547.2021.00023(39-46)Online publication date: Aug-2021
https://doi.org/10.1109/TASE52547.2021.00023
Schmaus FPfeiffer NHonig TNolte JSchroder-Preikschat W(2021)Nowa: A Wait-Free Continuation-Stealing Concurrency Platform2021 IEEE International Parallel and Distributed Processing Symposium (IPDPS)10.1109/IPDPS49936.2021.00044(360-371)Online publication date: May-2021
https://doi.org/10.1109/IPDPS49936.2021.00044
Chen DJiang YXu CMa X(2021)On interleaving space exploration of multi-threaded programsFrontiers of Computer Science: Selected Publications from Chinese Universities10.1007/s11704-020-9501-615:4Online publication date: 1-Aug-2021
https://dl.acm.org/doi/10.1007/s11704-020-9501-6
Kirkham JSorensen TTureci EMartonosi M(2020)Foundations of empirical memory consistency testingProceedings of the ACM on Programming Languages10.1145/34282944:OOPSLA(1-29)Online publication date: 13-Nov-2020
https://dl.acm.org/doi/10.1145/3428294
Chin KTsay RWu H(2020)A Heuristic Region-based Concurrency Bug Testing Approach2020 IEEE Intl Conf on Parallel & Distributed Processing with Applications, Big Data & Cloud Computing, Sustainable Computing & Communications, Social Computing & Networking (ISPA/BDCloud/SocialCom/SustainCom)10.1109/ISPA-BDCloud-SocialCom-SustainCom51426.2020.00168(1126-1135)Online publication date: Dec-2020
https://doi.org/10.1109/ISPA-BDCloud-SocialCom-SustainCom51426.2020.00168
López-Gómez Jdel Rio Astorga DDolz MFernández JGarcía J(2020)Detecting semantic violations of lock-free data structures through C++ contractsThe Journal of Supercomputing10.1007/s11227-019-02827-476:7(5057-5078)Online publication date: 1-Jul-2020
https://dl.acm.org/doi/10.1007/s11227-019-02827-4
Show More Cited By

View Options

Get Access

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 Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents