Hunting Superfluous Locks with Model Checking - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Chapitre D'ouvrage Année : 2019

Hunting Superfluous Locks with Model Checking

Résumé

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.
Fichier principal
Vignette du fichier
Nguyen-Serwe-Mateescu-Jenn-19.pdf (282.94 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-02314088 , version 1 (11-10-2019)

Identifiants

Citer

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⟩
180 Consultations
189 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More