Thread-Local Semantics and its Efficient Sequential Abstractions for Race-Free Programs
Authors: Suvam Mukherjee, Oded Padon, Sharon Shoham, Deepak D'Souza, Noam Rinetzky
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, and which are in the same
spirit as the ``sync-CFG'' analysis originally proposed in [De2011]. To achieve
this, we first propose a novel concrete semantics for DRF programs called L-DRF that
is thread-local in nature with each thread operating 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
scalable analyses for DRF programs. Next, we parameterize the semantics 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 upto 65% of the assertions, in
comparison to 25% proved by a version of the analysis from [De2011].
pdf