Preventing bugs, and improving code quality with Microsoft SAL (Part 1, Prologue)
Microsoft’s SAL started nearly ten years ago at Microsoft as part of a major push for code quality, and (more visibly) preventing bugchecks. In its earliest versions, it appears to have been effectively restricted to the Windows core codebase, with kernel-mode-driver developers following suit. “Unleashing the Power of Static Analysis” says that here it helped developers fix more than twenty thousands bugs in Windows Vista, and more than 6,500 bugs in Microsoft Office 12. Of these, they found one buffer overrun per twenty annotations!
Kernel-mode-driver developers have access to a much larger set of annotations, as they have much greater sensitivity to complex conditions and small bugs. Chances are, that as PC user, you’ve seen at least one blue screen that has a cryptic error message like “IRQL_NOT_LESS_OR_EQUAL”, which means roughly that a driver tried to read memory when it shouldn’t have.
Proper annotation can catch this in static analysis.
In “Engineering Better Software at Microsoft“, Jason Yang gives examples of ‘common-sense’ properties and behaviors, as implemented in “SAL-speak”:
In another slide, he shows some concurrency annotations, which I’ve found invaluable:
But most importantly, SAL has matured to become part of an even larger ecosystem:
Personally I place great emphasis on static analysis, and think others place too much emphasis on testing as a means of bug prevention. My philosophy is that if you find bugs during testing, then you’re doing something terribly wrong. “Testing” should mean “validation“, whereby we’re pretty damned sure that everything is right. Partly, this is because we can never expect to exercise all possible conditions in testing; it’s kind of silly to try, like attempting to prove Fermat’s Last Theorem, as Prof. John Conway describes it beginning at 7:30, by testing all possible numbers – it’s never going to work.
Coming up in Part 2: using SAL to detect invalid usage of already-closed handles.