BMC for Weak Memory Models: Relation Analysis for Compact SMT Encodings
Loading...
Access rights
openAccess
Journal Title
Journal ISSN
Volume Title
Conference article in proceedings
This publication is imported from Aalto University research portal.
View publication in the Research portal
View/Open full text file from the Research portal
Other link related to publication
View publication in the Research portal
View/Open full text file from the Research portal
Other link related to publication
Date
2019-01-01
Department
Major/Subject
Mcode
Degree programme
Language
en
Pages
11
355-365
355-365
Series
Computer Aided Verification - 31st International Conference, CAV 2019, Proceedings, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Volume 11561 LNCS
Abstract
We present Dartagnan, a bounded model checker (BMC) for concurrent programs under weak memory models. Its distinguishing feature is that the memory model is not implemented inside the tool but taken as part of the input. Dartagnan reads CAT, the standard language for memory models, which allows to define x86/TSO, ARMv7, ARMv8, Power, C/C++, and Linux kernel concurrency primitives. BMC with memory models as inputs is challenging. One has to encode into SMT not only the program but also its semantics as defined by the memory model. What makes Dartagnan scale is its relation analysis, a novel static analysis that significantly reduces the size of the encoding. Dartagnan matches or even exceeds the performance of the model-specific verification tools Nidhugg and CBMC, as well as the performance of Herd, a CAT-compatible litmus testing tool. Compared to the unoptimized encoding, the speed-up is often more than two orders of magnitude.Description
Keywords
BMC, CAT, Concurrency, SMT, Weak memory models
Other note
Citation
Gavrilenko, N, Ponce-de-León, H, Furbach, F, Heljanko, K & Meyer, R 2019, BMC for Weak Memory Models : Relation Analysis for Compact SMT Encodings . in I Dillig & S Tasiran (eds), Computer Aided Verification - 31st International Conference, CAV 2019, Proceedings . Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 11561 LNCS, Springer, pp. 355-365, International Conference on Computer Aided Verification, New York City, New York, United States, 15/07/2019 . https://doi.org/10.1007/978-3-030-25540-4_19
