Self-Adjusting Computation with Self-Adjusting SML

Compiler

The compiler is modified version of the MLton compiler.

Source package

• sa-mlton-20080512-1.src.tgz

Binary packages

• sa-mlton-20080512-1.amd64-linux.tgz, glibc 2.3
• sa-mlton-20080512-1.x86-cygwin.tgz, Cygwin 1.5.25-12
• sa-mlton-20080512-1.x86-darwin.gmp-macports.tgz (Mac OS X), dynamically linked against GnuMP in /opt/local/lib (suitable for MacPorts install of GnuMP)
• sa-mlton-20080512-1.x86-linux.tgz, glibc 2.3

Installation

Simply un-tar the binary package in a suitable installation location; your HOME directory or sub-directory thereof would be a good choice.

This will create a sa-mlton directory.

The compiler may be invoked via sa-mlton/bin/mlton.

Library and Examples

This package provides the self-adjusting library along with some sample applications.

See apps/dynamic/examples for some simple examples (also discussed in the lecture notes).

Source package

• src-release.tar.gz

Installation

Simply un-tar the binary package in a suitable installation location; your HOME directory or sub-directory thereof would be a good choice.

This will create a src-release directory.

To compile to an executable, use ~/sa-mlton/bin/mlton doit.mlb. To execute an executable, use ./doit.

Lectures

• AFP 2008

  You can download the lecture notes and slides.

  Please do not distribute.

Papers

• A Cost Semantics for Self-Adjusting Computation (Ruy Ley-Wild, Umut Acar, Matthew Fluet; To appear at POPL'09)

  Self-adjusting computation is an evaluation model in which programs can respond efficiently to small changes to their input data by using a change-propagation mechanism that updates computation by re-building only the parts affected by changes. Previous work has proposed language techniques for self-adjusting computation and showed the approach to be effective in a number of application areas. However, due to the complex semantics of change propagation and the indirect nature of previously proposed language techniques, it remains difficult to reason about the efficiency of self-adjusting programs and change propagation.

  In this paper, we propose a cost semantics for self-adjusting computation that enables reasoning about its effectiveness. As our source language, we consider a direct-style $\lambda$-calculus with first-class mutable references and develop a notion of trace distance for source programs. To facilitate asymptotic analysis, we propose techniques for composing and generalizing concrete distances via trace contexts (traces with holes). We then show how to translate the source language into a self-adjusting target language such that the translation (1) preserves the extensional semantics of the source programs and the cost of from-scratch runs, and (2) ensures that change propagation between two evaluations takes time bounded by their relative distance. We consider several examples and analyze their effectiveness by considering upper and lower bounds.

• Compiling Self–Adjusting Programs with Continuations (Ruy Ley-Wild, Matthew Fluet; Appeared at ICFP'08; icfp08-talk.pdf)

  Self-adjusting programs respond automatically and efficiently to input changes by tracking the dynamic data dependences of the computation and incrementally updating the output as needed. In order to identify data dependences, previously proposed approaches require the user to make use of a set of monadic primitives. Rewriting an ordinary program into a self-adjusting program with these primitives, however, can be difficult and error-prone due to various monadic and proper-usage restrictions, some of which cannot be enforced statically. Previous work therefore suggests that self-adjusting computation would benefit from direct language and compiler support.

  In this paper, we propose a language-based technique for writing and compiling self-adjusting programs from ordinary programs. To compile self-adjusting programs, we use a continuation-passing style (cps) transformation to automatically infer a conservative approximation of the dynamic data dependences. To prevent the inferred, approximate dependences from degrading the performance of change propagation, we generate memoized versions of cps functions that can reuse previous work even when they are invoked with different continuations. The approach offers a natural programming style that requires minimal changes to existing code, while statically enforcing the invariants required by self-adjusting computation.

  We validate the feasibility of our proposal by extending Standard ML and by integrating the transformation into MLton, a whole-program optimizing compiler for Standard ML. Our experiments indicate that the proposed compilation technique can produce self-adjusting programs whose performance is consistent with the asymptotic bounds and experimental results obtained via manual rewriting (up to a constant factor).