research-article

Open access

C11Tester: a race detector for C/C++ atomics

Authors:

Brian DemskyAuthors Info & Claims

ASPLOS '21: Proceedings of the 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems

Pages 630 - 646

https://doi.org/10.1145/3445814.3446711

Published: 17 April 2021 Publication History

Abstract

Writing correct concurrent code that uses atomics under the C/C++ memory model is extremely difficult. We present C11Tester, a race detector for the C/C++ memory model that can explore executions in a larger fragment of the C/C++ memory model than previous race detector tools. Relative to previous work, C11Tester's larger fragment includes behaviors that are exhibited by ARM processors. C11Tester uses a new constraint-based algorithm to implement modification order that is optimized to allow C11Tester to make decisions in terms of application-visible behaviors. We evaluate C11Tester on several benchmark applications, and compare C11Tester's performance to both tsan11rec, the state of the art tool that controls scheduling for C/C++; and tsan11, the state of the art tool that does not control scheduling.

Supplementary Material

Auxiliary Archive (asplos21main-p172-p-archive.zip)

Supplemental material - C11Tester: A Race Detector for C/C++ Atomics Technical Report

Download
1.01 MB

References

[1]

2020. N4849: Working Draft, Standard for ProgrammingLanguage C++. http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2020/n4849.pdf.

[2]

Parosh Abdulla, Stavros Aronis, Bengt Jonsson, and Konstantinos Sagonas. 2014. Optimal Dynamic Partial Order Reduction. In Proceedings of the 2014 Symposium on Principles of Programming Languages. 373?384. http://doi.acm.org/10.1145/2535838.2535845

Digital Library

[3]

Parosh Aziz Abdulla, Stavros Aronis, Mohamed Faouzi Atig, Bengt Jonsson, Carl Leonardsson, and Konstantinos Sagonas. 2015. Stateless model checking for TSO and PSO. In Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 353?367. http://link.springer.com/chapter/10.1007

Digital Library

[4]

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bengt Jonsson, Magnus L\aang, Tuan Phong Ngo, and Konstantinos Sagonas. 2019. Optimal Stateless Model Checking for Reads-from Equivalence Under Sequential Consistency. Proceedings of ACM on Programming Languages 3, OOPSLA, Article 150 (Oct. 2019), 29 pages. issn:2475-1421 https://doi.org/10.1145/3360576

Digital Library

[5]

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bengt Jonsson, and Tuan Phong Ngo. 2018. Optimal Stateless Model Checking Under the Release-acquire Semantics. Proceedings of the ACM on Programming Languages 2, OOPSLA, Article 135 (Oct. 2018), 29 pages. issn:2475-1421 https://doi.org/10.1145/3276505

Digital Library

[6]

Jade Alglave, Luc Maranget, and Michael Tautschnig. 2014. Herding Cats: Modelling, Simulation, Testing, and Data Mining for Weak Memory. ACM Transactions on Programming Languages and Systems 36, 2 (July 2014), 7:1?7:74. http://doi.acm.org/10.1145/2627752

Digital Library

[7]

F. Eugene Aumson. 2018. gdax-orderbook-hpp. https://github.com/feuGeneA/gdax-orderbook-hpp.

[8]

Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, and Tjark Weber. 2011. Mathematizing C++ Concurrency. In Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages.

Digital Library

[9]

Pete Becker. 2011. ISO/IEC 14882:2011, Information Technology ? Programming Languages ? C++.

[10]

Jasmin Christian Blanchette, Tjark Weber, Mark Batty, Scott Owens, and Susmit Sarkar. 2011. Nitpicking C++ Concurrency. In Proceedings of the 13th International ACM SIGPLAN Symposium on Principles and Practices of Declarative Programming. 113?124. http://doi.acm.org/10.1145/2003476.2003493

Digital Library

[11]

Hans Boehm and Brian Demsky. 2014. Outlawing Ghosts: Avoiding Out-of-Thin-Air Results. In Proceedings of ACM SIGPLAN Workshop on Memory Systems Performance and Correctness. 7:1?7:6. http://doi.acm.org/10.1145/2618128.2618134

Digital Library

[12]

Hans-J. Boehm. 2012. Can Seqlocks Get Along with Programming Language Memory Models?. In Proceedings of the 2012 ACM SIGPLAN Workshop on Memory Systems Performance and Correctness. 12?20. http://doi.acm.org/10.1145/2247684.2247688

