RacerX

RacerX: Effective, static detection of race conditions and deadlocks. 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.

This software is also peer reviewed by journal TOMS.


References in zbMATH (referenced in 12 articles )

Showing results 1 to 12 of 12.
Sorted by year (citations)

  1. Chatterjee, Krishnendu; De Alfaro, Luca; Faella, Marco; Majumdar, Rupak; Raman, Vishwanath: Code aware resource management (2013)
  2. Lafortune, Stéphane; Wang, Yin; Reveliotis, Spyros: Eliminating concurrency bugs in multithreaded software: an approach based on control of Petri nets (2013)
  3. Liao, Hongwei; Wang, Yin; Cho, Hyoun Kyu; Stanley, Jason; Kelly, Terence; Lafortune, Stéphane; Mahlke, Scott; Reveliotis, Spyros: Concurrency bugs in multithreaded software: modeling and analysis using Petri nets (2013)
  4. Pun, Ka I.; Steffen, Martin; Stolz, Volker: Deadlock checking by a behavioral effect system for lock handling (2012)
  5. Chiu, Yung-Chang; Shieh, Ce-Kuen; Huang, Tzu-Chi; Liang, Tyng-Yeu; Chu, Kuo-Chih: Data race avoidance and replay scheme for developing and debugging parallel programs on distributed shared memory systems (2011)
  6. Donaldson, Alastair F.; Haller, Leopold; Kroening, Daniel: Strengthening induction-based race checking with lightweight static analysis (2011)
  7. Donaldson, Alastair F.; Kroening, Daniel; Rümmer, Philipp: Automatic analysis of DMA races using model checking and $k$-induction (2011)
  8. Demeyer, Romain: Program analysis to support concurrent programming in declarative languages (2010)
  9. Kim, Moonzoo; Hong, Shin; Hong, Changki; Kim, Taeho: Model-based kernel testing for concurrency bugs through counter example replay (2009)
  10. Regehr, John; Cooprider, Nathan: Interrupt verification via thread verification. (2007)
  11. Sidiroglou, Stelios; Keromytis, Angelos D.: Execution transactions for defending against software failures: use and evaluation (2006)
  12. Sidiroglou, Stelios; Keromytis, Angelos D.: Execution transactions for defending against software failures: use and evaluation (2006)