Thread-Local Semantics and Its Efficient Sequential Abstractions for Race-Free Programs

DOI10.1007/978-3-319-66706-5_13MaRDI QIDQ5233246zbMATH OpenOpenAlexFDO

Authors Suvam Mukherjee, Oded Padon, Sharon Shoham, Deepak D'Souza, Noam Rinetzky

Publication date 16 September 2019

Published in Static Analysis (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2009.02775

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55)

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.

Recommendations

• Local Reasoning for Storable Locks and Threads
• Precise thread-modular abstract interpretation of concurrent programs using relational interference abstractions
• Formalizing and checking thread refinement for data-race-free execution models
• Abstract local reasoning for concurrent libraries: mind the gap
• Non-preemptive semantics for data-race-free programs
• Locally abstract, globally concrete semantics of concurrent programming languages
• A Deadlock-Free Semantics for Shared Memory Concurrency
• Towards a thread-local proof technique for starvation freedom

Cited in

(7)

• Data-race and concurrent-write freedom are undecidable.
• Non-preemptive semantics for data-race-free programs
• Dataflow analysis for datarace-free programs
• Local Data Race Freedom with Non-multi-copy Atomicity
• Improving thread-modular abstract interpretation
• Formalizing and checking thread refinement for data-race-free execution models
• Clustered relational thread-modular abstract interpretation with local traces

This page was built for publication: Thread-Local Semantics and Its Efficient Sequential Abstractions for Race-Free Programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5233246)