IRUS Total

Effective lock handling in stateless model checking.

File Description SizeFormat 
3360599.pdfPublished version937.21 kBAdobe PDFView/Open
Title: Effective lock handling in stateless model checking.
Authors: Kokologiannakis, M
Raad, A
Vafeiadis, V
Item Type: Journal Article
Abstract: Stateless Model Checking (SMC) is a verification technique for concurrent programs that checks for safety violations by exploring all possible thread interleavings. SMC is usually coupled with Partial Order Reduction (POR), which exploits the independence of instructions to avoid redundant explorations when an equivalent one has already been considered. While effective POR techniques have been developed for many different memory models, they are only able to exploit independence at the instruction level, which makes them unsuitable for programs with coarse-grained synchronization mechanisms such as locks. We present a lock-aware POR algorithm, LAPOR, that exploits independence at both instruction and critical section levels. This enables LAPOR to explore exponentially fewer interleavings than the state-of-the-art techniques for programs that use locks conservatively. Our algorithm is sound, complete, and optimal, and can be used for verifying programs under several different memory models. We implement LAPOR in a tool and show that it can be exponentially faster than the state-of-the-art model checkers.
Issue Date: 1-Oct-2019
Date of Acceptance: 1-Oct-2019
URI: http://hdl.handle.net/10044/1/75938
DOI: 10.1145/3360599
ISSN: 2475-1421
Publisher: Association for Computing Machinery (ACM)
Start Page: 173:1
End Page: 173:26
Journal / Book Title: Proceedings of the ACM on Programming Languages
Volume: 3
Copyright Statement: © 2019 Copyright held by the owner/author(s). This work is licensed under a Creative Commons Attribution 4.0 International License. (https://creativecommons.org/licenses/by/4.0/)
Open Access location: https://dl.acm.org/doi/pdf/10.1145/3360599?download=true
Article Number: Article No.: 173
Online Publication Date: 2019-10-01
Appears in Collections:Computing