Global Value Numbering using Random Interpretation

Sumit Gulwani George C. Necula

To appear at Principles of Programming Languages (POPL04), Venice, Italy, January 14-16, 2004


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.

Server START Conference Manager
Update Time 19 Sep 2003 at 17:40:43
Start Conference Manager
Conference Systems