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

OpenMP is a popular API for the development of parallel, shared memory programs and allows programmers to easily ready their programs to utilize modern multi-core processors. However, OpenMPcompliant programs do not guarantee that the OpenMP parallelization is functionally equivalent to a sequential execution of the program. Therefore, several approaches analyze OpenMP programs. While some approaches check functional equivalence, they are either general purpose approaches, which ignore the structure of the program and the design pattern applied for parallelization, or they focus on parallelized for-loops. In this paper, we propose a verication technique that aims at pipeline parallelism. To show functional equivalence, our technique mainly computes the dependencies that a sequential execution imposes on the pipeline stages and checks whether these dependencies are properly incorporated in the OpenMP parallelzation. We implemented our verication technique in a prototype tool and evaluated it on several examples. Our evaluation shows that our technique soundly detects incorrect pipeline implementations.

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
11:00
20m
Talk
Verifying Pipeline Implementations in OpenMP
SPIN
Maik Wiesner TU Darmstadt, Marie-Christine Jakobs TU Darmstadt, Germany
11:20
20m
Talk
A model-checked I2C specification
SPIN
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
11:40
20m
Talk
PatEC: Pattern-based Equivalence Checking
SPIN
Marie-Christine Jakobs TU Darmstadt, Germany