Sökning: onr:"swepub:oai:DiVA.org:uu-398252" >
Verification of pro...
Verification of programs under the release-acquire semantics
-
- Abdulla, Parosh Aziz, Professor (författare)
- Uppsala universitet,Datorteknik,Avdelningen för datorteknik
-
Arora, Jatin (författare)
-
- Atig, Mohamed Faouzi (författare)
- Uppsala universitet,Datorteknik,Avdelningen för datorteknik
-
visa fler...
-
Krishna, Shankaranarayanan (författare)
-
visa färre...
-
(creator_code:org_t)
- 2019-06-08
- 2019
- Engelska.
-
Ingår i: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. - New York, NY, USA : Association for Computing Machinery (ACM). - 9781450367127 ; , s. 1117-1132
- Relaterad länk:
-
https://urn.kb.se/re...
-
visa fler...
-
https://doi.org/10.1...
-
visa färre...
Abstract
Ämnesord
Stäng
- We address the verification of concurrent programs running under the release-acquire (RA) semantics. We show that the reachability problem is undecidable even in the case where the input program is finite-state. Given this undecidability, we follow the spirit of the work on context-bounded analysis for detecting bugs in programs under the classical SC model, and propose an under-approximate reachability analysis for the case of RA. To this end, we propose a novel notion, called view-switching, and provide a code-to-code translation from an input program under RA to a program under SC. This leads to a reduction, in polynomial time, of the bounded view-switching reachability problem under RA to the bounded context-switching problem under SC. We have implemented a prototype tool VBMC and tested it on a set of benchmarks, demonstrating that many bugs in programs can be found using a small number of view switches.
Ämnesord
- NATURVETENSKAP -- Data- och informationsvetenskap -- Datavetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Computer Sciences (hsv//eng)
Nyckelord
- Model-Checking
- weak memory models
- RA
Publikations- och innehållstyp
- ref (ämneskategori)
- kon (ämneskategori)
Hitta via bibliotek
Till lärosätets databas