Program parallelization is a common software engineering task, in which parallel design patterns (i.e., well-established parallelization solutions) are applied regularly. The focus of parallelization is on performance. Meanwhile, the functional behavior should be kept invariant, i.e., sequential and parallelized program should be functionally equivalent. While several verification techniques exist that analyze properties of parallel programs, only a few approaches inspect functional equivalence between a sequential program and its parallelization. Even less approaches that check equivalence consider parallel design patterns.

In this paper, we present PatEC, which checks equivalence between sequential programs and their OpenMP parallelizations. PatEC utilizes the knowledge about the applied parallel design pattern to split equivalence checking into smaller subtasks. Our experiments show that PatEC is effective, efficient and often outperforms existing approaches.