Locksmith is a static analysis tool for automatically detecting data races in C programs. In this paper, we describe each of Locksmith's component analyses precisely, and present systematic measurements that isolate interesting tradeoffs between precision and efficiency in each analysis. Using a benchmark suite comprising standalone applications and Linux device drivers totaling more than 200,000 lines of code, we found that a simple no-worklist strategy yielded the most efficient interprocedural dataflow analysis; that our sharing analysis was able to determine that most locations are thread-local, and therefore need not be protected by locks; that modeling C structs and void pointers precisely is key to both precision and efficiency; and that context-sensitivity yields a much more precise analysis, though with decreased scalability. Put together, our results illuminate some of the key engineering challenges in building Locksmith and data race detection analyses in particular, and constraint-based program analyses in general.

[ .pdf ]

@article{pratikakis11locksmith,
  title = {Locksmith: Practical Static Race Detection for {C}},
  author = {Polyvios Pratikakis and Jeffrey S. Foster and Michael Hicks},
  journal = {{ACM} Transactions on Programming Languages and Systems (TOPLAS)},
  month = jan,
  year = 2011,
  volume = {33},
  number = 1,
  pages = {Article 3}
}

This file was generated by bibtex2html 1.99.