Scalable, Context-Sensitive, Guarded Data Race Detection

Despite significant progress in recent years, the important problem of practical static race detection remains open. Previous static techniques either suffer from a high false positive rate due to the compromise of precision, or scalability issues caused by a highly precise analysis.

In this work, we present a staged approach to resolve this paradox. It first performs a lightweight context-sensitive data access analysis, based on the value flow of a program, to identify the candidate data race subpaths instead of the whole program paths. Second, we employ May-Happen-in-Parallel (MHP) analysis to identify whether two data accesses in a program may execute concurrently. This stage is scalable, due to the design of the thread flow graph (TFG), that encodes thread information to query MHP relationship of the subpaths. Finally, for each subpath whose two data accesses are MHP, we apply heavyweight path-sensitive analysis to verify the feasibility of the data races.