Preventing bugs, and improving code quality with Microsoft SAL (Part 1, Prologue)
You’re using an invalid handle!
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!
A slide from “Unleashing the Power of Static Analysis“, by Manuvir Das, of the Microsoft Center for Software Excellence
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.
A slide from “Driver Annotations in Depth, Part I“, by Donn Terry.
Design Rule Checking is a term that you may recognize from the from the world of Electronic Design Automation, where Printed Circuit Boards are required to be within certain specifications for manufacturability.
Proper annotation can catch this in static analysis.
A slide from “Driver Annotations in Depth, Part 2“, by Donn Terry
See: Driver Annotations in Depth, Part 1, and Driver Annotations in Depth, Part 2
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:
SAL’s modern Infrastructure
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.
Further reading:
Alexander Riccio 