Search: onr:"swepub:oai:DiVA.org:uu-474510" >
The Decidability of...
The Decidability of Verification under PS 2.0
-
- Abdulla, Parosh Aziz, Professor, 1961- (author)
- Uppsala universitet,Datorteknik,Avdelningen för datorteknik
-
- Atig, Mohamed Faouzi (author)
- Uppsala universitet,Datorteknik,Avdelningen för datorteknik
-
- Godbole, Adwait (author)
- Indian Inst Technol, Mumbai, Maharashtra, India.
-
show more...
-
- Krishna, S. (author)
- Indian Inst Technol, Mumbai, Maharashtra, India.
-
- Vafeiadis, Viktor (author)
- MPI SWS, Kaiserslautern, Germany.
-
show less...
-
(creator_code:org_t)
- 2021-03-23
- 2021
- English.
-
In: Programming Languages And Systems, ESOP 2021. - Cham : Springer Nature. - 9783030720193 - 9783030720186 ; , s. 1-29
- Related links:
-
https://doi.org/10.1...
-
show more...
-
https://uu.diva-port... (primary) (Raw object)
-
https://library.oape...
-
https://urn.kb.se/re...
-
https://doi.org/10.1...
-
show less...
Abstract
Subject headings
Close
- We consider the reachability problem for finite-state multi-threaded programs under the promising semantics (PS 2.0) of Lee et al., which captures most common program transformations. Since reachability is already known to be undecidable in the fragment of PS 2.0 with only release-acquire accesses (PS 2.0-ra), we consider the fragment with only relaxed accesses and promises (PS 2.0-rlx). We show that reachability under PS 2.0-rlx is undecidable in general and that it becomes decidable, albeit non-primitive recursive, if we bound the number of promises. Given these results, we consider a bounded version of the reachability problem. To this end, we bound both the number of promises and of "view-switches", i.e., the number of times the processes may switch their local views of the global memory. We provide a code-to-code translation from an input program under PS 2.0 (with relaxed and release-acquire memory accesses along with promises) to a program under SC, thereby reducing the bounded reachability problem under PS 2.0 to the bounded context-switching problem under SC. We have implemented a tool and tested it on a set of benchmarks, demonstrating that typical bugs in programs can be found with a small bound.
Subject headings
- NATURVETENSKAP -- Data- och informationsvetenskap -- Datavetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Computer Sciences (hsv//eng)
Keyword
- Model-Checking
- Memory Models
- Promising Semantics
Publication and Content Type
- ref (subject category)
- kon (subject category)
Find in a library
To the university's database