
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.
participants (1)
-
Melissa M Lawson