The Virtues of Conflict: Analyzing Modern Concurrency

TL;DR

This paper introduces a conflict-aware, truly concurrent semantics for weak memory programs that improves the efficiency of detecting assertion violations in multi-threaded C/C++ programs.

Contribution

It proposes a novel symbolic semantics based on event structures that better models real-world program conflicts and outperforms existing partial-order approaches.

Findings

Outperforms state-of-the-art partial-order based methods

Efficient decision procedure for assertion violations

Scalable analysis on large benchmarks

Abstract

Modern shared memory multiprocessors permit reordering of memory operations for performance reasons. These reorderings are often a source of subtle bugs in programs written for such architectures. Traditional approaches to verify weak memory programs often rely on interleaving semantics, which is prone to state space explosion, and thus severely limits the scalability of the analysis. In recent times, there has been a renewed interest in modelling dynamic executions of weak memory programs using partial orders. However, such an approach typically requires ad-hoc mechanisms to correctly capture the data and control-flow choices/conflicts present in real-world programs. In this work, we propose a novel, conflict-aware, composable, truly concurrent semantics for programs written using C/C++ for modern weak memory architectures. We exploit our symbolic semantics based on general event structures to build an efficient decision procedure that detects assertion violations in bounded multi-threaded programs. Using a large, representative set of benchmarks, we show that our conflict-aware semantics outperforms the state-of-the-art partial-order based approaches.