Re: Presberger arithmetic in compiler optimisation.

Christopher League <>
23 Nov 1999 13:02:43 -0500

          From comp.compilers

Related articles
Presberger arithmetic in compiler optimisation. (john green) (1999-11-23)
Re: Presberger arithmetic in compiler optimisation. (Christopher League) (1999-11-23)
Re: Presberger arithmetic in compiler optimisation. (1999-11-23)
Re: Presberger arithmetic in compiler optimisation. (Daniel G. Chavarria) (1999-11-23)
| List of all articles for this month |

From: Christopher League <>
Newsgroups: comp.compilers
Date: 23 Nov 1999 13:02:43 -0500
Organization: Yale University Computer Science
References: 99-11-130
Keywords: arithmetic, optimize, bibliography

* john green <> writes:
| In the literature I often see mention of applications [of Presberger
| arithmetic] in compiler optimisation, but have found little in the
| literature.

    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

Post a followup to this message

Return to the comp.compilers page.
Search the comp.compilers archives again.