research-article

BiRD: Race Detection in Software Binaries under Relaxed Memory Models

Authors:
Ridhi Jain

Indraprastha Institute of Information Technology Delhi, New Delhi, India

Indraprastha Institute of Information Technology Delhi, New Delhi, India

0000-0002-6102-7114
View Profile

,
Rahul Purandare

Indraprastha Institute of Information Technology Delhi, New Delhi, India

Indraprastha Institute of Information Technology Delhi, New Delhi, India
View Profile

,
Subodh Sharma

Indian Institute of Technology Delhi, New Delhi, India

Indian Institute of Technology Delhi, New Delhi, India
View Profile

ACM Transactions on Software Engineering and Methodology Volume 31 Issue 4Article No.: 58pp 1–29https://doi.org/10.1145/3498538

Published:12 July 2022Publication History

ACM Transactions on Software Engineering and Methodology

Abstract

Instruction reordering and interleavings in program execution under relaxed memory semantics result in non-intuitive behaviors, making it difficult to provide assurances about program correctness. Studies have shown that up to 90% of the concurrency bugs reported by state-of-the-art static analyzers are false alarms. As a result, filtering false alarms and detecting real concurrency bugs is a challenging problem. Unsurprisingly, this problem has attracted the interest of the research community over the past few decades. Nonetheless, many of the existing techniques rely on analyzing source code, rarely consider the effects introduced by compilers, and assume a sequentially consistent memory model. In a practical setting, however, developers often do not have access to the source code, and even commodity architectures such as x86 and ARM are not sequentially consistent.

In this work, we present Bird, a prototype tool, to dynamically detect harmful data races in x86 binaries under relaxed memory models, TSO and PSO. Bird employs source-DPOR to explore all distinct feasible interleavings for a multithreaded application. Our evaluation of Bird on 42 publicly available benchmarks and its comparison with the state-of-the-art tools indicate Bird’s potential in effectively detecting data races in software binaries.

REFERENCES

