Cited By
View all- Ang ZMathur U(2024)Predictive Monitoring with Strong Trace PrefixesComputer Aided Verification10.1007/978-3-031-65630-9_9(182-204)Online publication date: 24-Jul-2024
Optimistic Prediction of Synchronization-Reversal Data Races
Article No.: 134, Pages 1 - 13
Abstract
Dynamic data race detection has emerged as a key technique for ensuring reliability of concurrent software in practice. However, dynamic approaches can often miss data races owing to non-determinism in the thread scheduler. Predictive race detection techniques cater to this shortcoming by inferring alternate executions that may expose data races without re-executing the underlying program. More formally, the dynamic data race prediction problem asks, given a trace σ of an execution of a concurrent program, can σ be correctly reordered to expose a data race? Existing state-of-the art techniques for data race prediction either do not scale to executions arising from real world concurrent software, or only expose a limited class of data races, such as those that can be exposed without reversing the order of synchronization operations.
In general, exposing data races by reasoning about synchronization reversals is an intractable problem. In this work, we identify a class of data races, called Optimistic Sync(hronization)-Reversal races that can be detected in a tractable manner and often include non-trivial data races that cannot be exposed by prior tractable techniques. We also propose a sound algorithm OSR for detecting all optimistic sync-reversal data races in overall quadratic time, and show that the algorithm is optimal by establishing a matching lower bound. Our experiments demonstrate the effectiveness of OSR--- on our extensive suite of benchmarks, OSR reports the largest number of data races, and scales well to large execution traces.
References
[1]
[n. d.]. ECP Proxy Applications. https://proxyapps.exascaleproject.org/. Accessed: 2021-08-01.
[2]
[n. d.]. Mantevo Project. https://mantevo.org/. Accessed: 2021-08-01.
[3]
[n. d.]. RaceInjector traces. https://github.com/ALFA-group/RaceInjector-counterexamples/tree/main. Accessed: 2023-07-14.
[4]
[n. d.]. RAPID. https://github.com/umangm/rapid. Accessed: 2023-07-06.
[5]
2014. CORAL Benchmarks. Accessed: 2021-08-01.
[6]
2014. CORAL2 Benchmarks. Accessed: 2021-08-01.
[7]
2023. Range Minima Query Solutions. https://en.wikipedia.org/wiki/Range_minimum_query. Accessed: 2023-07-18.
[8]
2024. OSR implementation. https://zenodo.org/records/10437347. Accessed: 2024-01-11.
[9]
2024. OSR technical report. https://arxiv.org/abs/2401.05642. Accessed: 2024-01-12.
[10]
Parosh Abdulla, Stavros Aronis, Bengt Jonsson, and Konstantinos Sagonas. 2014. Optimal Dynamic Partial Order Reduction. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (San Diego, California, USA) (POPL '14). Association for Computing Machinery, New York, NY, USA, 373--384.
[11]
Udit Agarwal, Pantazis Deligiannis, Cheng Huang, Kumseok Jung, Akash Lal, Immad Naseer, Matthew Parkinson, Arun Thangamani, Jyothi Vedurada, and Yunpeng Xiao. 2021. Nekara: Generalized Concurrency Testing. In 2021 36th IEEE/ACM International Conference on Automated Software Engineering (ASE). 679--691.
[12]
Zhendong Ang and Umang Mathur. 2024. Predictive Monitoring against Pattern Regular Languages. Proc. ACM Program. Lang. 8, POPL, Article 73 (jan 2024).
[13]
David H Bailey, Eric Barszcz, John T Barton, David S Browning, Robert L Carter, Leonardo Dagum, Rod A Fatoohi, Paul O Frederickson, Thomas A Lasinski, Rob S Schreiber, et al. 1991. The NAS parallel benchmarks---summary and preliminary results. In Proceedings of the 1991 ACM/IEEE Conference on Supercomputing. 158--165.
[14]
RICHARD BELLMAN. 1958. ON A ROUTING PROBLEM. Quart. Appl. Math. 16, 1 (1958), 87--90. http://www.jstor.org/stable/43634538
[15]
Stephen M Blackburn, Robin Garner, Chris Hoffmann, Asjad M Khang, Kathryn S McKinley, Rotem Bentzur, Amer Diwan, Daniel Feinberg, Daniel Frampton, Samuel Z Guyer, et al. 2006. The DaCapo benchmarks: Java benchmarking development and analysis. In Proceedings of the 21st annual ACM SIGPLAN conference on Object-oriented programming systems, languages, and applications. 169--190.
[16]
Sam Blackshear, Nikos Gorogiannis, Peter W O'Hearn, and Ilya Sergey. 2018. RacerD: compositional static race detection. Proceedings of the ACM on Programming Languages 2, OOPSLA (2018), 1--28.
[17]
Hans-J Boehm. 2012. Position paper: Nondeterminism is unavoidable, but data races are pure evil. In Proceedings of the 2012 ACM workshop on Relaxing synchronization for multicore and manycore scalability. 9--14.
[18]
Michael D. Bond, Katherine E. Coons, and Kathryn S. McKinley. 2010. PACER: Proportional Detection of Data Races. In Proceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation (Toronto, Ontario, Canada) (PLDI '10). Association for Computing Machinery, New York, NY, USA, 255--268.
[19]
Sebastian Burckhardt, Pravesh Kothari, Madanlal Musuvathi, and Santosh Nagarakatte. 2010. A randomized scheduler with probabilistic guarantees of finding bugs. ACM SIGARCH Computer Architecture News 38, 1 (2010), 167--178.
[20]
Yan Cai, Hao Yun, Jinqiu Wang, Lei Qiao, and Jens Palsberg. 2021. Sound and efficient concurrency bug prediction. In Proceedings of the 29th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering. 255--267.
[21]
Milind Chabbi and Murali Krishna Ramanathan. 2022. A Study of Real-World Data Races in Golang. In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation (San Diego, CA, USA) (PLDI 2022). Association for Computing Machinery, New York, NY, USA, 474--489.
[22]
Lijie Chen and Ryan Williams. 2019. An equivalence class for orthogonal vectors. In Proceedings of the Thirtieth Annual ACM-SIAM Symposium on Discrete Algorithms. SIAM, 21--40.
[23]
Pantazis Deligiannis, Aditya Senthilnathan, Fahad Nayyar, Chris Lovett, and Akash Lal. 2023. Industrial-Strength Controlled Concurrency Testing for C# Programs with COYOTE. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 433--452.
[24]
Hyunsook Do, Sebastian Elbaum, and Gregg Rothermel. 2005. Supporting controlled experimentation with testing techniques: An infrastructure and its potential impact. Empirical Software Engineering 10 (2005), 405--435.
[25]
Antonio J Dorta, Casiano Rodriguez, and Francisco de Sande. 2005. The OpenMP source code repository. In 13th Euromicro Conference on Parallel, Distributed and Network-Based Processing. IEEE, 244--250.
[26]
Eitan Farchi, Yarden Nir, and Shmuel Ur. 2003. Concurrent bug patterns and how to test them. In Proceedings international parallel and distributed processing symposium. IEEE, 7--pp.
[27]
Azadeh Farzan and Umang Mathur. 2024. Coarser Equivalences for Causal Concurrency. Proc. ACM Program. Lang. 8, POPL, Article 31 (jan 2024).
[28]
Cormac Flanagan and Stephen N. Freund. 2009. FastTrack: Efficient and Precise Dynamic Race Detection. In Proceedings of the 30th ACM SIGPLAN Conference on Programming Language Design and Implementation (Dublin, Ireland) (PLDI '09). Association for Computing Machinery, New York, NY, USA, 121--133.
[29]
Lester Randolph Ford. 1956. Network flow theory. (1956).
[30]
Harold N Gabow, Jon Louis Bentley, and Robert E Tarjan. 1984. Scaling and related techniques for geometry problems. In Proceedings of the sixteenth annual ACM symposium on Theory of computing. 135--143.
[31]
Kaan Genç, Jake Roemer, Yufan Xu, and Michael D Bond. 2019. Dependence-aware, unbounded sound predictive race detection. Proceedings of the ACM on Programming Languages 3, OOPSLA (2019), 1--30.
[32]
Patrice Godefroid. 2005. Software model checking: The VeriSoft approach. Formal Methods in System Design 26 (2005), 77--101.
[33]
Jeff Huang, Patrick O'Neil Meredith, and Grigore Rosu. 2014. Maximal sound predictive race detection with control flow abstraction. In Proceedings of the 35th ACM SIGPLAN conference on programming language design and implementation. 337--348.
[34]
Dae R Jeong, Kyungtae Kim, Basavesh Shivakumar, Byoungyoung Lee, and Insik Shin. 2019. Razzer: Finding kernel race bugs through fuzzing. In 2019 IEEE Symposium on Security and Privacy (SP). IEEE, 754--768.
[35]
Christian Gram Kalhauge and Jens Palsberg. 2018. Sound Deadlock Prediction. Proc. ACM Program. Lang. 2, OOPSLA, Article 146 (oct 2018), 29 pages.
[36]
Dileep Kini, Umang Mathur, and Mahesh Viswanathan. 2017. Dynamic Race Prediction in Linear Time. In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (Barcelona, Spain) (PLDI 2017). Association for Computing Machinery, New York, NY, USA, 157--170.
[37]
Michalis Kokologiannakis and Viktor Vafeiadis. 2021. GenMC: A model checker for weak memory models. In International Conference on Computer Aided Verification. Springer, 427--440.
[38]
Rucha Kulkarni, Umang Mathur, and Andreas Pavlogiannis. 2021. Dynamic Data-Race Detection Through the Fine-Grained Lens. In 32nd International Conference on Concurrency Theory.
[39]
Leslie Lamport. 1978. Time, Clocks, and the Ordering of Events in a Distributed System. Commun. ACM 21, 7 (jul 1978), 558--565.
[40]
Yanze Li, Bozhen Liu, and Jeff Huang. 2019. Sword: A scalable whole program race detector for java. In 2019 IEEE/ACM 41st International Conference on Software Engineering: Companion Proceedings (ICSE-Companion). IEEE, 75--78.
[41]
Chunhua Liao, Pei-Hung Lin, Joshua Asplund, Markus Schordan, and Ian Karlin. 2017. DataRaceBench: a benchmark suite for systematic evaluation of data race detection tools. In Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis. 1--14.
[42]
Weiyu Luo and Brian Demsky. 2021. C11Tester: a race detector for C/C++ atomics. In Proceedings of the 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems. 630--646.
[43]
Daniel Marino, Madanlal Musuvathi, and Satish Narayanasamy. 2009. LiteRace: Effective sampling for lightweight data-race detection. In Proceedings of the 30th ACM SIGPLAN Conference on Programming Language Design and Implementation. 134--143.
[44]
Umang Mathur, Dileep Kini, and Mahesh Viswanathan. 2018. What happens-after the first race? enhancing the predictive power of happens-before based dynamic race detection. Proceedings of the ACM on Programming Languages 2, OOPSLA (2018), 1--29.
[45]
Umang Mathur, Andreas Pavlogiannis, Hünkar Can Tunç, and Mahesh Viswanathan. 2022. A Tree Clock Data Structure for Causal Orderings in Concurrent Executions. In Proceedings of the 27th ACM International Conference on Architectural Support for Programming Languages and Operating Systems. ACM, Lausanne Switzerland, 710--725.
[46]
Umang Mathur, Andreas Pavlogiannis, and Mahesh Viswanathan. 2020. The complexity of dynamic data race prediction. In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science. 713--727.
[47]
Umang Mathur, Andreas Pavlogiannis, and Mahesh Viswanathan. 2021. Optimal prediction of synchronization-preserving races. Proceedings of the ACM on Programming Languages 5, POPL (2021), 1--29.
[48]
Umang Mathur and Mahesh Viswanathan. 2020. Atomicity Checking in Linear Time Using Vector Clocks. In Proceedings of the Twenty-Fifth International Conference on Architectural Support for Programming Languages and Operating Systems (Lausanne, Switzerland) (ASPLOS '20). Association for Computing Machinery, New York, NY, USA, 183--199.
[49]
Patrick Meredith and Grigore Roşu. 2010. Runtime verification with the RV system. In International Conference on Runtime Verification. Springer, 136--152.
[50]
Edward F. Moore. 1959. The shortest path through a maze. In Proc. Internat. Sympos. Switching Theory 1957, Part II. Harvard Univ. Press, Cambridge, Mass., 285--292.
[51]
Arndt Müehlenfeld and Franz Wotawa. 2007. Fault Detection in Multi-threaded C++ Server Applications. In Proceedings of the 12th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (San Jose, California, USA) (PPoPP '07). ACM, New York, NY, USA, 142--143.
[52]
Suvam Mukherjee, Pantazis Deligiannis, Arpita Biswas, and Akash Lal. 2020. Learning-based controlled concurrency testing. Proceedings of the ACM on Programming Languages 4, OOPSLA (2020), 1--31.
[53]
Mayur Naik, Alex Aiken, and John Whaley. 2006. Effective static race detection for Java. In Proceedings of the 27th ACM SIGPLAN Conference on Programming Language Design and Implementation. 308--319.
[54]
Brian Norris and Brian Demsky. 2013. CDSchecker: Checking Concurrent Data Structures Written with C/C++ Atomics. In Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications (Indianapolis, Indiana, USA) (OOPSLA '13). Association for Computing Machinery, New York, NY, USA, 131--150.
[55]
Jonas Oberhauser, Rafael Lourenco de Lima Chehab, Diogo Behrens, Ming Fu, Antonio Paolillo, Lilith Oberhauser, Koustubha Bhat, Yuzhong Wen, Haibo Chen, Jaeho Kim, et al. 2021. VSync: push-button verification and optimization for synchronization primitives on weak memory models. In Proceedings of the 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems. 530--545.
[56]
Andreas Pavlogiannis. 2019. Fast, sound, and effectively complete dynamic race prediction. Proceedings of the ACM on Programming Languages 4, POPL (2019), 1--29.
[57]
Eli Pozniansky and Assaf Schuster. 2003. Efficient on-the-fly data race detection in multithreaded C++ programs. In Proceedings of the ninth ACM SIGPLAN symposium on Principles and practice of parallel programming. 179--190.
[58]
Jake Roemer, Kaan Genç, and Michael D Bond. 2020. SmartTrack: efficient predictive race detection. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation. 747--762.
[59]
Jake Roemer, Kaan Genç, and Michael D. Bond. 2018. High-Coverage, Unbounded Sound Predictive Race Detection. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation (Philadelphia, PA, USA) (PLDI 2018). Association for Computing Machinery, New York, NY, USA, 374--389.
[60]
Jake Roemer, Kaan Genç, and Michael D. Bond. 2018. High-Coverage, Unbounded Sound Predictive Race Detection. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation (Philadelphia, PA, USA) (PLDI 2018). Association for Computing Machinery, New York, NY, USA, 374--389.
[61]
Caitlin Sadowski and Jaeheon Yi. 2014. How Developers Use Data Race Detection Tools. In Proceedings of the 5th Workshop on Evaluation and Usability of Programming Languages and Tools (Portland, Oregon, USA) (PLATEAU '14). Association for Computing Machinery, New York, NY, USA, 43--51.
[62]
Mahmoud Said, Chao Wang, Zijiang Yang, and Karem Sakallah. 2011. Generating data race witnesses by an SMT-based analysis. In NASA Formal Methods Symposium. Springer, 313--327.
[63]
Stefan Savage, Michael Burrows, Greg Nelson, Patrick Sobalvarro, and Thomas Anderson. 1997. Eraser: A dynamic data race detector for multithreaded programs. ACM Transactions on Computer Systems (TOCS) 15, 4 (1997), 391--411.
[64]
Adrian Schmitz, Joachim Protze, Lechen Yu, Simon Schwitanski, and Matthias S Müller. 2019. DataRaceOnAccelerator-a micro-benchmark suite for evaluating correctness tools targeting accelerators. In European Conference on Parallel Processing. Springer, 245--257.
[65]
Koushik Sen, Grigore Roşu, and Gul Agha. 2005. Detecting errors in multithreaded programs by generalized predictive analysis of executions. In Formal Methods for Open Object-Based Distributed Systems: 7th IFIP WG 6.1 International Conference, FMOODS 2005, Athens, Greece, June 15--17, 2005. Proceedings 7. Springer, 211--226.
[66]
Konstantin Serebryany and Timur Iskhodzhanov. 2009. ThreadSanitizer: data race detection in practice. In Proceedings of the workshop on binary instrumentation and applications. 62--71.
[67]
Yannis Smaragdakis, Jacob Evans, Caitlin Sadowski, Jaeheon Yi, and Cormac Flanagan. 2012. Sound Predictive Race Detection in Polynomial Time. In Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Philadelphia, PA, USA) (POPL '12). Association for Computing Machinery, New York, NY, USA, 387--400.
[68]
Francesco Sorrentino, Azadeh Farzan, and P. Madhusudan. 2010. PENELOPE: Weaving Threads to Expose Atomicity Violations. In Proceedings of the Eighteenth ACM SIGSOFT International Symposium on Foundations of Software Engineering (Santa Fe, New Mexico, USA) (FSE '10). Association for Computing Machinery, New York, NY, USA, 37--46.
[69]
Mosaad Al Thokair, Minjian Zhang, Umang Mathur, and Mahesh Viswanathan. 2023. Dynamic Race Detection with O (1) Samples. Proceedings of the ACM on Programming Languages 7, POPL (2023), 1308--1337.
[70]
Hünkar Can Tunç, Umang Mathur, Andreas Pavlogiannis, and Mahesh Viswanathan. 2023. Sound Dynamic Deadlock Prediction in Linear Time. Proc. ACM Program. Lang. 7, PLDI, Article 177 (jun 2023), 26 pages.
[71]
Michael Wang, Shashank Srikant, Malavika Samak, and Una-May O'Reilly. 2023. RaceInjector: Injecting Races to Evaluate and Learn Dynamic Race Detection Algorithms. In Proceedings of the 12th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis. 63--70.
[72]
Ryan Williams. 2005. A new algorithm for optimal 2-constraint satisfaction and its implications. Theoretical Computer Science 348, 2 (2005), 357--365. Automata, Languages and Programming: Algorithms and Complexity (ICALP-A 2004).
[73]
Meng Xu, Sanidhya Kashyap, Hanqing Zhao, and Taesoo Kim. 2020. Krace: Data race fuzzing for kernel file systems. In 2020 IEEE Symposium on Security and Privacy (SP). IEEE, 1643--1660.
[74]
Xinhao Yuan, Junfeng Yang, and Ronghui Gu. 2018. Partial order aware concurrency sampling. In Computer Aided Verification: 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14--17, 2018, Proceedings, Part II 30. Springer, 317--335.
[75]
Sheng Zhan and Jeff Huang. 2016. ECHO: instantaneous in situ race detection in the IDE. In Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering. 775--786.
Recommendations
Optimal prediction of synchronization-preserving races
Concurrent programs are notoriously hard to write correctly, as scheduling nondeterminism introduces subtle errors that are both hard to detect and to reproduce. The most common concurrency errors are (data) races, which occur when memory-conflicting ...
Efficiently Trigger Data Races through Speculative Execution
HPCC-CSS-ICESS '15: Proceedings of the 2015 IEEE 17th International Conference on High Performance Computing and Communications, 2015 IEEE 7th International Symposium on Cyberspace Safety and Security, and 2015 IEEE 12th International Conf on Embedded Software and SystemsHarmful data races hidden in concurrent programs are hard to be detected due to non-determinism. Many race detectors report a large number of benign data races. To detect the harmful data races automatically, previous tools dynamically execute program ...
Healing data races on-the-fly
PADTAD '07: Proceedings of the 2007 ACM workshop on Parallel and distributed systems: testing and debuggingTesting of concurrent software is extremely difficult. Despite all the progress in the testing and verification technology, concurrent bugs, the most common of which are deadlocks and races, make it to the field. This paper describes a set of techniques,...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
May 2024
2942 pages
ISBN:9798400702174
DOI:10.1145/3597503
- Co-chairs:
- Ana Paiva,
- Rui Abreu,
- Program Co-chairs:
- Abhik Roychoudhury,
- Margaret Storey
This work is licensed under a Creative Commons Attribution International 4.0 License.
Sponsors
In-Cooperation
- Faculty of Engineering of University of Porto
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 12 April 2024
Check for updates
Badges
Qualifiers
- Research-article
Funding Sources
- National Cybersecurity R&D Programme
- Villum Fonden
- National Research Foundation Singapore
Conference
ICSE '24
Sponsor:
ICSE '24: IEEE/ACM 46th International Conference on Software Engineering
April 14 - 20, 2024
Lisbon, Portugal
Acceptance Rates
Overall Acceptance Rate 276 of 1,856 submissions, 15%
Upcoming Conference
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 153Total Downloads
- Downloads (Last 12 months)153
- Downloads (Last 6 weeks)31
Reflects downloads up to 28 Sep 2024
Other Metrics
Citations
Cited By
View all- Ang ZMathur U(2024)Predictive Monitoring with Strong Trace PrefixesComputer Aided Verification10.1007/978-3-031-65630-9_9(182-204)Online publication date: 24-Jul-2024
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.
Sign in