Skip to Main content Skip to Navigation
Book sections

Hunting Superfluous Locks with Model Checking

Abstract : Parallelization of existing sequential programs to increase their performance and exploit recent multi and many-core architectures is a challenging but inevitable effort. One increasingly popular paral-lelization approach is based on OpenMP, which enables the designer to annotate a sequential program with constructs specifying the parallel execution of code blocks. These constructs are then interpreted by the OpenMP compiler and runtime, which assigns blocks to threads running on a parallel architecture. Although this scheme is very flexible and not (very) intrusive, it does not prevent the occurrence of synchronization errors (e.g., deadlocks) or data races on shared variables. In this paper, we propose an iterative method to assist the OpenMP parallelization by using formal methods and verification. In each iteration, potential data races are identified by applying to the OpenMP program a lockset analysis , which computes the set of shared variables that potentially need to be protected by locks. To avoid the insertion of superfluous locks, an abstract , action-based formal model of the OpenMP program is extracted and analyzed using the ACTL on-the-fly model checker of the CADP formal verification toolbox. We describe the method, compare it with existing work, and illustrate its practical use.
Complete list of metadata

Cited literature [42 references]  Display  Hide  Download
Contributor : Radu Mateescu Connect in order to contact the contributor
Submitted on : Friday, October 11, 2019 - 5:20:15 PM
Last modification on : Friday, February 4, 2022 - 3:25:19 AM


Files produced by the author(s)



Viet-Anh Nguyen, Wendelin Serwe, Radu Mateescu, Eric Jenn. Hunting Superfluous Locks with Model Checking. From Software Engineering to Formal Methods and Tools, and Back, 11865, Springer Verlag, pp.416-432, 2019, Lecture Notes in Computer Science, ⟨10.1007/978-3-030-30985-5_24⟩. ⟨hal-02314088⟩



Record views


Files downloads