Validating Library Usage Interactively
Date
2013-01-28Author
Jha, Somesh
Lu, Shan
Jin, Guoliang
Harris, William R.
Metadata
Show full item recordAbstract
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.
Subject
program optimization
program equivalence
abductive reasoning
Permanent Link
http://digital.library.wisc.edu/1793/64921Citation
TR1782
Part of
Licensed under: