Verifying Parallel Code After Refactoring Using Equivalence Checking

Abstract

To take advantage of multi-core systems, programmers are replacing sequential software with parallel software. Software engineers often avoid writing their parallel software from scratch and prefer refactoring their legacy application, either manually or with the help of a refactoring tool. In either case, it is extremely challenging to produce correct parallel code, taking into account all synchronization issues. Furthermore, the complexity of parallel code makes its verification extremely difficult. We introduce a method for the verification of parallel code after refactoring. Our method, which is based on symbolic interpretation, leverages the original sequential code that in most cases was already tested and/or verified, and checks whether it is equivalent to the code after refactoring. The advantage of this method is that it can generically find any problem in the parallel code that does not exist in the original sequential code. As a result, it can help create higher quality and safer parallel code.