Lock and Fence When Needed: State Space Exploration + Static Analysis = Improved Fence and Lock Insertion

Sander de Putter, Anton Wijs

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review


When targeting modern parallel hardware architectures, constructing correct and high-performing software is complex and time-consuming. In particular, reorderings of memory accesses that violate intended sequentially consistent behaviour are a major source of bugs. Applying synchronisation mechanisms to repair these should be done sparingly, as they negatively impact performance. In the past, both static analysis approaches and techniques based on explicit-state model checking have been proposed to identify where synchronisation fences have to be placed in a program. The former are fast, but the latter more precise, as they tend to insert fewer fences. Unfortunately, the model checking techniques suffer a form of state space explosion that is even worse than the traditional one. In this work, we propose a technique using a combination of state space exploration and static analysis. This combination is in terms of precision comparable to purely model checking-based techniques, but it reduces the state space explosion problem to the one typically seen in model checking. Furthermore, experiments show that the combination frequently outperforms both purely model checking and static analysis techniques. In addition, we have added the capability to check for atomicity violations, which is another major source of bugs.

Originele taal-2Engels
TitelIntegrated Formal Methods - 16th International Conference, IFM 2020, Proceedings
RedacteurenBrijesh Dongol, Elena Troubitsyna
UitgeverijSpringer Science and Business Media Deutschland GmbH
Aantal pagina's21
ISBN van geprinte versie9783030634605
StatusGepubliceerd - 2020
Evenement16th International Conference on Integrated Formal Methods, IFM 2020 - Lugano, Zwitserland
Duur: 16 nov 202020 nov 2020

Publicatie series

NaamLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume12546 LNCS
ISSN van geprinte versie0302-9743
ISSN van elektronische versie1611-3349


Congres16th International Conference on Integrated Formal Methods, IFM 2020

Vingerafdruk Duik in de onderzoeksthema's van 'Lock and Fence When Needed: State Space Exploration + Static Analysis = Improved Fence and Lock Insertion'. Samen vormen ze een unieke vingerafdruk.

Citeer dit