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

Download:

Current browse context:

cs.LO

Change to browse by:

References & Citations

DBLP - CS Bibliography

Bookmark

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

Computer Science > Logic in Computer Science

Title: Safety Verification of Parameterized Systems under Release-Acquire

Abstract: We study the safety verification problem for parameterized systems under the release-acquire (RA) semantics. It has been shown that the problem is intractable for systems with unlimited access to atomic compare-and-swap (CAS) instructions. We show that, from a verification perspective where approximate results help, this is overly pessimistic. We study parameterized systems consisting of an unbounded number of environment threads executing identical but CAS-free programs and a fixed number of distinguished threads that are unrestricted.
Our first contribution is a new semantics that considerably simplifies RA but is still equivalent for the above systems as far as safety verification is concerned. We apply this (general) result to two subclasses of our model. We show that safety verification is only \pspace-complete for the bounded model checking problem where the distinguished threads are loop-free. Interestingly, we can still afford the unbounded environment. We show that the complexity jumps to \nexp-complete for thread-modular verification where an unrestricted distinguished `ego' thread interacts with an environment of CAS-free threads plus loop-free distinguished threads (as in the earlier setting). Besides the usefulness for verification, the results are strong in that they delineate the tractability border for an established semantics.
Subjects: Logic in Computer Science (cs.LO); Programming Languages (cs.PL)
Cite as: arXiv:2101.12123 [cs.LO]
  (or arXiv:2101.12123v2 [cs.LO] for this version)

Submission history

From: Shankara Narayanan Krishna [view email]
[v1] Thu, 28 Jan 2021 17:13:14 GMT (243kb,D)
[v2] Thu, 5 May 2022 17:10:26 GMT (996kb,D)

Link back to: arXiv, form interface, contact.