Dynamic Verification with Observational Equivalence of C/C++ Concurrency

TL;DR

This paper introduces observational equivalence for verifying C/C++ concurrent programs under relaxed memory models, enabling more efficient state-space exploration and improved verification accuracy.

Contribution

It proposes a new coarser trace equivalence called observational equivalence, along with an algorithm to compute it efficiently for C/C++ concurrency verification.

Findings

Significant reduction in explored traces using OE

More extensive treatment of C/C++ concurrency than existing methods

Effective verification demonstrated on threaded C/C++ programs

Abstract

Program executions under relaxed memory model (rmm) semantics are significantly more difficult to analyze; the rmm semantics result in out of order execution of program events leading to an explosion of state-space. Dynamic partial order reduction (DPOR) is a powerful technique to address such a state-space explosion and has been used to verify programs under rmm such as TSO, PSO, and POWER. Central to such DPOR techniques is the notion of trace-equivalence, which is computed based on the independence relation among program events. We propose a coarser notion of rmm-aware trace equivalence called observational equivalence (OE). Two program behaviors are observationally equivalent if every read event reads the same value in both the behaviors. We propose a notion of observational independence (OI) and provide an algorithmic construction to compute trace equivalence (modulo OI) efficiently. We also demonstrate the effectiveness of DPOR with OE on threaded C/C++ programs by first providing an elaborate happensbefore (hb) relation for capturing the C/C++ concurrency semantics. We implement the presented technique in a runtime model checker called Drista. Our experiments reflect that (i) when compared to existing nonOE techniques, we achieve significant savings in the number of traces explored under OE, and (ii) our treatment of C/C++ concurrency is more extensive than the existing state-of-the-art techniques.