Witnessing an SSA Transformation

ABSTRACT. Ensuring the correctness of program compilations is an important step in assuring the correctness of an overall software system. In this work, we describe an effort to verify he SSA (single static assignment) compiler transformation, which turns memory references (i.e., load, store) into corresponding register references (i.e., read, write). It is one of the most important optimizations in modern compilers, and may account for more than half of the optimization speed up. Formally verifying the algorithm behind this transformation is thought to be a difficult task. Verifying the actual code, as implemented in a production compiler, is currently infeasible. We describe an alternative verification strategy, based on generating and checking ``witnesses'' for each instance of the transformation. This approach enormously simplifies the verification task, primarily because it does not require showing that the transformation code is correct.