Write a Blog >>
SPIN 2021
Mon 12 Jul 2021 Online
co-located with ECOOP and ISSTA 2021
Mon 12 Jul 2021 11:40 - 12:00 at SPIN - Session 1 Chair(s): Anton Wijs

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 Jul

Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

11:00 - 12:00
Session 1SPIN at SPIN
Chair(s): Anton Wijs Eindhoven University of Technology
Verifying Pipeline Implementations in OpenMP
Maik Wiesner TU Darmstadt, Marie-Christine Jakobs TU Darmstadt, Germany
A model-checked I2C specification
Lukas Humbel ETH Zurich, Daniel Schwyn ETH Zurich, Nora Hossle ETH Zurich, Roni Häcki ETH Zurich, Melissa Licciardello ETH Zurich, Jan Schär ETH Zurich, David Cock ETH Zurich, Michael Giardino ETH Zurich, Timothy Roscoe ETH Zurich
PatEC: Pattern-based Equivalence Checking
Marie-Christine Jakobs TU Darmstadt, Germany