Verifying Pipeline Implementations in OpenMP
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 JulDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
11:00 - 12:00 | |||
11:00 20mTalk | Verifying Pipeline Implementations in OpenMP SPIN | ||
11:20 20mTalk | 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 20mTalk | PatEC: Pattern-based Equivalence Checking SPIN Marie-Christine Jakobs TU Darmstadt, Germany |