BMC for Weak Memory Models: Relation Analysis for Compact SMT Encodings

Natalia Gavrilenko; Hernán Ponce-de-León; Florian Furbach; Keijo Heljanko; Roland Meyer

doi:10.1007/978-3-030-25540-4_19

BMC for Weak Memory Models: Relation Analysis for Compact SMT Encodings

Natalia Gavrilenko^*, Hernán Ponce-de-León, Florian Furbach, Keijo Heljanko, Roland Meyer

^*Tämän työn vastaava kirjoittaja

Tietotekniikan laitos

Tutkimustuotos: Artikkeli kirjassa/konferenssijulkaisussa › Conference contribution › Scientific › vertaisarvioitu

19 Sitaatiot (Scopus)

113 Lataukset (Pure)

Abstrakti

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.

Alkuperäiskieli	Englanti
Otsikko	Computer Aided Verification - 31st International Conference, CAV 2019, Proceedings
Toimittajat	Isil Dillig, Serdar Tasiran
Kustantaja	Springer
Sivut	355-365
Sivumäärä	11
ISBN (painettu)	9783030255398
DOI - pysyväislinkit	https://doi.org/10.1007/978-3-030-25540-4_19
Tila	Julkaistu - 1 tammik. 2019
OKM-julkaisutyyppi	A4 Artikkeli konferenssijulkaisuussa
Tapahtuma	International Conference on Computer Aided Verification - New York City, Yhdysvallat Kesto: 15 heinäk. 2019 → 18 heinäk. 2019 Konferenssinumero: 31

Julkaisusarja

Nimi	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Vuosikerta	11561 LNCS
ISSN (painettu)	0302-9743
ISSN (elektroninen)	1611-3349

Conference

Conference	International Conference on Computer Aided Verification
Lyhennettä	CAV
Maa/Alue	Yhdysvallat
Kaupunki	New York City
Ajanjakso	15/07/2019 → 18/07/2019

Pääsy asiakirjaan

10.1007/978-3-030-25540-4_19

Gavrilenko2019_Chapter_BMCForWeakMemoryModelsRelationFinal published version, 543 KBLisenssi: CC BY

OpenUrl-saatavuus

Koko teksti

Muut tiedostot ja linkit

Link to publication in Scopus

Siteeraa tätä

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. teoksessa I. Dillig, & S. Tasiran (Toimittajat), Computer Aided Verification - 31st International Conference, CAV 2019, Proceedings (Sivut 355-365). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vuosikerta 11561 LNCS). Springer. https://doi.org/10.1007/978-3-030-25540-4_19

Gavrilenko, Natalia ; Ponce-de-León, Hernán ; Furbach, Florian et al. / BMC for Weak Memory Models : Relation Analysis for Compact SMT Encodings. Computer Aided Verification - 31st International Conference, CAV 2019, Proceedings. Toimittaja / Isil Dillig ; Serdar Tasiran. Springer, 2019. Sivut 355-365 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{4e699328c9964f43a915b86b5091c913,

title = "BMC for Weak Memory Models: Relation Analysis for Compact SMT Encodings",

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.",

keywords = "BMC, CAT, Concurrency, SMT, Weak memory models",

author = "Natalia Gavrilenko and Hern{\'a}n Ponce-de-Le{\'o}n and Florian Furbach and Keijo Heljanko and Roland Meyer",

year = "2019",

month = jan,

day = "1",

doi = "10.1007/978-3-030-25540-4_19",

language = "English",

isbn = "9783030255398",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "355--365",

editor = "Isil Dillig and Serdar Tasiran",

booktitle = "Computer Aided Verification - 31st International Conference, CAV 2019, Proceedings",

address = "Germany",

note = "International Conference on Computer Aided Verification, CAV ; Conference date: 15-07-2019 Through 18-07-2019",

}

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. julkaisussa I Dillig & S Tasiran (toim), 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), Vuosikerta 11561 LNCS, Springer, Sivut 355-365, International Conference on Computer Aided Verification, New York City, New York, Yhdysvallat, 15/07/2019. https://doi.org/10.1007/978-3-030-25540-4_19

BMC for Weak Memory Models: Relation Analysis for Compact SMT Encodings. / Gavrilenko, Natalia; Ponce-de-León, Hernán; Furbach, Florian et al.
Computer Aided Verification - 31st International Conference, CAV 2019, Proceedings. toim. / Isil Dillig; Serdar Tasiran. Springer, 2019. s. 355-365 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vuosikerta 11561 LNCS).

Tutkimustuotos: Artikkeli kirjassa/konferenssijulkaisussa › Conference contribution › Scientific › vertaisarvioitu

TY - GEN

T1 - BMC for Weak Memory Models

T2 - International Conference on Computer Aided Verification

AU - Gavrilenko, Natalia

AU - Ponce-de-León, Hernán

AU - Furbach, Florian

AU - Heljanko, Keijo

AU - Meyer, Roland

N1 - Conference code: 31

PY - 2019/1/1

Y1 - 2019/1/1

N2 - 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.

AB - 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.

KW - BMC

KW - CAT

KW - Concurrency

KW - SMT

KW - Weak memory models

UR - http://www.scopus.com/inward/record.url?scp=85069884055&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-25540-4_19

DO - 10.1007/978-3-030-25540-4_19

M3 - Conference contribution

AN - SCOPUS:85069884055

SN - 9783030255398

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 355

EP - 365

BT - Computer Aided Verification - 31st International Conference, CAV 2019, Proceedings

A2 - Dillig, Isil

A2 - Tasiran, Serdar

PB - Springer

Y2 - 15 July 2019 through 18 July 2019

ER -

Gavrilenko N, Ponce-de-León H, Furbach F, Heljanko K, Meyer R. BMC for Weak Memory Models: Relation Analysis for Compact SMT Encodings. julkaisussa Dillig I, Tasiran S, toimittajat, Computer Aided Verification - 31st International Conference, CAV 2019, Proceedings. Springer. 2019. s. 355-365. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-030-25540-4_19

BMC for Weak Memory Models: Relation Analysis for Compact SMT Encodings

Abstrakti

Julkaisusarja

Conference

Pääsy asiakirjaan

OpenUrl-saatavuus

Muut tiedostot ja linkit

Sormenjälki

Siteeraa tätä