Bounded Model Checking of Concurrent Data Types on Relaxed Memory Models: A Case Study

In this paper we present new implementation details and benchmarking results for our parallel portfolio solver TopoSAT2. In particular, we discuss ideas and implementation details for the exchange of learned clauses in a massively-parallel SAT solver which is designed to run more that 1, 000 solver threads in parallel. Furthermore, we go back to the roots of portfolio SAT solving, and discuss the impact of diversifying the solver by using different restart- , branching- and clause database management heuristics. We show that these techniques can be used to tune the solver towards different problems. However, in a case study on formulas derived from Bounded Model Checking problems we see the best performance when using a rather simple clause exchange strategy. We show details of these tests and discuss possible explanations for this phenomenon.As computing times on massively-parallel clusters are expensive, we consider it especially interesting to share these kind of experimental results.

Download Full-text

Dartagnan: Bounded Model Checking for Weak Memory Models (Competition Contribution)

Tools and Algorithms for the Construction and Analysis of Systems - Lecture Notes in Computer Science ◽

10.1007/978-3-030-45237-7_24 ◽

2020 ◽

pp. 378-382

Author(s):

Hernán Ponce-de-León ◽

Florian Furbach ◽

Keijo Heljanko ◽

Roland Meyer

Keyword(s):

Model Checking ◽

Bounded Model Checking ◽

Memory Models ◽

Memory Model ◽

Complete Analysis ◽

Concurrent Programs ◽

Sequential Consistency ◽

Model Checker ◽

Safety Properties ◽

C Programs

Abstract Dartagnanis a bounded model checker for concurrent programs under weak memory models. What makes it different from other tools is that the memory model is not hard-coded inside Dartagnanbut taken as part of the input. For SV-COMP’20, we take as input sequential consistency (i.e. the standard interleaving memory model) extended by support for atomic blocks. Our point is to demonstrate that a universal tool can be competitive and perform well in SV-COMP. Being a bounded model checker, Dartagnan’s focus is on disproving safety properties by finding counterexample executions. For programs with bounded loops, Dartagnanperforms an iterative unwinding that results in a complete analysis. The SV-COMP’20 version of Dartagnanworks on Boogiecode. The C programs of the competition are translated internally to Boogieusing SMACK.

Download Full-text

Efficient Bounded Model Checking of Heap-Manipulating Programs using Tight Field Bounds

Fundamental Approaches to Software Engineering - Lecture Notes in Computer Science ◽

10.1007/978-3-030-71500-7_11 ◽

2021 ◽

pp. 218-239

Author(s):

Pablo Ponzio ◽

Ariel Godio ◽

Nicolás Rosner ◽

Marcelo Arroyo ◽

Nazareno Aguirre ◽

...

Keyword(s):

Model Checking ◽

Data Structures ◽

Efficient Algorithm ◽

Bounded Model Checking ◽

Model Checker ◽

Data Types ◽

Dynamic Data Structures ◽

Dynamic Data ◽

Software Model ◽

Improve Model

AbstractSoftware model checkers are able to exhaustively explore different bounded program executions arising from various sources of non-determinism. These tools provide statements to produce non-deterministic values for certain variables, thus forcing the corresponding model checker to consider all possible values for these during verification. While these statements offer an effective way of verifying programs handling basic data types and simple structured types, they are inappropriate as a mechanism for nondeterministic generation of pointers, favoring the use of insertion routines to produce dynamic data structures when verifying, via model checking, programs handling such data types.We present a technique to improve model checking of programs handling heap-allocated data types, by taming the explosion of candidate structures that can be built when non-deterministically initializing heap object fields. The technique exploits precomputed relational bounds, that disregard values deemed invalid by the structure’s type invariant, thus reducing the state space to be explored by the model checker. Precomputing the relational bounds is a challenging costly task too, for which we also present an efficient algorithm, based on incremental SAT solving.We implement our approach on top of the bounded model checker, and show that, for a number of data structures implementations, we can handle significantly larger input structures and detect faults that is unable to detect.

Download Full-text