RacerX: effective, static detection of race conditions and deadlocks

ABSTRACT

This paper describes RacerX, a static tool that uses flow-sensitive, interprocedural analysis to detect both race conditions and deadlocks. It is explicitly designed to find errors in large, complex multithreaded systems. It aggressively infers checking information such as which locks protect which operations, which code contexts are multithreaded, and which shared accesses are dangerous. It tracks a set of code features which it uses to sort errors both from most to least severe. It uses novel techniques to counter the impact of analysis mistakes. The tool is fast, requiring between 2-14 minutes to analyze a 1.8 million line system. We have applied it to Linux, FreeBSD, and a large commercial code base, finding serious errors in all of them. RacerX is a static tool that uses flow-sensitive, interprocedural analysis to detect both race conditions and deadlocks. It uses novel strategies to infer checking information such as which locks protect which operations, which code contexts are multithreaded, and which shared accesses are dangerous. We applied it to FreeBSD, Linux and a large commercial code base and found serious errors in all of them.

REFERENCES

• 1: Chandrasekhar Boyapati , Robert Lee , Martin Rinard, Ownership types for safe programming: preventing data races and deadlocks, Proceedings of the 17th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, November 04-08, 2002, Seattle, Washington, USA
• 2: Willem Visser , Klaus Havelund , Guillaume Brat , SeungJoon Park, Model Checking Programs, Proceedings of the 15th IEEE international conference on Automated software engineering, p.3, September 11-15, 2000
• 3: M. Burrows and K. Leino. Finding stale-value errors in concurrent programs. Technical Report SRC-TN-2002-004, Compaq Systems Research Center, May 2002.
• 4: William R. Bush , Jonathan D. Pincus , David J. Sielaff, A static analyzer for finding dynamic programming errors, Software—Practice & Experience, v.30 n.7, p.775-802, June 2000 [doi>10.1002/(SICI)1097-024X(200006)30:7<775::AID-SPE309>3.0.CO;2-H]
• 5: Satish Chandra , Bradley Richards , James R. Larus, Teapot: A Domain-Specific Language for Writing Cache Coherence Protocols, IEEE Transactions on Software Engineering, v.25 n.3, p.317-333, May 1999 [doi>10.1109/32.798322]
• 6: Guang-Ien Cheng , Mingdong Feng , Charles E. Leiserson , Keith H. Randall , Andrew F. Stark, Detecting data races in Cilk programs that use locks, Proceedings of the tenth annual ACM symposium on Parallel algorithms and architectures, p.298-309, June 28-July 02, 1998, Puerto Vallarta, Mexico [doi>10.1145/277651.277696]
• 7: Jong-Deok Choi , Keunwoo Lee , Alexey Loginov , Robert O'Callahan , Vivek Sarkar , Manu Sridharan, Efficient and precise datarace detection for multithreaded object-oriented programs, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 8: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 9: James C. Corbett, Evaluating Deadlock Detection Methods for Concurrent Software, IEEE Transactions on Software Engineering, v.22 n.3, p.161-180, March 1996 [doi>10.1109/32.489078]
• 10: James C. Corbett , Matthew B. Dwyer , John Hatcliff , Shawn Laubach , Corina S. Păsăreanu , Robby , Hongjun Zheng, Bandera: extracting finite-state models from Java source code, Proceedings of the 22nd international conference on Software engineering, p.439-448, June 04-11, 2000, Limerick, Ireland [doi>10.1145/337180.337234]
• 11: Manuvir Das , Sorin Lerner , Mark Seigle, ESP: path-sensitive program verification in polynomial time, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 12: D. Detlefs, K. R. M. Leino, G. Nelson, and J. Saxe. Extended static checking. TR SRC-159, COMPAQ SRC, Dec. 1998.
• 13: A. Dinning , E. Schonberg, An empirical comparison of monitoring algorithms for access anomaly detection, Proceedings of the second ACM SIGPLAN symposium on Principles & practice of parallel programming, p.1-10, March 14-16, 1990, Seattle, Washington, United States
• 14: Dawson Engler , David Yu Chen , Seth Hallem , Andy Chou , Benjamin Chelf, Bugs as deviant behavior: a general approach to inferring errors in systems code, Proceedings of the eighteenth ACM symposium on Operating systems principles, October 21-24, 2001, Banff, Alberta, Canada
• 15: Cormac Flanagan , Stephen N. Freund, Type-based race detection for Java, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.219-232, June 18-21, 2000, Vancouver, British Columbia, Canada
• 16: Cormac Flanagan , K. Rustan M. Leino, Houdini, an Annotation Assistant for ESC/Java, Proceedings of the International Symposium of Formal Methods Europe on Formal Methods for Increasing Software Productivity, p.500-517, March 12-16, 2001
• 17: D. Freedman, R. Pisani, and R. Purves. Statistics. W.W. Norton, third edition edition, 1998.
• 18: James Gosling , Bill Joy , Guy Steele , Gilad Bracha, Java Language Specification, Second Edition: The Java Series, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2000
• 19: Dan Grossman, Type-safe multithreading in cyclone, Proceedings of the 2003 ACM SIGPLAN international workshop on Types in languages design and implementation, January 18-18, 2003, New Orleans, Louisiana, USA
• 20: Seth Hallem , Benjamin Chelf , Yichen Xie , Dawson Engler, A system and language for building system-specific, static analyses, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 21: D. P. Helmbold , C. E. McDowell, A TAXONOMY OF RACE DETECTION ALGORITHMS, University of California at Santa Cruz, Santa Cruz, CA, 1994
• 22: Leslie Lamport, Time, clocks, and the ordering of events in a distributed system, Communications of the ACM, v.21 n.7, p.558-565, July 1978 [doi>10.1145/359545.359563]
• 23: Butler W. Lampson , David D. Redell, Experience with processes and monitors in Mesa, Communications of the ACM, v.23 n.2, p.105-117, Feb. 1980 [doi>10.1145/358818.358824]
• 24: K. M. Leino, G. Nelson, and J. Saxe. ESC/Java user's manual. Technical note 2000-002, Compaq Systems Research Center, Oct. 2001.
• 25: John Mellor-Crummey, On-the-fly detection of data races for programs with nested fork-join parallelism, Proceedings of the 1991 ACM/IEEE conference on Supercomputing, p.24-33, November 18-22, 1991, Albuquerque, New Mexico, United States [doi>10.1145/125826.125861]
• 26: A. Morton. Personal communication. Semantics and deadlock implications of the Linux BKL, Feb. 2003.
• 27: Dejan Perkovic , Peter J. Keleher, Online data-race detection via coherency guarantees, Proceedings of the second USENIX symposium on Operating systems design and implementation, p.47-57, October 29-November 01, 1996, Seattle, Washington, United States
• 28: Thomas Reps , Susan Horwitz , Mooly Sagiv, Precise interprocedural dataflow analysis via graph reachability, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.49-61, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199462]
• 29: Stefan Savage , Michael Burrows , Greg Nelson , Patrick Sobalvarro , Thomas Anderson, Eraser: a dynamic data race detector for multithreaded programs, ACM Transactions on Computer Systems (TOCS), v.15 n.4, p.391-411, Nov. 1997 [doi>10.1145/265924.265927]
• 30: N. Sterling. Warlock: A static data race analysis tool. In Proceedings of the 1993 USENIX Winter Technical Conference, pages 97--106, 1993.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

Additional Classification:
  D. Software
  D.4 OPERATING SYSTEMS
      D.4.5 Reliability

General Terms:
Reliability, Verification

Keywords:
deadlock detection, program checking, race detection