Validating Library Usage Interactively

Abstract

Programmers who develop large, mature applications often want to optimize the performance of their program without changing the semantics of the program. They often do so by changing how their program invokes a library function or a function provided by another module of the program. Unfortunately, once a programmer makes such an optimization, it is difficult for him to determine that the optimization does not change the semantics of the original program, because the orig- inal and optimized programs are equivalent only due to subtle, implicit assumptions about library functions called by the programs.

In this work, we present an interactive program analysis that a program- mer can apply to determine that his optimization does not change the behavior of a program. Our analysis casts the problem of validating an optimization as an abductive inference problem in the context of checking program equivalence. Our analysis solves the abductive equivalence prob- lem by interacting with the programmer so that the programmer imple- ments a solver for a logical theory that models library functions invoked by the program. We have used our analysis to validate optimizations from a set real-world, mature applications consisting of the Apache webserver, the Mozilla software suite, and the MySQL database.