This seminar series covers a range of topics in program
verification and related areas in programming languages and
compilers. Of particular interest is the verification of program
transformations and optimizations in modern compilers.
The next (and last) talk in the series will be:
Thursday, December 7 at 3pm
12th Floor Conference Room, 715 Broadway
Systematic and Powerful Program Optimization by Incrementalization
Y. Annie Liu
Computer Science Department
SUNY Stony Brook
Incremental computation takes advantage of repeated computations on
inputs that differ slightly from one another, computing each output
efficiently by exploiting the previous output. This talk gives an
overview of a general and systematic approach to incrementalization:
given a program f and an operation +, the approach yields an
incremental program that computes f(x+y) efficiently by using the
result of f(x), the intermediate results of f(x), and auxiliary
information of f(x) that can be inexpensively maintained. The
approach unifies existing incremental computation approaches and
exploits many program analysis and transformation techniques.
Since every nontrivial computation proceeds by iteration or recursion,
the approach can be used for achieving efficient computation by
computing each iteration incrementally using an appropriate
incremental program. Incrementalizing aggregate array computations in
loops yields new powerful optimizations that are fully automatable;
incrementalizing recursive equations allows dynamic programming
programs to be automatically derived; incrementalizing set expressions
underlies the finite differencing techniques studied by Paige et al.
These optimizations yield drastic performance improvements and form
the basis of a systematic method for program development, algorithm
design, and general problem solving.