Sökning: onr:"swepub:oai:DiVA.org:liu-92596" >
Memorax, a Precise ...
Memorax, a Precise and Sound Tool for Automatic Fence Insertion under TSO
-
- Abdulla, Parosh Aziz (författare)
- Uppsala universitet,Datorteknik,Uppsala University, Sweden
-
- Atig, Mohamed Faouzi (författare)
- Uppsala universitet,Datorteknik,Uppsala University, Sweden
-
- Chen, Yu-Fang (författare)
- Academia Sinica, Taiwan
-
visa fler...
-
- Leonardsson, Carl (författare)
- Uppsala universitet,Datorteknik,Uppsala University, Sweden
-
- Rezine, Ahmed (författare)
- Linköpings universitet,Programvara och system,Tekniska högskolan,Linköping University
-
visa färre...
-
(creator_code:org_t)
- Berlin, Heidelberg : Springer Berlin/Heidelberg, 2013
- 2013
- Engelska.
-
Ingår i: Tools and Algorithms for the Construction and Analysis of Systems. - Berlin, Heidelberg : Springer Berlin/Heidelberg. - 9783642367410 - 9783642367427 ; , s. 530-536
- Relaterad länk:
-
https://link.springe...
-
visa fler...
-
https://uu.diva-port... (primary) (Raw object)
-
https://urn.kb.se/re...
-
https://doi.org/10.1...
-
https://urn.kb.se/re...
-
visa färre...
Abstract
Ämnesord
Stäng
- We introduce MEMORAX, a tool for the verification of control state reachability (i.e., safety properties) of concurrent programs manipulating finite range and integer variables and running on top of weak memory models. The verification task is non-trivial as it involves exploring state spaces of arbitrary or even infinite sizes. Even for programs that only manipulate finite range variables, the sizes of the store buffers could grow unboundedly, and hence the state spaces that need to be explored could be of infinite size. In addition, MEMORAX in- corporates an interpolation based CEGAR loop to make possible the verification of control state reachability for concurrent programs involving integer variables. The reachability procedure is used to automatically compute possible memory fence placements that guarantee the unreachability of bad control states under TSO. In fact, for programs only involving finite range variables and running on TSO, the fence insertion functionality is complete, i.e., it will find all minimal sets of memory fence placements (minimal in the sense that removing any fence would result in the reachability of the bad control states). This makes MEMORAX the first freely available, open source, push-button verification and fence insertion tool for programs running under TSO with integer variables.
Ämnesord
- NATURVETENSKAP -- Data- och informationsvetenskap -- Datavetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Computer Sciences (hsv//eng)
- NATURVETENSKAP -- Data- och informationsvetenskap -- Programvaruteknik (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Software Engineering (hsv//eng)
Nyckelord
- TECHNOLOGY
- TEKNIKVETENSKAP
Publikations- och innehållstyp
- ref (ämneskategori)
- kon (ämneskategori)
Hitta via bibliotek
Till lärosätets databas