Digital Library

[13]

Hans-J. Boehm. 2013. N3786: Prohibiting "out of thin air" results in C++14. http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2013/n3786.htm.

[14]

Hans-J. Boehm, Mark Batty, Brian Demsky, Olivier Giroux, Paul McKenney, Peter Sewell, Francesco Zappa Nardelli, et al\mbox. 2013. N3710: Specifying the absence of "out of thin air" results (LWG2265). http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2013/n3710.html.

[15]

Hans-J. Boehm, Olivier Giroux, and Viktor Vafeiades. 2018. P0982R0: Weaken Release Sequences. http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2018/p0982r0.html.

[16]

Sebastian Burckhardt, Rajeev Alur, and Milo M. K. Martin. 2007. CheckFence: Checking Consistency of Concurrent Data Types on Relaxed Memory Models. In Proceedings of the 2007 Conference on Programming Language Design and Implementation. 12?21. http://doi.acm.org/10.1145/1250734.1250737

Digital Library

[17]

Man Cao, Jake Roemer, Aritra Sengupta, and Michael D. Bond. 2016. Prescient Memory: Exposing Weak Memory Model Behavior by Looking into the Future. In Proceedings of the 2016 ACM SIGPLAN International Symposium on Memory Management. 99?110. http://doi.acm.org/10.1145/2926697.2926700

Digital Library

[18]

Brian Demsky and Patrick Lam. 2015. SATCheck: SAT-Directed Stateless Model Checking for SC and TSO. In Proceedings of the 2015 Conference on Object-Oriented Programming, Systems, Languages, and Applications. 20?36. http://doi.acm.org/10.1145/2814270.2814297

Digital Library

[19]

Changxue Deng. 2018. Mabain: A fast and light-weighted key-value store library. https://github.com/chxdeng/mabain.

[20]

Ulrich Drepper. 2013. ELF Handling For Thread-Local Storage. https://akkadia.org/drepper/tls.pdf.

[21]

