Click here for full text:
The Straight-Line Automatic Programming Problem
Joshi, Rajeev; Nelson, Greg; Zhou, Yunhong
HPL-2003-236
Keyword(s): super-optimization; code generation; straight-line automatic programming problem
Abstract: The paper presents a design for the Denali-2 super- optimizer, which will generate minimum-instruction- length machine code for realistic machine architectures using automatic theorem-proving technology: specifically, using E-graph matching (a technique for pattern matching in the presence of equality information) and boolean satisfiability solving. The paper presents a precise definition of the underlying automatic programming problem solved by the Denali-2 super-optimizer. It sketches the E-graph matching phase and presents a detailed exposition and proof of correctness of the reduction of the automatic programming problem to the boolean satisfiability problem.
18 Pages
Back to Index
| 
printable version
