We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:


Current browse context:


Change to browse by:


References & Citations

DBLP - CS Bibliography


(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Programming Languages

Title: Thread-modular Analysis of Release-Acquire Concurrency

Abstract: We present a thread-modular abstract interpretation(TMAI) technique to verify programs under the release-acquire (RA) memory model for safety property violations. The main contributions of our work are: we capture the execution order of program statements as an abstract domain, and propose a sound upper approximation over this domain to efficiently reason over RA concurrency. The proposed domain is general in its application and captures the ordering relations as a first-class feature in the abstract interpretation theory. In particular, the domain represents a set of sequences of modifications of a global variable in concurrent programs as a partially ordered set. Under this approximation, older sequenced-before stores of a global variable are forgotten and only the latest stores per variable are preserved. We establish the soundness of our proposed abstractions and implement them in a prototype abstract interpreter called PRIORI. The evaluations of PRIORI on existing and challenging RA benchmarks demonstrate that the proposed technique is not only competitive in refutation, but also in verification. PRIORI shows significantly fast analysis runtimes with higher precision compared to recent state-of-the-art tools for RA concurrency.
Subjects: Programming Languages (cs.PL)
Cite as: arXiv:2107.02346 [cs.PL]
  (or arXiv:2107.02346v3 [cs.PL] for this version)

Submission history

From: Divyanjali Sharma [view email]
[v1] Tue, 6 Jul 2021 02:08:09 GMT (405kb)
[v2] Sat, 10 Jul 2021 07:34:30 GMT (401kb)
[v3] Tue, 17 Aug 2021 18:19:35 GMT (461kb)

Link back to: arXiv, form interface, contact.