Recurrence sets characterize non-termination in sequential programs. We present a generalization of recurrence sets to concurrent programs that run on weak memory models. Sequential programs have operational semantics in terms of states and transitions, and classical recurrence sets are defined as sets of states that are existentially closed under transitions. Concurrent programs have axiomatic semantics in terms of executions, and our new recurrence sets are defined as sets of executions that are existentially closed under extensions. The semantics of concurrent programs is not only affected by the memory model, but also by fairness assumptions about its environment, be it the scheduler or the memory subsystems. Our new recurrence sets are formulated relative to such fairness assumptions. We show that our recurrence sets are sound for proving fair non-termination on all practical memory models, and even complete on many. To turn our theory into practice, we develop a new automated technique for proving fair non-termination in concurrent programs on weak memory models. At the heart of this technique is a finite representation of recurrence sets in terms of execution-based lassos. We implemented a lasso-finding algorithm in Dartagnan, and evaluated it on a number of programs running under CPU and GPU memory models.

After more than 30 years of research, there is a solid understanding of the consistency guarantees given by CPU systems. Unfortunately, the same is not yet true for GPUs. The growing popularity of general purpose GPU programming has been a call for action which industry players like Nvidia and Khronos have answered by formalizing their Ptx and Vulkan consistency models. These models give precise answers to questions about program's correctness. However, interpreting them still requires a level of expertise that escapes most developers, and the current tool support is insufficient.

The goal of this work is to improve the efficiency of bounded model checkers that are modular in the memory model. Our first contribution is a static analysis for the given memory model that is performed as a preprocessing step and helps us significantly reduce the encoding size. Memory model make use of relations to judge whether an execution is consistent. The analysis computes bounds on these relations: which pairs of events may or must be related. What is new is that the bounds are relativized to the execution of events. This makes it possible to derive, for the first time, not only upper but also meaningful lower bounds. Another important feature is that the analysis can import information about the verification instance from external sources to improve its precision. Our second contribution are new optimizations for the SMT encoding. Notably, the lower bounds allow us to simplify the encoding of acyclicity constraints. We implemented our analysis and optimizations within a bounded model checker and evaluated it on challenging benchmarks. The evaluation shows up-to 40% reduction in verification time (including the analysis) over previous encodings. Our optimizations allow us to efficiently check safety, liveness, and data race freedom in Linux kernel code.

The SPECTRE family of speculative execution attacks has required a rethinking of formal methods for security. Approaches based on operational speculative semantics have made initial inroads towards finding vulnerable code and validating defenses. However, with each new attack grows the amount of microarchitectural detail that has to be integrated into the underlying semantics. We propose an alternative, lightweight and axiomatic approach to specifying speculative semantics that relies on insights from memory models for concurrency. We use the CAT modeling language for memory consistency to specify execution models that capture speculative control flow, store-to-load forwarding, predictive store forwarding, and memory ordering machine clears. We present a bounded model checking framework parameterized by our speculative CAT models and evaluate its implementation against the state of the art. Due to the axiomatic approach, our models can be rapidly extended to allow our framework to detect new types of attacks and validate defenses against them.

Abstract The validation of violation witnesses is an important step during software verification. It hides false alarms raised by verifiers from engineers, which in turn helps them concentrate on critical issues and improves the verification experience. Until the 2021 edition of the Competition on Software Verification (SV-COMP), CPAchecker was the only witness validator for the ConcurrencySafety category. This article describes how we extended the Dartagnan verifier to support the validation of violation witnesses. The results of the 2022 edition of the competition show that, for witnesses generated by different verifiers, Dartagnan succeeds in the validation of witnesses where CPAchecker does not. Our extension thus improves the validation possibilities for the overall competition. We discuss Dartagnan ’s strengths and weaknesses as a validation tool and describe possible ways to improve it in the future.

We propose a family of logical theories for capturing an abstract notion of consistency and show how to build a generic and efficient theory solver that works for all members in the family. The theories can be used to model the influence of memory consistency models on the semantics of concurrent programs. They are general enough to precisely capture important examples like TSO, POWER, ARMv8, RISC-V, RC11, IMM, and the Linux kernel memory model. To evaluate the expressiveness of our theories and the performance of our solver, we integrate them into a lazy SMT scheme that we use as a backend for a bounded model checking tool. An evaluation against related verification tools shows, besides flexibility, promising performance on challenging programs under complex memory models.

Abstract We describe the new features of the bounded model checkerDartagnanforSV-COMP’21. We participate, for the first time, in theReachSafetycategory on the verification of sequential programs. In some of these verification tasks, bugs only show up after many loop iterations, which is a challenge for bounded model checking. We address the challenge by simplifying the structure of the input program while preserving its semantics. For simplification, we leverage common compiler optimizations, which we get for free by using LLVM. Yet, there is a price to pay. Compiler optimizations may introduce bitwise operations, which require bit-precise reasoning. We evaluated an SMT encoding based on the theory of integers + bit conversions against one based on the theory of bit-vectors and found that the latter yields better performance. Compared to the unoptimized version ofDartagnan, the combination of compiler optimizations and bit-vectors yields a speed-up of an order of magnitude on average.

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.

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 , ARM v7, ARM v8, 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.

This paper reports progress in verification tool engineering for weak memory models. We present two bounded model checking tools for concurrent programs. Their distinguishing feature is modularity: Besides a program, they expect as input a module describing the hardware architecture for which the program should be verified. DARTAGNAN verifies state reachability under the given memory model using a novel SMT encoding. PORTHOS checks state equivalence under two given memory models using a guided search strategy. We have performed experiments to compare our tools against other memory model-aware verifiers and find them very competitive, despite the modularity offered by our approach.

This article focuses on computing minimal test suites for multithreaded programs. Based on previous work on test case generation for multithreaded programs using unfoldings, this article shows how this unfolding can be used to generate minimal test suites covering all local states of the program. Generating such minimal test suites is shown to be NP-complete in the size of the unfolding. We propose an SMT encoding for this problem and two methods based on heuristics which only approximate the solution, but scale better in practice. Finally, we apply our methods to compute the minimal test suites for several benchmarks.

SUMMARY We propose a theoretical testing framework and a test generation algorithm for concurrent systems specified with true‐concurrency models, such as Petri nets or networks of automata. The semantic model of computation of such formalisms is labelled event structures, which allow to represent concurrency explicitly. We introduce the notions of strong and weak concurrency: strongly concurrent events must be concurrent in the implementation, while weakly concurrent ones may eventually be ordered. The ioco type conformance relations for sequential systems rely on the observation of sequences of actions and blockings; thus, they are not capable of capturing and exploiting concurrency of non‐sequential behaviours. We propose an extension of ioco for labelled event structures, named co‐ioco, allowing to deal with strong and weak concurrency. We extend the notions of test cases and test execution to labelled event structures and give a test generation algorithm building a complete test suite for co‐ioco. Copyright © 2014 John Wiley & Sons, Ltd.