Writing a well-functioning computer program is an exercise in following rules. Complying with the rules is made much easier when a program can verify its own compliance. This is why we write assertions: they express the rules we wish a program to follow in a way that allows the program to verify its compliance.
But assertions are limited to a particular kind of rule: the rule must be parameterized only by the data the program has at hand. Assertions work wonderfully for “don’t divide by zero,” but they struggle with “don’t read from an uninitialized object” or “don’t write past the end of an array,” and fail entirely with “don’t destroy an object twice” or “don’t write to an object from which another thread might be reading.” The information needed to verify compliance with these rules is simply not available.
So let’s make it available! Let’s try writing extra declarations into programs, and recording the information needed to verify compliance with all the rules. This is, of course, what sanitizers attempt to do. But for compatibility, sanitizers rely on a great deal of guesswork, particularly about objects accessed from more than one translation unit. By providing extra declarations, we can make our intent clear and take the guesswork out of verifying code.
These new declarations form a bookkeeping system for our program. By keeping balanced books, we can detect imminent violations of our programming rules, and head off much undefined behavior before it happens. In this lecture, I will explore the details of this bookkeeping system.
View Slides
Lisa Lippincott designed the software architectures of Tanium and BigFix, two systems for managing large fleets of computers. She's currently assistant chair of the numerics study group of the C++ standardization committee. In her spare time, she studies mathematical logic, and wants to make computer-checked proofs of correctness a routine part of programming.