[1] ETAPS 2019. COMP 2019—8th International Competition on Software Verification. Retrieved February 19, 2022 from https://sv-comp.sosy-lab.org/2019/.Google Scholar
[2] Abadi Martin, Flanagan Cormac, and Freund Stephen N.. 2006. Types for safe locking: Static race detection for Java. ACM Transactions on Programming Languages and Systems 28, 2 (2006), 207–255.Google ScholarDigital Library
[3] Abdulla Parosh, Aronis Stavros, Jonsson Bengt, and Sagonas Konstantinos. 2014. Optimal dynamic partial order reduction. ACM SIGPLAN Notices 49, 1 (2014), 373–384.Google ScholarDigital Library
[4] Abdulla Parosh Aziz, Aronis Stavros, Atig Mohamed Faouzi, Jonsson Bengt, Leonardsson Carl, and Sagonas Konstantinos. 2017. Stateless model checking for TSO and PSO. Acta Informatica 54, 8 (2017), 789–818.Google ScholarDigital Library
[5] Abdulla Parosh Aziz, Aronis Stavros, Jonsson Bengt, and Sagonas Konstantinos. 2017. Source sets: A foundation for optimal dynamic partial order reduction. Journal of the ACM 64, 4 (Aug. 2017), Article 25, 49 pages. Google ScholarDigital Library
[6] Abdulla Parosh Aziz, Aronis Stavros, Jonsson Bengt, and Sagonas Konstantinos. 2017. Source sets: A foundation for optimal dynamic partial order reduction. Journal of the ACM 64, 4 (2017), 25.Google ScholarDigital Library
[7] Abdulla Parosh Aziz, Arora Jatin, Atig Mohamed Faouzi, and Krishna Shankaranarayanan. 2019. Verification of programs under the release-acquire semantics. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’19). ACM, New York, NY, 1117–1132. Google ScholarDigital Library
[8] Albert Elvira, Arenas Puri, Banda María García de la, Gómez-Zamalloa Miguel, and Stuckey Peter J.. 2017. Context-sensitive dynamic partial order reduction. In Computer Aided Verification, Majumdar Rupak and Kunčak Viktor (Eds.). Springer International, Cham, Switzerland, 526–543.Google Scholar
[9] Alglave Jade, Kroening Daniel, Nimal Vincent, and Tautschnig Michael. 2013. Software verification for weak memory via program transformation. In Proceedings of the European Symposium on Programming. 512–532.Google ScholarDigital Library
[10] Alglave Jade, Maranget Luc, Sarkar Susmit, and Sewell Peter. 2011. Litmus: Running tests against hardware. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 41–44.Google ScholarCross Ref
[11] Alrabaee Saed, Wang Lingyu, and Debbabi Mourad. 2016. BinGold: Towards robust binary analysis by extracting the semantics of binary code as semantic flow graphs (SFGs). Digital Investigation 18 (2016), S11–S22.Google ScholarDigital Library
[12] Andriesse Dennis. 2018. Practical Binary Analysis: Build Your Own Linux Tools for Binary Instrumentation, Analysis, and Disassembly. No Starch Press.Google Scholar
[13] Atzeni Simone, Gopalakrishnan Ganesh, Rakamaric Zvonimir, Ahn Dong H., Laguna Ignacio, Schulz Martin, Lee Gregory L., Protze Joachim, and Müller Matthias S.. 2016. ARCHER: Effectively spotting data races in large OpenMP applications. In Proceedings of the 2016 IEEE International Parallel and Distributed Processing Symposium (IPDPS’16). IEEE, Los Alamitos, CA, 53–62.Google ScholarCross Ref
[14] Banerjee Utpal, Bliss Brian, Ma Zhiqiang, and Petersen Paul. 2006. Unraveling data race detection in the Intel thread checker. In Proceedings of the 1st Workshop on Software Tools for MultiCore Systems (STMCS’06).Google Scholar
[15] Batty Mark, Owens Scott, Sarkar Susmit, Sewell Peter, and Weber Tjark. 2011. Mathematizing C++ concurrency. In Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’11). ACM, New York, NY, 55–66. Google ScholarDigital Library
[16] Blum Ben and Gibson Garth. 2016. Stateless model checking with data-race preemption points. ACM SIGPLAN Notices 51, 10 (Oct. 2016), 477–493. Google ScholarDigital Library
[17] Burnim Jabob, Sen Koushik, and Stergiou Christos. 2011. Sound and complete monitoring of sequential consistency for relaxed memory models. In Tools and Algorithms for the Construction and Analysis of Systems, Abdulla Parosh Aziz and Leino K. Rustan M. (Eds.). Springer, Berlin, Germany, 11–25.Google ScholarCross Ref
[18] Burrows Michael and Leino Rustan. 2004. Finding stale-value errors in concurrent programs. Concurrency and Computation: Practice and Experience 16, 12 (2004), 1161–1172.Google ScholarDigital Library
[19] Choi Jong-Deok and Min Sang Lyul. 1991. Race Frontier: Reproducing data races in parallel-program debugging. ACM SIGPLAN Notices 26, 7 (1991), 145–154.Google ScholarDigital Library
[20] Chugh Ravi, Voung Jan W., Jhala Ranjit, and Lerner Sorin. 2008. Dataflow analysis for concurrent programs using datarace detection. In Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’08). ACM, New York, NY, 316–326. Google ScholarDigital Library
[21] Edelstein Orit, Farchi Eitan, Goldin Evgeny, Nir Yarden, Ratsaby Gil, and Ur Shmuel. 2003. Framework for testing multi-threaded Java programs. Concurrency and Computation: Practice and Experience 15, 3–5 (2003), 485–499.Google ScholarCross Ref
[22] Effinger-Dean Laura, Lucia Brandon, Ceze Luis, Grossman Dan, and Boehm Hans-J.. 2012. IFRit: Interference-free regions for dynamic data-race detection. ACM SIGPLAN Notices 47 (2012), 467–484.Google Scholar
[23] Eizenberg Ariel, Peng Yuanfeng, Pigli Toma, Mansky William, and Devietti Joseph. 2017. BARRACUDA: Binary-level analysis of runtime RAces in CUDA programs. In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’17). ACM, New York, NY, 126–140. Google ScholarDigital Library
[24] Elmas Tayfun, Qadeer Shaz, and Tasiran Serdar. 2007. Goldilocks: A race and transaction-aware Java runtime. ACM SIGPLAN Notices 42 (2007), 245–255.Google Scholar
[25] Elver M. and Nagarajan V.. 2014. TSO-CC: Consistency directed cache coherence for TSO. In Proceedings of the 2014 IEEE 20th International Symposium on High Performance Computer Architecture (HPCA’14). 165–176. Google ScholarCross Ref
[26] Flanagan Cormac and Freund Stephen N.. 2009. FastTrack: Efficient and precise dynamic race detection. ACM SIGPLAN Notices 44 (2009), 121–133.Google Scholar
[27] Flanagan Cormac and Godefroid Patrice. 2005. Dynamic partial-order reduction for model checking software. ACM SIGPLAN Notices 40, 1 (Jan. 2005), 110–121. Google ScholarDigital Library
[28] Godefroid Patrice. 1990. Using partial orders to improve automatic verification methods. In Proceedings of the International Conference on Computer Aided Verification. 176–185.Google Scholar
[29] Godefroid Patrice and Nagappan Nachiappan. 2008. Concurrency at Microsoft: An exploratory survey. In Proceedings of the CAV Workshop on Exploiting Concurrency Efficiently and Correctly.Google Scholar
[30] Godefroid Patrice, Leeuwen Jan van, Hartmanis Juris, Goos Gerhard, and Wolper Pierre. 1996. Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem, Vol. 1032. Springer, Heidelberg, Germany.Google ScholarCross Ref
[31] Grossman Dan. 2003. Type-safe multithreading in cyclone. ACM SIGPLAN Notices 38 (2003), 13–25.Google Scholar
[32] Han Kyoung Soo, Kang Boojoong, and Im Eul Gyu. 2011. Malware classification using instruction frequencies. In Proceedings of the 2011 ACM Symposium on Research in Applied Computation. 298–300.Google ScholarDigital Library
[33] Hartung Marc. n.d. DataRaceBenchmark: Concurrency Benchmarks. Retrieved February 19, 2022 from https://github.com/marchartung/DataRaceBenchmark/; https://github.com/marchartung/DataRaceBenchmark/find/master.Google Scholar
[34] Hartung Marc, Schintke Florian, and Schütt Thorsten. 2019. Pinpoint data races via testing and classification. In Proceedings of the 2019 IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW’19). IEEE, Los Alamitos, CA, 386–393.Google ScholarCross Ref
[35] Huang Jeff, Meredith Patrick O’Neil, and Rosu Grigore. 2014. Maximal sound predictive race detection with control flow abstraction. In Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’14). ACM, New York, NY, 337–348. Google ScholarDigital Library
[36] Huang Jeff and Zhang Charles. 2011. Persuasive prediction of concurrency access anomalies. In Proceedings of the 2011 International Symposium on Software Testing and Analysis. ACM, New York, NY, 144–154.Google ScholarDigital Library
[37] Huang Shiyou and Huang Jeff. 2016. Maximal causality reduction for TSO and PSO. ACM SIGPLAN Notices 51, 10 (2016), 447–461.Google ScholarDigital Library
[38] Jahić Jasmin, Kumar Varun, Jung Matthias, Wirrer Gerhard, Wehn Norbert, and Kuhn Thomas. 2019. Rapid identification of shared memory in multithreaded embedded systems with static scheduling. In Proceedings of the 48th International Conference on Parallel Processing: Workshops (ICPP’19). ACM, New York, NY, Article 15, 8 pages. Google ScholarDigital Library
[39] Jeong Dae R., Kim Kyungtae, Shivakumar Basavesh, Lee Byoungyoung, and Shin Insik. 2019. Razzer: Finding kernel race bugs through fuzzing. In Proceedings of the 2019 IEEE Symposium on Security and Privacy (SP’19). IEEE, Los Alamitos, CA, 754–768.Google ScholarCross Ref
[40] Kahlon Vineet, Gupta Aarti, and Sinha Nishant. 2006. Symbolic model checking of concurrent programs using partial orders and on-the-fly transactions. In Computer Aided Verification, Ball Thomas and Jones Robert B. (Eds.). Springer, Berlin, Germany, 286–299.Google Scholar
[41] Kahlon Vineet, Sinha Nishant, Kruus Erik, and Zhang Yun. 2009. Static data race detection for concurrent programs with asynchronous calls. In Proceedings of the 7th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE’09). ACM, New York, NY, 13–22. Google ScholarDigital Library
[42] Kahlon Vineet, Yang Yu, Sankaranarayanan Sriram, and Gupta Aarti. 2007. Fast and accurate static data-race detection for concurrent programs. In Proceedings of the International Conference on Computer Aided Verification. 226–239.Google ScholarCross Ref
[43] Kasikci Baris, Zamfir Cristian, and Candea George. 2012. Data races vs. data race bugs: Telling the difference with portend. ACM SIGPLAN Notices 47, 4 (2012), 185–198.Google ScholarDigital Library
[44] Kim K., Yavuz-Kahveci T., and Sanders B. A.. 2009. Precise data race detection in a relaxed memory model using heuristic-based model checking. In Proceedings of the 2009 IEEE/ACM International Conference on Automated Software Engineering. 495–499.Google ScholarDigital Library
[45] Kokologiannakis Michalis, Lahav Ori, Sagonas Konstantinos, and Vafeiadis Viktor. 2018. Effective stateless model checking for C/C++ concurrency. Proceedings of the ACM on Programming Languages 2, POPL (2018), Article 17, 32 pages. Google ScholarDigital Library
[46] Kokologiannakis Michalis, Raad Azalea, and Vafeiadis Viktor. 2019. Model checking for weakly consistent libraries. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’19). ACM, New York, NY, 96–110. Google ScholarDigital Library
[47] Kokologiannakis Michalis and Vafeiadis Viktor. 2020. HMC: Model checking for hardware memory models. In Proceedings of the 25th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS’20). ACM, New York, NY, 1157–1171. Google ScholarDigital Library
[48] Koval Nikita, Sokolova Maria, Fedorov Alexander, Alistarh Dan, and Tsitelov Dmitry. 2020. Testing concurrency on the JVM with Lincheck. In Proceedings of the 25th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP’20). ACM, New York, NY, 423–424. Google ScholarDigital Library
[49] Lahav Ori, Giannarakis Nick, and Vafeiadis Viktor. 2016. Taming release-acquire consistency. ACM SIGPLAN Notices 51, 1 (Jan. 2016), 649–662. Google ScholarDigital Library
[50] Lahav Ori and Margalit Roy. 2019. Robustness against release/acquire semantics. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’19). ACM, New York, NY, 126–141. Google ScholarDigital Library
[51] Lamport Leslie. 2019. Time, clocks, and the ordering of events in a distributed system. In Concurrency: The Works of Leslie Lamport, Dahlia Malkhi (Ed). ACM Books, New York, NY, 179–196.Google Scholar
[52] Lidbury Christopher and Donaldson Alastair F.. 2017. Dynamic race detection for C++ 11. ACM SIGPLAN Notices 52, 1 (2017), 443–457.Google ScholarDigital Library
[53] Lidbury Christopher and Donaldson Alastair F.. 2017. Dynamic race detection for C++11. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL’17). ACM, New York, NY, 443–457. Google ScholarDigital Library
[54] Luk Chi-Keung, Cohn Robert, Muth Robert, Patil Harish, Klauser Artur, Lowney Geoff, Wallace Steven, Reddi Vijay Janapa, and Hazelwood Kim. 2005. Pin: Building customized program analysis tools with dynamic instrumentation. ACM SIGPLAN Notices 40 (2005), 190–200.Google Scholar
[55] Luo Weiyu and Demsky Brian. 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.Google ScholarDigital Library
[56] Mazurkiewicz Antoni W.. 1987. Trace theory. In Proceedings of an Advanced Course on Petri Nets: Central Models and Their Properties, Advances in Petri Nets 1986—Part II. Springer-Verlag, Berlin, Germany, 279–324. http://dl.acm.org/citation.cfm?id=647422.725772.Google ScholarCross Ref
[57] McAllester David A.. 1993. Partial order backtracking. Journal of Artificial Intelligence Research 1 (1993), 17–24.Google Scholar
[58] Group Imperial College London Multicore. n.d. SCTBench: C/C++ Pthread Benchmarks. Retrieved February 19, 2022 from https://github.com/mc-imperial/sctbench.Google Scholar
[59] Muzahid Abdullah, Otsuki Norimasa, and Torrellas Josep. 2010. AtomTracker: A comprehensive approach to atomic region inference and violation detection. In Proceedings of the 2010 43rd Annual IEEE/ACM International Symposium on Microarchitecture. IEEE, Los Alamitos, CA, 287–297.Google ScholarDigital Library
[60] Naik Mayur, Aiken Alex, and Whaley John. 2006. Effective static race detection for Java. In Proceedings of the 27th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’06). ACM, New York, NY, 308–319. Google ScholarDigital Library
[61] Narayanasamy Satish, Wang Zhenghao, Tigani Jordan, Edwards Andrew, and Calder Brad. 2007. Automatically classifying benign and harmful data races using replay analysis. ACM SIGPLAN Notices 42 (2007), 22–31.Google Scholar
[62] Norris Brian and Demsky Brian. 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 and Applications (OOPSLA’13). ACM, New York, NY, 131–150. Google ScholarDigital Library
[63] O’Callahan Robert and Choi Jong-Deok. 2003. Hybrid dynamic data race detection. In Proceedings of the 9th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP’03). ACM, New York, NY, 167–178. Google ScholarDigital Library
[64] Park Sangmin, Vuduc Richard W., and Harrold Mary Jean. 2010. Falcon: Fault localization in concurrent programs. In Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering—Volume 1. ACM, New York, NY, 245–254.Google ScholarDigital Library
[65] Pavlogiannis Andreas. 2019. Fast, sound, and effectively complete dynamic race prediction. Proceedings of the ACM on Programming Languages 4, POPL (2019), 1–29.Google ScholarDigital Library
[66] Peled Doron. 2018. Partial-Order Reduction. Springer International, Cham, Switzerland, 173–190. Google ScholarCross Ref
[67] Peled Doron, Valmari Antti, and Kokkarinen Ilkka. 2001. Relaxed visibility enhances partial order reduction. Formal Methods in System Design 19, 3 (2001), 275–289.Google ScholarDigital Library
[68] Perdisci Roberto, Lanzi Andrea, and Lee Wenke. 2008. McBoost: Boosting scalability in malware collection and analysis using statistical classification of executables. In Proceedings of the 2008 Annual Computer Security Applications Conference (ACSAC’08). IEEE, Los Alamitos, CA, 301–310.Google ScholarDigital Library
[69] Pozzetti Tommaso and Kshemkalyani Ajay D.. 2020. Resettable encoded vector clock for causality analysis with an application to dynamic race detection. IEEE Transactions on Parallel and Distributed Systems 32, 4 (2020), 772–785.Google ScholarDigital Library
[70] Pulte Christopher, Flur Shaked, Deacon Will, French Jon, Sarkar Susmit, and Sewell Peter. 2017. Simplifying ARM concurrency: Multicopy-atomic axiomatic and operational models for ARMv8. Proceedings of the ACM on Programming Languages 2, POPL (Dec. 2017), Article 19, 29 pages. Google ScholarDigital Library
[71] Roemer Jake, Genç Kaan, and Bond Michael D.. 2020. SmartTrack: Efficient predictive race detection. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’20). ACM, New York, NY, 747–762. Google ScholarDigital Library
[72] Sadowski Caitlin and Yi Jaeheon. 2014. How developers use data race detection tools. In Proceedings of the 5th Workshop on Evaluation and Usability of Programming Languages and Tools. 43–51.Google ScholarDigital Library
[73] Santos Igor, Brezo Felix, Nieves Javier, Penya Yoseba K., Sanz Borja, Laorden Carlos, and Bringas Pablo G.. 2010. Idea: Opcode-sequence-based malware detection. In Proceedings of the International Symposium on Engineering Secure Software and Systems. 35–43.Google ScholarDigital Library
[74] Savage Stefan, Burrows Michael, Nelson Greg, Sobalvarro Patrick, and Anderson Thomas. 1997. Eraser: A dynamic data race detector for multithreaded programs. ACM Transactions on Computer Systems 15, 4 (Nov. 1997), 391–411. Google ScholarDigital Library
[75] Shacham Ohad, Sagiv Mooly, and Schuster Assaf. 2005. Scaling model checking of dataraces using dynamic information. In Proceedings of the 10th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP’05). ACM, New York, NY, 107–118. Google ScholarDigital Library
[76] Sharma Divyanjali and Sharma Subodh. n.d. Thread-modular analysis of release-acquire concurrency. arXiv preprint arXiv:2107.02346 [accepted in SAS’21] (n.d.).Google Scholar
[77] Sheng Tianwei, Vachharajani Neil, Eranian Stephane, Hundt Robert, Chen Wenguang, and Zheng Weimin. 2011. RACEZ: A lightweight and non-invasive race detection tool for production applications. In Proceedings of the 2011 33rd International Conference on Software Engineering (ICSE’11). IEEE, Los Alamitos, CA, 401–410.Google ScholarDigital Library
[78] Shoshitaishvili Yan, Wang Ruoyu, Salls Christopher, Stephens Nick, Polino Mario, Dutcher Andrew, Grosen John, et al. 2016. SOK: (State of) the art of war: Offensive techniques in binary analysis. In Proceedings of the 2016 IEEE Symposium on Security and Privacy (SP’16). IEEE, Los Alamitos, CA, 138–157.Google ScholarCross Ref
[79] Smaragdakis Yannis, Evans Jacob, Sadowski Caitlin, Yi Jaeheon, and Flanagan Cormac. 2012. Sound predictive race detection in polynomial time. ACM SIGPLAN Notices 47 (2012), 387–400.Google Scholar
[80] Sterling Nicholas. 1993. WARLOCK—A static data race analysis tool. In Proceedings of the USENIX Winter 1993 Conference. 97–106.Google Scholar
[81] Tassarotti Joseph, Dreyer Derek, and Vafeiadis Viktor. 2015. Verifying read-copy-update in a logic for weak memory. ACM SIGPLAN Notices 50, 6 (2015), 110–120.Google ScholarDigital Library
[82] Tice Caroline, Roeder Tom, Collingbourne Peter, Checkoway Stephen, Erlingsson Úlfar, Lozano Luis, and Pike Geoff. 2014. Enforcing forward-edge control-flow integrity in GCC and LLVM. In Proceedings of the 23rd USENIX Security Symposium (USENIX’14). 941–955.Google Scholar
[83] Trippel Caroline, Manerkar Yatin A., Lustig Daniel, Pellauer Michael, and Martonosi Margaret. 2017. TriCheck: Memory model verification at the trisection of software, hardware, and ISA. ACM SIGPLAN Notices 52, 4 (April 2017), 119–133. Google ScholarDigital Library
[84] Valmari Antti. 1996. The state explosion problem. In Advanced Course on Petri Nets. Springer, 429–528.Google Scholar
[85] Veeraraghavan Kaushik, Chen Peter M., Flinn Jason, and Narayanasamy Satish. 2011. Detecting and surviving data races using complementary schedules. In Proceedings of the 23rd ACM Symposium on Operating Systems Principles. 369–384.Google ScholarDigital Library
[86] Voung Jan Wen, Jhala Ranjit, and Lerner Sorin. 2007. RELAY: Static race detection on millions of lines of code. In Proceedings of the the 6th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC-FSE’07). ACM, New York, NY, 205–214. Google ScholarDigital Library
[87] Wang Chao, Yang Zijiang, Kahlon Vineet, and Gupta Aarti. 2008. Peephole partial order reduction. In Tools and Algorithms for the Construction and Analysis of Systems, Ramakrishnan C. R. and Rehof Jakob (Eds.). Springer, Berlin, Germany, 382–396.Google ScholarCross Ref
[88] Wester Benjamin, Devecsery David, Chen Peter M., Flinn Jason, and Narayanasamy Satish. 2013. Parallelizing data race detection. ACM SIGPLAN Notices 48, 4 (March 2013), 27–38. Google ScholarDigital Library
[89] Wichmann Arne. 2012. Binary Analysis for Code Reconstruction of Control Software. Diploma Thesis. Hamburg University of Technology.Google Scholar
[90] Wilcox James R., Flanagan Cormac, and Freund Stephen N.. 2018. VerifiedFT: A verified, high-performance precise dynamic race detector. In Proceedings of the 23rd ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming. ACM, New York, NY, 354–367.Google ScholarDigital Library
[91] Yang Yu, Chen Xiaofang, and Gopalakrishnan Ganesh. 2008. Inspect: A Runtime Model Checker for Multithreaded C Programs. Technical Report UUCS-08-004. University of Utah.Google Scholar
[92] Yang Yu, Chen Xiaofang, Gopalakrishnan Ganesh, and Kirby Robert M.. 2008. Efficient stateful dynamic partial order reduction. In Model Checking Software, Havelund Klaus, Majumdar Rupak, and Palsberg Jens (Eds.). Springer, Berlin, Germany.Google Scholar
[93] Yu Jie, Narayanasamy Satish, Pereira Cristiano, and Pokam Gilles. 2012. Maple: A coverage-driven testing tool for multithreaded programs. ACM SIGPLAN Notices 47 (2012), 485–502.Google Scholar
[94] Yu Yuan, Rodeheffer Tom, and Chen Wei. 2005. RaceTrack: Efficient detection of data race conditions via adaptive tracking. In Proceedings of the 20th ACM Symposium on Operating Systems Principles (SOSP’05). ACM, New York, NY, 221–234. Google ScholarDigital Library
[95] Yun Heecul. n.d. DPthread—Deterministic Pthread Benchmarks. Retrieved February 19, 2022 from https://github.com/heechul/dpthread.Google Scholar
[96] Zhang Naling, Kusano Markus, and Wang Chao. 2015. Dynamic partial order reduction for relaxed memory models. ACM SIGPLAN Notices 50 (2015), 250–259.Google Scholar
[97] Zhang Tong, Jung Changhee, and Lee Dongyoon. 2017. ProRace: Practical data race detection for production use. ACM SIGPLAN Notices 52, 4 (2017), 149–162.Google ScholarDigital Library

