Sumit Gulwani and George C. Necula

EECS Department
University of California, Berkeley
Technical Report No. UCB/CSD-03-1296
November 2003

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2003/CSD-03-1296.pdf

We present a polynomial time randomized algorithm for global value numbering. Our algorithm is complete when conditionals are treated as non-deterministic and all operators are treated as uninterpreted functions. We are not aware of any complete polynomial-time deterministic algorithm for the same problem. The algorithm does not require symbolic manipulations and hence is simpler to implement than the deterministic symbolic algorithms. The price for these benefits is that there is a probability that the algorithm can report a false equality. We prove that this probability can be made arbitrarily small by controlling various parameters of the algorithm.

Our algorithm is based on the idea of random interpretation, which relies on executing a program on a number of random inputs and discovering relationships from the computed values. The computations are done by giving random linear interpretations to the operators in the program. Both branches of a conditional are executed. At join points, the program states are combined using a random affine combination. We discuss ways in which this algorithm can be made more precise by using more accurate interpretations for the linear arithmetic operators and other language constructs.

BibTeX citation:

@techreport{Gulwani:CSD-03-1296,
    Author = {Gulwani, Sumit and Necula, George C.},
    Title = {Global Value Numbering Using Random Interpretation (Full version)},
    Institution = {EECS Department, University of California, Berkeley},
    Year = {2003},
    Month = {Nov},
    URL = {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2003/6359.html},
    Number = {UCB/CSD-03-1296},
    Abstract = {We present a polynomial time randomized algorithm for global value numbering. Our algorithm is complete when conditionals are treated as non-deterministic and all operators are treated as uninterpreted functions. We are not aware of any complete polynomial-time deterministic algorithm for the same problem. The algorithm does not require symbolic manipulations and hence is simpler to implement than the deterministic symbolic algorithms. The price for these benefits is that there is a probability that the algorithm can report a false equality. We prove that this probability can be made arbitrarily small by controlling various parameters of the algorithm. <p> Our algorithm is based on the idea of random interpretation, which relies on executing a program on a number of random inputs and discovering relationships from the computed values. The computations are done by giving random linear interpretations to the operators in the program. Both branches of a conditional are executed. At join points, the program states are combined using a random affine combination. We discuss ways in which this algorithm can be made more precise by using more accurate interpretations for the linear arithmetic operators and other language constructs.}
}

EndNote citation:

%0 Report
%A Gulwani, Sumit
%A Necula, George C.
%T Global Value Numbering Using Random Interpretation (Full version)
%I EECS Department, University of California, Berkeley
%D 2003
%@ UCB/CSD-03-1296
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2003/6359.html
%F Gulwani:CSD-03-1296