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 metadatas

Cited literature [42 references]  Display  Hide  Download

https://hal.inria.fr/hal-02314088
Contributor : Radu Mateescu <>
Submitted on : Friday, October 11, 2019 - 5:20:15 PM
Last modification on : Friday, October 25, 2019 - 1:28:26 AM

File

Nguyen-Serwe-Mateescu-Jenn-19....
Files produced by the author(s)

Identifiers

Citation

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, pp.416-432, 2019, Lecture Notes in Computer Science, ⟨10.1007/978-3-030-30985-5_24⟩. ⟨hal-02314088⟩

Share

Metrics

Record views

71

Files downloads

198