[talks] B Guo preFPO

[Melissa M Lawson]

Bolei Guo will present her preFPO on Tuesday January 9 at 1PM in Room 402.
The members of her committee are; David August, advisor; Andrew Appel and 
Michael Hind (IBM TJ Watson), readers; Brian Kernighan and David Walker, 
nonreaders.  Everyone is invited to attend her talk.  Her abstract follows below.
-------------------------------------------
"Low-Level Shape Analysis with Inductive Recursion Synthesis"

Aggressive memory disambiguation for low-level code can eliminate the problem of
conservatively propagating high-level memory analysis results.  It critically affects the
effective-ness of back-end code optimizations.  In particular, automatic loop
parallelization relies on a type of memory analysis called shape analysis, which
determines the shapes of data structures built by the program.

We designed a separation-logic-based shape analysis for low-level code. 
  Separation logic with recursively defined predicates allows for concise yet precise
description of the shapes of data structures.  
However, inferring such predicates is a difficult task.  Current uses of separation logic
involve pre-defined built-in predicates and logic rules specificially written for these
predicates, limiting the class of analyzable programs.  We developed an inductive learning
technique to automatically infer arbitrary recursive shape predicates.  In addition, to
facilitate the interaction between local reasoning and the global invariants given by the
recursive predicates, a notion of "truncation points" is introduced in a predicate, which
gives rise to generic algorithms for unfolding and folding arbitrary data structures.
This shape analysis uses the alias information provided by a fast low-level pointer
analysis to identify recursive data structures and to prune away code that does not affect
the result of shape analysis.  It has been implemented in the Velocity compiler and
evaluated on benchmarks from the SPEC2000 and Olden benchmark suites.