Commutativity-aware Runtime Verification for Concurrent Programs

Concurrent programs are notoriously difficult to write correctly, as scheduling nondeterminism can introduce subtle errors that are hard to detect and debug. Considerable effort has been made towards developing effective program analysis and verification techniques for concurrency bug detection. Most notably, runtime verification aims to infer the presence of concurrency bugs from the execution traces and has been shown very effective in practice. This thesis first develops an efficient runtime verification technique to detect unseen order violations from the observed execution. Our technique novelly extends existing predictive analyses that construct partial ordering over trace events in a streaming fashion, reporting unordered pairs of conflicting events as potential order violations. Unlike existing predictive analyses, our technique aims to detect a wider class of concurrency bugs beyond the traditional races. We introduce the notion of commutativity order violations. A commutativity order violation occurs in the input trace if there is a witness in which two non-commutative actions appear in the reversed order. This broad definition captures both racy and non-racy interaction at the library interface and thus strictly subsumes the standard definition of predictable races. For example, an order violation involving two conflicting actions on the same lock is not a race due to the lock synchronization. We implemented our algorithm into a tool called OVPredict. To address the performance bottleneck of existing predictive analyses, we further propose a space-efficient shadow word representation for tracking the ordering between conflicting critical sections. Our experiments on several real-world large Go and C++ applications show that our analysis detects more order violations than ThreadSanitizer, an industrial-strength race detector, and scales to traces with billions of events. OVPredict revealed several previously unknown order vioilations in Kubernetes and CockroachDB. The second focus of this thesis is to develop an efficient stateless model checking algorithm for concurrent programs that use linearizable commutative data structures. We present NCMC, a new stateless model checking algorithm that exploits semantic commutativity between method invocations in concurrent programs. Unlike most previous approaches that capture independence at the instruction level, our approach reasons about independence at both instruction and semantics levels. We introduce the notion of semantic commutativity equivalence (SC-equivalence), a coarser equivalence than the ones characterized by partial orders over events at the instruction level. Underpinned by SC-equivalence, our algorithm uses a commutativity specification to identify noncommutative operations in each exploration and avoids exploring executions that do not cover any new abstract state of the program