Ruy Ley-Wild

Programmable Self-Adjusting Computation Degree Type: Ph.D. in Computer Science
Advisor(s): Guy Blelloch
Graduated: December 2010

Abstract:

Self-adjusting computation is a paradigm for programming incremental computations that efficiently respond to input changes by updating the output in time proportional to the changes in the structure of the computation. This dissertation defends the thesis that high-level programming abstractions improve the experience of reading, writing, and reasoning about and the efficiency of self-adjusting programs.

We show that high-level language constructs are suitable for writing readable self-adjusting programs and can be compiled into low-level primitives. In particular, language constructs such as ML-style modifiable references and memoizing functions provide orthogonal mechanisms for identifying stale computation to re-execute and opportunities for computation reuse. An adaptive continuation-passing style (ACPS) transformation compiles the high-level primitives into a continuation-passing language with explicit support for incrementality.

We show that a high-level cost semantics captures the performance of a self-adjusting program and a theory of trace distance suffices for formal reasoning about the efficiency of self-adjusting programs. The formal approach enables generalizing results from concrete runs to asymptotic bounds and compositional reasoning when combining self-adjusting programs.

We raise the level of abstraction for dependence-tracking from modifiable references to traceable data types, which can exploit problem-specific structure to identify stale computation. We consider in-order memoization that efficiently reuses work from previous runs in the same execution order and out-of-order memoization that allows previous work to be reordered at an additional expense.

The compilation approach is realized in the ΔML language, an extension to SML, and implemented as an extension to MLton with compiler and runtime support. Experimental evaluation of ΔML shows that applications with modifiable references are competitive with previous approaches. Moreover, traceable data types enable an asymptotic improvement in time and space usage relative to modifiable references.

Thesis Committee:
Guy Blelloch (Chair)
Stephen Brookes
Robert Harper
Umut Acar (Max-Planck Institute for Software Systems)

Jeannette Wing, Head, Computer Science Department
Randy Bryant, Dean, School of Computer Science

Keywords:
Self-adjusting computation, adaptivity, memoization, change-propagation, continuation-passing style, typed compilation, cost semantics, trace distance, traceable data type