PatEC: Pattern-based Equivalence Checking
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.
Mon 12 JulDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
11:00 - 12:00
|Verifying Pipeline Implementations in OpenMP|
|A model-checked I2C specification|
|PatEC: Pattern-based Equivalence Checking|
Marie-Christine Jakobs TU Darmstadt, Germany