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

Sander de Putter, Anton Wijs

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

Abstract

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.

Original languageEnglish
Title of host publicationIntegrated Formal Methods - 16th International Conference, IFM 2020, Proceedings
EditorsBrijesh Dongol, Elena Troubitsyna
PublisherSpringer Science and Business Media Deutschland GmbH
Pages297-317
Number of pages21
ISBN (Print)9783030634605
DOIs
Publication statusPublished - 2020
Event16th International Conference on Integrated Formal Methods, IFM 2020 - Lugano, Switzerland
Duration: 16 Nov 202020 Nov 2020

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume12546 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference16th International Conference on Integrated Formal Methods, IFM 2020
CountrySwitzerland
CityLugano
Period16/11/2020/11/20

Fingerprint Dive into the research topics of 'Lock and Fence When Needed: State Space Exploration + Static Analysis = Improved Fence and Lock Insertion'. Together they form a unique fingerprint.

Cite this