Tayfun Elmas, Jacob Burnim, George Necula, and Koushik Sen. 2013. CONCURRIT: A Domain Specific Language for Reproducing Concurrency Bugs. In Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation (Seattle, Washington, USA) (PLDI '13). 153?164. isbn:978-1-4503-2014-6 https://doi.org/10.1145/2491956.2462162

Digital Library

[22]

Tayfun Elmas, Shaz Qadeer, and Serdar Tasiran. 2007. Goldilocks: A Race and Transaction-Aware Java Runtime. In Proceedings of the 2007 ACM SIGPLAN Conference on Programming Language Design and Implementation. 245?255. http://doi.acm.org/10.1145/1250734.1250762

Digital Library

[23]

Dawson Engler and Ken Ashcraft. 2003. RacerX: Effective, Static Detection of Race Conditions and Deadlocks. In Proceedings of the Nineteenth ACM Symposium on Operating Systems Principles. 237?252. http://doi.acm.org/10.1145/945445.945468

Digital Library

[24]

Cormac Flanagan and Stephen N. Freund. 2009. FastTrack: Efficient and Precise Dynamic Race Detection. In Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation. 121?133. http://doi.acm.org/10.1145/1542476.1542490

Digital Library

[25]

Cormac Flanagan and Stephen N. Freund. 2010. Adversarial memory for detecting destructive races. In Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation. 244?254. http://doi.acm.org/10.1145/1806596.1806625

Digital Library

[26]

Cormac Flanagan and Patrice Godefroid. 2005. Dynamic Partial-Order Reduction for Model Checking Software. In Proceedings of the 2005 Symposium on Principles of Programming Languages. 110?121. http://doi.acm.org/10.1145/1040305.1040315

Digital Library

[27]

Jeff Huang. 2015. Stateless Model Checking Concurrent Programs with Maximal Causality Reduction. In Proceedings of the 2015 Conference on Programming Language Design and Implementation. 165?174. http://doi.acm.org/10.1145/2813885.2737975

Digital Library

[28]

Jeff Huang, Patrick Meredith, and Grigore Rosu. 2014. Maximal Sound Predictive Race Detection with Control Flow Abstraction. In Proceedings of the 35th annual ACM SIGPLAN conference on Programming Language Design and Implementation (PLDI'14). ACM, 337?348. https://doi.org/10.1145/2594291.2594315

Digital Library

[29]

Shiyou Huang and Jeff Huang. 2016. Maximal Causality Reduction for TSO and PSO. In Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications. 447?461. http://doi.acm.org/10.1145/2983990.2984025

Digital Library

[30]

Bengt Jonsson. 2009. State-space exploration for concurrent algorithms under weak memory orderings. SIGARCH Computer Architecture News 36, 5 (June 2009), 65?71. http://doi.acm.org/10.1145/1556444.1556453

Digital Library

[31]

ISO JTC. 2011. ISO/IEC 9899:2011, Information Technology ? Programming Languages ? C.

[32]

Max Khiszinsky. 2017. https://github.com/khizmax/libcds.

[33]

Michalis Kokologiannakis, Ori Lahav, Konstantinos Sagonas, and Viktor Vafeiadis. 2017. Effective Stateless Model Checking for C/C++ Concurrency. Proceedings of the ACM on Programming Languages 2, POPL, Article 17 (December 2017), 32 pages. issn:2475-1421 https://doi.org/10.1145/3158105

Digital Library

[34]

Michalis Kokologiannakis, Azalea Raad, and Viktor Vafeiadis. 2019. Model Checking for Weakly Consistent Libraries. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation (Phoenix, AZ, USA) (PLDI 2019). 96?110. isbn:978-1-4503-6712-7 https://doi.org/10.1145/3314221.3314609

Digital Library

[35]

Michael Kuperstein, Martin Vechev, and Eran Yahav. 2010. Automatic inference of memory fences. In Proceedings of the Conference on Formal Methods in Computer-Aided Design. 111?120. http://dl.acm.org/citation.cfm?id=1998496.1998518

Digital Library

[36]

Leslie Lamport. 1978. Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21, 7 (July 1978), 558?565.

Digital Library

[37]

Christopher Lidbury and Alastair F. Donaldson. 2017. Dynamic Race Detection for C++11. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (Paris, France) (POPL 2017). ACM, New York, NY, USA, 443?457. isbn:978-1-4503-4660-3 https://doi.org/10.1145/3009837.3009857

Digital Library

[38]

Christopher Lidbury and Alastair F. Donaldson. 2019. Sparse Record and Replay with Controlled Scheduling. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2019). 576?593. https://doi.org/10.1145/3314221.3314635

Digital Library

[39]

Brandon Lucia, Luis Ceze, Karin Strauss, Shaz Qadeer, and Hans Boehm. 2010. Conflict Exceptions: Simplifying Concurrent Language Semantics with Precise Hardware Exceptions for Data-Races. In Proceedings of the 37th Annual International Symposium on Computer Architecture. 210?221. http://doi.acm.org/10.1145/1815961.1815987

Digital Library

[40]

Weiyu Luo and Brian Demsky. 2021. C11Tester: A Race Detector for C/C++ Atomics. Technical Report. (2021). arxiv:2102.07901 [cs.PL]

[41]

Nuno Machado, Brandon Lucia, and Luís Rodrigues. 2015. Concurrency Debugging with Differential Schedule Projections. SIGPLAN Not. 50, 6 (June 2015), 586?595. issn:0362-1340 https://doi.org/10.1145/2813885.2737973

Digital Library

[42]

Nuno Machado, Brandon Lucia, and Luís Rodrigues. 2016. Production-Guided Concurrency Debugging. SIGPLAN Not. 51, 8, Article 29 (Feb. 2016), 12 pages. issn:0362-1340 https://doi.org/10.1145/3016078.2851149

Digital Library

[43]

Pablo Montesinos, Luis Ceze, and Josep Torrellas. 2008. DeLorean: Recording and Deterministically Replaying Shared-Memory Multiprocessor Execution Efficiently. SIGARCH Comput. Archit. News 36, 3 (June 2008), 289?300. issn:0163-5964 https://doi.org/10.1145/1394608.1382146

Digital Library

[44]

Brian Norris and Brian Demsky. 2013. CDSChecker: Checking Concurrent Data Structures Written with C/C++ Atomics. In Proceedings of the 2013 Conference on Object-Oriented Programming, Systems, Languages, and Applications. 131?150. http://doi.acm.org/10.1145/2544173.2509514

Digital Library

[45]

Brian Norris and Brian Demsky. 2016. A Practical Approach for Model Checking C/C++11 Code. ACM Transactions on Programming Languages and Systems 38, 3 (May 2016), 10:1?10:51.

Digital Library

[46]

Peizhao Ou and Brian Demsky. 2018. Towards Understanding the Costs of Avoiding Out-of-thin-air Results. Proceedings of the ACM on Programming Languages Volume 2 Issue OOPSLA 2, OOPSLA (Oct. 2018), 136:1?136:29. https://doi.org/10.1145/3276506

Digital Library

[47]

Seungjoon Park and David L. Dill. 1999. An Executable Specification and Verifier for Relaxed Memory Order. IEEE Trans. Comput. 48, 2 (February 1999), 227?235. http://dx.doi.org/10.1109/12.752664

Digital Library

[48]

Gregor Richards, Andreas Gal, Brendan Eich, and Jan Vitek. 2011. Automated Construction of JavaScript Benchmarks. In Proceedings of the 2011 ACM International Conference on Object Oriented Programming Systems Languages and Applications (Portland, Oregon, USA) (OOPSLA ?11). Association for Computing Machinery, New York, NY, USA, 677?694. isbn:9781450309400 https://doi.org/10.1145/2048066.2048119

Digital Library

[49]

Mathias Guenter Ricken. 2011. A Framework for Testing Concurrent Programs. Ph.D. Dissertation. Houston, TX, USA. Advisor(s) Cartwright, Robert. isbn:978-1-124-77507-4 AAI3463989.

[50]

Koushik Sen. 2007. Effective Random Testing of Concurrent Programs. In Proceedings of the Twenty-second IEEE/ACM International Conference on Automated Software Engineering (Atlanta, Georgia, USA) (ASE '07). 323?332. isbn:978-1-59593-882-4 https://doi.org/10.1145/1321631.1321679

Digital Library

[51]

Stephen Tu, Wenting Zheng, and Eddie Kohler. 2015. Silo: Multicore in-memory storage engine. https://github.com/stephentu/silo.

[52]

Stephen Tu, Wenting Zheng, Eddie Kohler, Barbara Liskov, and Samuel Madden. 2013. Speedy Transactions in Multicore In-memory Databases. In Proceedings of the Twenty-Fourth ACM Symposium on Operating Systems Principles (SOSP '13). 18?32. https://doi.org/10.1145/2517349.2522713

Digital Library

[53]

Paul Turner. 2013. User-level threads...with threads. https://blog.linuxplumbersconf.org/2013/ocw/system/presentations/1653/original/LPC\

[54]

Viktor Vafeiadis and Chinmay Narayan. 2013. Relaxed separation logic: A program logic for C11 concurrency. In Proceedings of the 2013 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications. 867?884.

Digital Library

[55]

Dmitriy Vyukov. 2011. Relacy Race Detector. http://relacy.sourceforge.net/.

[56]

Naling Zhang, Markus Kusano, and Chao Wang. 2015. Dynamic Partial Order Reduction for Relaxed Memory Models. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation. 250?259. http://doi.acm.org/10.1145/2737924.2737956

Digital Library

[57]

Xinjing Zhou. 2015. Iris: A low latency asynchronous C++ logging library. https://github.com/zxjcarrot/iris.

Cited By

Margalit RChristakis MPradel M(2024)Robustness against the C/C++11 Memory ModelProceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3650212.3685549(1881-1885)Online publication date: 11-Sep-2024
https://dl.acm.org/doi/10.1145/3650212.3685549
Chakraborty SKrishna SMathur UPavlogiannis A(2024)How Hard Is Weak-Memory Testing?Proceedings of the ACM on Programming Languages10.1145/36329088:POPL(1978-2009)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632908
Tunç HDeshmukh ACirisci BEnea CPavlogiannis ATsafrir DMusuvathi MGupta RAbu-Ghazaleh N(2024)CSSTs: A Dynamic Data Structure for Partial Orders in Concurrent Execution AnalysisProceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 310.1145/3620666.3651358(223-238)Online publication date: 27-Apr-2024
https://dl.acm.org/doi/10.1145/3620666.3651358
Show More Cited By

Index Terms

C11Tester: a race detector for C/C++ atomics
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language types
        Concurrent programming languages

Recommendations

Dynamic race detection for C++11
POPL '17: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages

The intricate rules for memory ordering and synchronisation associated with the C/C++11 memory model mean that data races can be difficult to eliminate from concurrent programs. Dynamic data race analysis can pinpoint races in large and complex ...
Dynamic race detection for C++11
POPL '17

The intricate rules for memory ordering and synchronisation associated with the C/C++11 memory model mean that data races can be difficult to eliminate from concurrent programs. Dynamic data race analysis can pinpoint races in large and complex ...
Extended sequential reasoning for data-race-free programs
MSPC '11: Proceedings of the 2011 ACM SIGPLAN Workshop on Memory Systems Performance and Correctness

Most multithreaded programming languages prohibit or discourage data races. By avoiding data races, we are guaranteed that variables accessed within a synchronization-free code region cannot be modified by other threads, allowing us to reason about such ...

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

ASPLOS '21: Proceedings of the 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems

April 2021

1090 pages

ISBN:9781450383172

DOI:10.1145/3445814

General Chair:
Tim Sherwood
University of California at Santa Barbara, USA
,
Program Chairs:
Emery Berger
University of Massachusetts at Amherst, USA
,
Christos Kozyrakis
Stanford University, USA

Copyright �� 2021 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 17 April 2021

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Conference

ASPLOS '21

Sponsor:

SIGPLAN

ASPLOS '21: 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems

April 19 - 23, 2021

Virtual, USA

Acceptance Rates

Overall Acceptance Rate 535 of 2,713 submissions, 20%

Upcoming Conference

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

12
Total Citations
View Citations
1,966
Total Downloads

Downloads (Last 12 months)495
Downloads (Last 6 weeks)54

Reflects downloads up to 19 Oct 2024

Other Metrics

View Author Metrics

Citations

Cited By

Margalit RChristakis MPradel M(2024)Robustness against the C/C++11 Memory ModelProceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3650212.3685549(1881-1885)Online publication date: 11-Sep-2024
https://dl.acm.org/doi/10.1145/3650212.3685549
Chakraborty SKrishna SMathur UPavlogiannis A(2024)How Hard Is Weak-Memory Testing?Proceedings of the ACM on Programming Languages10.1145/36329088:POPL(1978-2009)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632908
Tunç HDeshmukh ACirisci BEnea CPavlogiannis ATsafrir DMusuvathi MGupta RAbu-Ghazaleh N(2024)CSSTs: A Dynamic Data Structure for Partial Orders in Concurrent Execution AnalysisProceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 310.1145/3620666.3651358(223-238)Online publication date: 27-Apr-2024
https://dl.acm.org/doi/10.1145/3620666.3651358
Wolff DShi ZDuck GMathur URoychoudhury ATsafrir DMusuvathi MGupta RAbu-Ghazaleh N(2024)Greybox Fuzzing for Concurrency TestingProceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 210.1145/3620665.3640389(482-498)Online publication date: 27-Apr-2024
https://dl.acm.org/doi/10.1145/3620665.3640389
Haas TMaseli RMeyer RPonce de León H(2023)Static Analysis of Memory Models for SMT EncodingsProceedings of the ACM on Programming Languages10.1145/36228557:OOPSLA2(1618-1647)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622855
Lee SCho MMargalit RHur CLahav O(2023)Putting Weak Memory in Order via a Promising Intermediate RepresentationProceedings of the ACM on Programming Languages10.1145/35912977:PLDI(1872-1895)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591297
Tunç HAbdulla PChakraborty SKrishna SMathur UPavlogiannis A(2023)Optimal Reads-From Consistency Checking for C11-Style Memory ModelsProceedings of the ACM on Programming Languages10.1145/35912517:PLDI(761-785)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591251
Gao MChakraborty SOzkan BAamodt TJerger NSwift M(2023)Probabilistic Concurrency Testing for Weak Memory ProgramsProceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 210.1145/3575693.3575729(603-616)Online publication date: 27-Jan-2023
https://dl.acm.org/doi/10.1145/3575693.3575729
Singh ALahav O(2023)An Operational Approach to Library Abstraction under Relaxed Memory ConcurrencyProceedings of the ACM on Programming Languages10.1145/35712467:POPL(1542-1572)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571246
Thokair MZhang MMathur UViswanathan M(2023)Dynamic Race Detection with O(1) SamplesProceedings of the ACM on Programming Languages10.1145/35712387:POPL(1308-1337)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571238
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

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

Media

Figures

Other

Tables

View Table of Contents