Implementing an Efficient Path Based Equivalence Checker for Parallel Programs
Soumyadip Bandyopadhyay, Kunal Banerjee · 2016
User written programs, when transformed by optimizing and parallelizing compilers, can be incorrect, if the compiler is not trusted. So, establishing the validity of these transformations is a crucial and challenging task. For program verification, the PRES+ (Petri net Representation of Embedded Systems) is now well accepted as a model to capture the data and control flow of a program. In this paper, an efficient path based equivalence checking method using a simple PRES+ model (which is easier to generate from a program) for validating several optimizing and parallelizing transformations is proposed. The experimental results demonstrate the efficiency of the method.