Today's general-purpose dynamic superscalar processors use large on-chip regular structures, such as the register file and caches, in order to exploit the available instruction-level parallelism and improve performance. These structures are often designed in order to maximize the performance of the average application. There is, however, a trade-off between the size of these structures and their speed and power consumption. The best design may differ on a per application and even a per phase basis.
Explicitly stated program invariants can help programmers by characterizing
certain aspects of program execution and identifying program properties
that must be preserved when modifying code. In practice, these invariants
are usually absent from code. An alternative to expecting programmers to
annotate code with invariants is to automatically infer invariants from the
program itself.
This talk has three parts. The first part gives background about dynamic
invariant detection, a technique for discovering invariants from execution
traces. The essential idea is to look for patterns in and relationships
among variable values over a set of executions. An implementation has
indicated that the approach is both effective -- successfully rediscovering
formal specifications -- and useful -- discovering invariants that assisted
software evolution tasks.
The second part of the talk describes an application of program invariants
to the task of refactoring. Program refactoring -- transforming a program
to improve readability, structure, performance, abstraction,
maintainability, or other features -- is not applied in practice as much as
might be desired. One deterrent is the cost of detecting candidates for
refactoring and of choosing the appropriate refactoring transformation.
This paper demonstrates the feasibility of automatically finding places in
the program that are candidates for specific refactorings. The approach
uses program invariants: when a particular pattern of invariant
relationships appears at a program point, a specific refactoring is
applicable. We applied this technique to an 8000-line Java program, and
its maintainer assessed the detected refactorings. This work will appear
in ICSM'01.
The third part of the talk shows how to integrate two complementary
techniques for manipulating program invariants: dynamic detection and
static verification. Dynamic detection proposes likely invariants based on
program executions, but the resulting properties are not guaranteed to be
true over all possible executions. Static verification checks that
properties are always true, but it can be difficult and tedious to select a
goal and to annotate programs for input to a static checker. Combining
these techniques overcomes the weaknesses of each: dynamically detected
invariants can annotate a program or provide goals for static verification,
and static verification can confirm properties proposed by a dynamic tool.
Our experiments suggest that dynamic analyses may be remarkably accurate:
the dynamically detected invariants had an average precision (a measure of
correctness) of .95 and an average recall (a measure of completeness) of
.94. This work appeared in RV'01.
About Michael Ernst
Michael D. Ernst is an assistant professor in the MIT Lab for Computer
Science. He received the Ph.D. in Computer Science and Engineering from
the University of Washington and has previously been a lecturer at Rice
University and a researcher at Microsoft Research. Ernst's primary
technical interest is programmer productivity, encompassing software
engineering, program analysis, compilation, and programming language
design. However, he has also published in artificial intelligence, theory,
and other areas of computer science.
![[RiceCS]](http://www.cs.rice.edu/Database/media/CSLogo.gif){kind=small}
![[Rice]](http://www.cs.rice.edu/Database/media/Owl.gif){kind=small}
