Equivalence Checking of Code Transformation by Numerical and Symbolic Approaches

Abstract

Due to the increasing diversity and complexity of high-performance systems, system-specific optimization is vital to extract the system performance. To ensure that optimization does not degrade code readability and maintainability, user-defined code transformation tools are used. However, such transformation tools may change the behavior of a program. This paper focuses on Xevolver, a code transformation tool where code patterns before and after transformation are used to define transformation rules, and proposes a method to check the equivalence of transformation rules based on symbolic execution. Since equivalence checking by symbolic execution has limitations such as long runtime and inability to detect numerical errors, we also propose an equivalence checking method by numerical comparison to assist the equivalence checking by symbolic execution. In the evaluation, various optimization methods described as Xevolver transformation rules are checked for equivalence using the proposed method. The evaluation results demonstrate that the proposed equivalence checking method can cover a wider range of application codes.