Reduce Dependence for Sound Concurrency Bug Prediction

Recently, dynamic concurrency bug predictions have kept making notable progress in improving concurrency coverage while ensuring soundness. Most of them rely solely on dynamic information in traces and overlook the static semantics of the program when predicting bugs. To ensure soundness, they assume that any (memory) read can fully affect subsequent program execution via control-flow and data-flow. However, the assumption over-approximates constraints among (memory) writes and reads and hence limits reordering space over thread interleaving, ultimately leading to false negatives. From program semantics, only a subset of reads actually affect their subsequent executions. Therefore, by refining dependencies between reads and subsequent executions based on static program semantics, one can refine the assumption and eliminate unnecessary constraints. This can bring a chance to explore more thread interleaving space and uncover more concurrency bugs. However, refining dependencies can compromise soundness and bring heavy overhead. To tackle these challenges, this paper introduces the concept of Necessary Consistent Read Event (NRE) and a hybrid analysis algorithm. NRE refines dependencies between reads and their subsequent events and is used to identify necessary constraints where a read probably affects the execution of its subsequent events. Next, we design an efficient and accurate hybrid analysis algorithm to calculate NREs for each event in the trace. The hybrid analysis algorithm maps events to program SSA instructions and simulates executions based on the original trace. NRE and the algorithm can enhance the capabilities of existing concurrency bug prediction methods at a low cost, regardless of the type of concurrency bug they target. In this paper, we focused on data race and developed NRE and the algorithm as a prototype tool RECONP. We conducted a set of comparative experiments on MySQL with M2 and Seqcheck. The results show that RECONP can detect 46.9% and 22.4% more data races than M2 and Seqcheck, respectively. And the hybrid algorithm only accounts for 34% of the total time cost.