A Thread-Local Semantics and Efficient Static Analyses for Race Free Programs

TL;DR

This paper introduces a thread-local semantics for data race free programs, enabling scalable and precise static analyses that significantly improve assertion proving efficiency and speed compared to existing tools.

Contribution

It proposes a novel thread-local semantics (L-DRF) for DRF programs, simplifying analysis by reducing it to sequential analysis, and develops a region-based abstraction for more precise analysis.

Findings

RATCOP proved up to 65% of assertions on benchmarks.

RATCOP was up to 5 orders of magnitude faster than recent analyzers.

The semantics enable scalable and precise static analysis for DRF programs.

Abstract

Data race free (DRF) programs constitute an important class of concurrent programs. In this paper we provide a framework for designing and proving the correctness of data flow analyses that target this class of programs. These analyses are in the same spirit as the "sync-CFG" analysis proposed in earlier literature. To achieve this, we first propose a novel concrete semantics for DRF programs, called L-DRF, that is thread-local in nature---each thread operates on its own copy of the data state. We show that abstractions of our semantics allow us to reduce the analysis of DRF programs to a sequential analysis. This aids in rapidly porting existing sequential analyses to sound and scalable analyses for DRF programs. Next, we parameterize L-DRF with a partitioning of the program variables into "regions" which are accessed atomically. Abstractions of the region-parameterized semantics yield more precise analyses for "region-race" free concurrent programs. We instantiate these abstractions to devise efficient relational analyses for race free programs, which we have implemented in a prototype tool called RATCOP. On the benchmarks, RATCOP was able to prove up to 65% of the assertions, in comparison to 25% proved by our baseline. Moreover, in a comparative study with a recent concurrent static analyzer, RATCOP was up to 5 orders of magnitude faster.