Annotation-based modular checkers have the potential to perform scalable checking of system-specific properties. However, such tools have seldom been deployed on large software applications of industrial relevance. We present a case study of applying a modular checker \HAVOC to check properties about the synchronization protocol of a core Microsoft Windows component with more than 300,000 lines of code and 1500 procedures. The effort found 45 serious bugs in the component with modest annotation effort and low false alarms; most of these bugs have since been fixed by the developers of the module. We describe the challenges faced in using a modular checker for finding errors in a well-tested application of this scale, and our design decisions to find them with low false alarms, modest annotation burden and high coverage. We believe that the lessons learned from this exercise will enable annotation-based checkers to be more widely deployed and provide value beyond automated bug-finding tools based on traditional static analysis.

PDF file

Details