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

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

Researchers

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

  • Roland Meyer

Research units

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

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.

Details

Original languageEnglish
Title of host publicationComputer Aided Verification - 31st International Conference, CAV 2019, Proceedings
EditorsIsil Dillig, Serdar Tasiran
Publication statusPublished - 1 Jan 2019
MoE publication typeA4 Article in a conference publication
EventInternational Conference on Computer Aided Verification - New York City, United States
Duration: 15 Jul 201918 Jul 2019
Conference number: 31

Publication series

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

Conference

ConferenceInternational Conference on Computer Aided Verification
Abbreviated titleCAV
CountryUnited States
CityNew York City
Period15/07/201918/07/2019

    Research areas

  • BMC, CAT, Concurrency, SMT, Weak memory models

Download statistics

No data available

ID: 36034523