Haverford College Computer Science

I am continuing my investigation of the behavior of the algorithms I used in my Ph.D. thesis. I developed algorithms for new forms of analysis of calculations involving arrays, including dataflow analysis and analysis of dependence conditions. My algorithms involved the generation of various Presburger Formulas, and the testing of these formulas for satisfiability (which appears to have complexity 2^2^2^O(n)). However, my dissertation included algorithms that are efficient for the cases that arise in practice.

In the late 90's, I performed detailed empirical studies of the behavior of the algorithms I use for simplification of Presburger Formulas. I identified several characteristics that lead to quick solution, rather than exponential blowup, for the formulas that arise during analysis of typical (benchmark) programs. These characteristics, as well as the algorithms and experimental system, are described in the paper (gzipped) that appeared in the May '98 issue of ACM Transactions on Programming Languages and Systems.

More recently, Rob Seater (HC '02) and I developed a formal description of a subdomain of Presburger Arithmetic that can be manipulated in polynomial time, and which includes almost all of the affine formulas involved in analysis of loop-carried dataflow. This work is described in our paper "Polynomial Time Array Dataflow Analysis" at LCPC '01. We went on to develop efficient algorithms for a domain that includes a wider variety of "disequality" constraints: See "Efficient Manipulation of Disequalities During Dependence Analysis" (published at LCPC '02) for details. I started this investigation at DIMACS (where I spent part of my junior leave); Vince Gabor (HC '99) worked with me during the preliminary investigation.

Page maintained by John Dougherty, David Wonnacott, and Rachel Heaton.
Computer Science Department, Haverford College.