Index Terms

BiRD: Race Detection in Software Binaries under Relaxed Memory Models
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation

Recommendations

Verification of STM on relaxed memory models

Software transactional memories (STM) are described in the literature with assumptions of sequentially consistent program execution and atomicity of high level operations like read, write, and abort. However, in a realistic setting, processors use ...
Read More
Testing concurrent programs on relaxed memory models
ISSTA '11: Proceedings of the 2011 International Symposium on Software Testing and Analysis

High-performance concurrent libraries, such as lock-free data structures and custom synchronization primitives, are notoriously difficult to write correctly. Such code is often implemented without locks, instead using plain loads and stores and low-...
Read More
Verifying dynamic race detection
CPP 2017: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs

Writing race-free concurrent code is notoriously difficult, and data races can result in bugs that are difficult to isolate and reproduce. Dynamic race detection can catch data races that cannot (easily) be detected statically. One approach to dynamic ...
Read More

Comments

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

Published in
ACM Transactions on Software Engineering and Methodology Volume 31, Issue 4
October 2022
867 pages
ISSN:1049-331X
EISSN:1557-7392
DOI:10.1145/3543992
Editor:
Mauro Pezzè
USI Università della Svizzera italiana and SIT Schaffhausen Institute of Technology, Switzerland
Issue’s Table of Contents
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].
Sponsors
In-Cooperation
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
- Published: 12 July 2022
- Online AM: 31 January 2022
- Accepted: 1 November 2021
- Revised: 1 September 2021
- Received: 1 March 2021
Published in tosem Volume 31, Issue 4

Permissions
Request permissions about this article.
Request Permissions

Check for updates
Author Tags
Relaxed memory models
TSO and PSO
dynamic race detection
software binaries
Qualifiers
- research-article
- Refereed
Conference
Funding Sources
Other Metrics
View Article Metrics

Article Metrics
- 1
  Total Citations
  View Citations
- 594
  Total Downloads
- Downloads (Last 12 months)111
- Downloads (Last 6 weeks)10
Other Metrics
View Author Metrics
Cited By
View all

PDF Format

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Full Text

View this article in Full Text.

View Full Text

HTML Format

View this article in HTML Format .

View HTML Format

BiRD: Race Detection in Software Binaries under Relaxed Memory Models

ACM Transactions on Software Engineering and Methodology

Abstract

REFERENCES

Cited By

Index Terms

Recommendations

Verification of STM on relaxed memory models

Testing concurrent programs on relaxed memory models

Verifying dynamic race detection