[hofa] Abstracting Abstract Machines: Storing and stacking continuations

[David Van Horn]

I'd like to announce a couple new papers that might be of interest to 
HOFA readers.

We've been working on two techniques for systematically deriving 
abstract interpretations approximating canonical machines for 
higher-order languages. The first allocates continuations in a bounded 
store to achieve a finite state-space. We demonstrate the generality of 
this approach by transforming classical abstract machines into abstract 
interpreters.

     Abstracting Abstract Machines.
     David Van Horn and Matthew Might.
     The 15th ACM SIGPLAN International Conference on Functional
     Programming (ICFP’10), Baltimore, Maryland, September, 2010.

     We describe a derivational approach to abstract interpretation that
     yields novel and transparently sound static analyses when applied
     to well-established abstract machines. To demonstrate the technique
     and support our claim, we transform the CEK machine of Felleisen
     and Friedman, a lazy variant of Krivine's machine, and the stack-
     inspecting CM machine of Clements and Felleisen into abstract
     interpretations of themselves. The resulting analyses bound
     temporal ordering of program events; predict return-flow and stack-
     inspection behavior; and approximate the flow and evaluation of
     by-need parameters. For all of these machines, we find that a
     series of well-known concrete machine refactorings, plus a
     technique we call store-allocated continuations, leads to machines
     that abstract into static analyses simply by bounding their stores.
     We demonstrate that the technique scales up uniformly to allow
     static analysis of realistic language features, including tail
     calls, conditionals, side effects, exceptions, first-class
     continuations, and even garbage collection.

     http://www.ccs.neu.edu/home/dvanhorn/pubs/vanhorn-might-icfp10.pdf

The second technique keeps continuations on the stack to achieve a 
push-down model of abstract interpretation. The resulting abstract 
interpreter always matches calls and returns, achieving a higher level 
of precision by never conflating call and return pairs. Although this 
technique produces abstract interpreters with infinite state-spaces, we 
demonstrate how basic static analysis questions remain decidable by 
casting them as language inclusion problems answered by push-down automata.

     Pushdown Control-Flow Analysis of Higher-Order Programs.
     Christopher Earl, Matthew Might, and David Van Horn.
     The 2010 Workshop on Scheme and Functional Programming (SFP 2010),
     Montréal, Québec, Canada, August, 2010.

     Context-free approaches to static analysis gain precision over
     classical approaches by perfectly matching returns to call sites--
     a property that eliminates spurious interprocedural paths.
     Vardoulakis and Shivers's recent formulation of CFA2 showed that it
     is possible (if expensive) to apply context-free methods to
     higher-order languages and gain the same boost in precision
     achieved over first-order programs.

     To this young body of work on context-free analysis of higher-order
     programs, we contribute a pushdown control-flow analysis framework,
     which we derive as an abstract interpretation of a CESK machine
     with an unbounded stack. One instantiation of this framework marks
     the first polyvariant pushdown analysis of higher-order programs;
     another marks the first polynomial-time analysis. In the end, we a
     arrive at a framework for control-flow analysis that can
     efficiently compute pushdown generalizations of classical
     control-flow analyses.

     http://www.ccs.neu.edu/home/dvanhorn/pubs/earl-might-vanhorn-sfp10.pdf

There are also some slides available from a Harvard PL seminar talk:

 
http://www.ccs.neu.edu/home/dvanhorn/talks/abstracting-abstract-machines-harvard-2010.pdf

Thanks,
David, Matt, Chris