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

Tutkimustuotos: Artikkeli kirjassa/konferenssijulkaisussavertaisarvioitu

Tutkijat

  • Natalia Gavrilenko
  • Hernán Ponce-de-León
  • Florian Furbach
  • Keijo Heljanko

  • Roland Meyer

Organisaatiot

  • fortiss GmbH
  • University of Helsinki
  • TU Braunschweig
  • Institute of Operating Systems and Computer Networks

Kuvaus

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.

Yksityiskohdat

AlkuperäiskieliEnglanti
OtsikkoComputer Aided Verification - 31st International Conference, CAV 2019, Proceedings
ToimittajatIsil Dillig, Serdar Tasiran
TilaJulkaistu - 1 tammikuuta 2019
OKM-julkaisutyyppiA4 Artikkeli konferenssijulkaisuussa
TapahtumaInternational Conference on Computer Aided Verification - New York City, Yhdysvallat
Kesto: 15 heinäkuuta 201918 heinäkuuta 2019
Konferenssinumero: 31

Julkaisusarja

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

Conference

ConferenceInternational Conference on Computer Aided Verification
LyhennettäCAV
MaaYhdysvallat
KaupunkiNew York City
Ajanjakso15/07/201918/07/2019

Lataa tilasto

Ei tietoja saatavilla

ID: 36034523