Tolerate Control-Flow Changes for Sound Data Race Prediction

Data races seriously threaten the correctness of concurrent programs. Earlier works can report false positives. Recently, trace-based predictive analysis has achieved sound results by inferring feasible traces based on sound partial orders or constraint solvers. However, they hold the same assumption: any read event may affect the control-flow of a predicted trace. Thus, being control-flow sensitive, they have to enforce any read event (in an inferred trace) to either read the same value or a value from the same event as that in the original trace, albeit some slightly relax this. This (even with relaxation) severely limits their predictive ability and many true data races can be missed. We introduce the concept of Fix-Point Event and propose a new partial order model. This allows us to not only predict races with witness traces (like existing works with no control-flow changes) but also soundly infer existences of witness traces with potential control-flow changes. Thus, we can achieve a higher concurrency coverage and detect more data races soundly. We have implemented above as a tool ToccRACE and conducted a set of experiments on a benchmark of seven real-world programs and a large-scale software MySQL, where MySQL produced 427 traces with a total size of 3.4TB. Compared with the state-of-the-art sound data race detector SeqCheck,ToccRACE is significantly more effective by detecting 84.4%/200% more unique/dynamic races on the benchmark programs and 52.22%/49.8% more unique/dynamic races on MySQL, incurring reasonable time and memory costs (about 1.1x×43.5x on the benchmark programs and 10x/1.03x on MySQL). Furthermore, ToccRACE is sound and is comnlcte on two threads.