Sökning: onr:"swepub:oai:DiVA.org:uu-474510" >
The Decidability of...
The Decidability of Verification under PS 2.0
-
- Abdulla, Parosh Aziz, Professor, 1961- (författare)
- Uppsala universitet,Datorteknik,Avdelningen för datorteknik
-
- Atig, Mohamed Faouzi (författare)
- Uppsala universitet,Datorteknik,Avdelningen för datorteknik
-
- Godbole, Adwait (författare)
- Indian Inst Technol, Mumbai, Maharashtra, India.
-
visa fler...
-
- Krishna, S. (författare)
- Indian Inst Technol, Mumbai, Maharashtra, India.
-
- Vafeiadis, Viktor (författare)
- MPI SWS, Kaiserslautern, Germany.
-
visa färre...
-
(creator_code:org_t)
- 2021-03-23
- 2021
- Engelska.
-
Ingår i: Programming Languages And Systems, ESOP 2021. - Cham : Springer Nature. - 9783030720193 - 9783030720186 ; , s. 1-29
- Relaterad länk:
-
https://doi.org/10.1...
-
visa fler...
-
https://uu.diva-port... (primary) (Raw object)
-
https://library.oape...
-
https://urn.kb.se/re...
-
https://doi.org/10.1...
-
visa färre...
Abstract
Ämnesord
Stäng
- 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.
Ämnesord
- NATURVETENSKAP -- Data- och informationsvetenskap -- Datavetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Computer Sciences (hsv//eng)
Nyckelord
- Model-Checking
- Memory Models
- Promising Semantics
Publikations- och innehållstyp
- ref (ämneskategori)
- kon (ämneskategori)
Hitta via bibliotek
Till lärosätets databas