|Presberger arithmetic in compiler optimisation. email@example.com (john green) (1999-11-23)|
|Re: Presberger arithmetic in compiler optimisation. firstname.lastname@example.org (Christopher League) (1999-11-23)|
|Re: Presberger arithmetic in compiler optimisation. email@example.com (1999-11-23)|
|Re: Presberger arithmetic in compiler optimisation. firstname.lastname@example.org (Daniel G. Chavarria) (1999-11-23)|
|From:||Christopher League <email@example.com>|
|Date:||23 Nov 1999 13:02:43 -0500|
|Organization:||Yale University Computer Science|
|Keywords:||arithmetic, optimize, bibliography|
* john green <firstname.lastname@example.org> writes:
| In the literature I often see mention of applications [of Presberger
| arithmetic] in compiler optimisation, but have found little in the
Here is one reference and project URL, you can probably start there
and track down other references...
William Pugh. Counting Solutions to Presburger Formulas: How and
Why. University of Maryland Department of Computer Science
CS-TR-3234. Also in PLDI'94.
We describe methods that are able to count the number of integer
solutions to selected free variables of a Presburger formula, or
sum a polynomial over all integer solutions of selected free
variables of a Presburger formula. This answer is given
symbolically, in terms of symbolic constants (the remaining free
variables in the Presburger formula).
For example, we can create a Presburger formula whose solutions
correspond to the iterations of a loop. By counting these, we
obtain an estimate of the execution time of the loop.
In more complicated applications, we can create Presburger
formulas who's solutions correspond to the distinct memory
locations or cache lines touched by a loop, the flops executed by
a loop, or the array elements that need to be communicated at a
particular point in a distributed computation. By counting the
number of solutions, we can evaluate the computation/memory
balance of a computation, determine if a loop is load balanced and
evaluate message traffic and allocate message buffers.
Christopher League Yale University Computer Science
Return to the
Search the comp.compilers archives again.