A Functional Perspective on SSA Optimisation Algorithms

The static single assignment (SSA) form is central to a range of optimisation algorithms relying on data flow information, and hence, to the correctness of compilers employing those algorithms. It is well known that the SSA form is closely related to lambda terms (i.e., functional programs) and, considering the large amount of energy expended on theories and frameworks for formal reasoning in the lambda calculus, it seems only natural to leverage this connection to improve our capabilities to reason about compiler optimisations. In this paper, we discuss a new formalisation of the mapping from SSA programs to a restricted form of lambda terms, called administrative normal form (ANF). We conjecture that this connection improves our ability to reason about SSA-based optimisation algorithms and provide a first data point by presenting an ANF variant of a well known SSA-based conditional constant propagation algorithm.

You can obtain the final version of the paper from Elsevier Science. Alternatively, I've made the final draft available free of charge at the following address:

http://www.jantar.org/papers/chakravarty03perspective.pdf

The slides from my presentation at the 2003 COCV workshop in Warsaw are also available here:

http://www.jantar.org/talks/zadarnowski03perspective.pdf

If you'd like to cite my work in your publication, please use the following BibTeX entry:

@inproceedings{chakravarty03perspective,
    author = {Chakravarty, Manuel M. T. and
              Keller, Gabriele and Zadarnowski, Patryk},
    title = {A Functional Perspective on SSA Optimisation Algorithms},
    booktitle = {COCV '03: Compiler Optimization Meets Compiler Verification},
    series = {Electronic Notes in Theoretical Computer Science},
    editor = {Knoop, Jens and Zimmermann, Wolf},
    year = {2003},
    month = {April},
    location = {Warsaw, Poland},
    volume = {82},
    issue = {2},
    pages = {347--361},
    publisher = {Elsevier Science},
 }

Last but not least, the source code for the ANF tookit referenced in the paper can be downloaded from:

http://www.jantar.org/ssa-lambda/lab.tar.gz

The tarball contains Haskell 98 source code for all algorithms described in the technical report. It includes a parser for a concrete syntax of the ANF and SSA forms, an interpreter implementing the operational semantics for both and the SSA-to-ANF translator. To compile the tookit, you will need a recent version of the Glasgow Haskell Compiler running on a UNIX machine. You should also be able to run the tookit using Hugs, but you're on your own there.

Please see the sample.anf and sample.ssa files for examples of the concrete syntax supported by the parser. To compile the toolkit, extract it and run make in the lab directory. This will create a binary lab which you can use as follows:

usage: lab -a [ANF source file...]
       lab -s [SSA source file...]
       lab -t SSA source file
       lab source file

The first two forms of invocation (lab -a and lab -s) evaluate an ANF and SSA expression from the standard input, respectively. Any source files supplied on the command-line will be loaded into the program as a “library” of primitives in addition to the standard add, sub, mul, div and rem. lab -t reads an SSA source file and prints the corresponding ANF program on the standard output. Finally, running lab without any command-line flags will parse and evaluate the supplied source file, which must have an .anf or .ssa suffix for ANF and SSA, respectively. If you need more help with the tookit, please contact me.