Sökning: onr:"swepub:oai:DiVA.org:uu-510185" >
Consistency and Per...
Consistency and Persistency in Program Verification : Challenges and Opportunities
-
- Abdulla, Parosh, Professor, 1961- (författare)
- Uppsala universitet,Avdelningen för datorteknik,Datorteknik
-
- Atig, Mohamed Faouzi (författare)
- Uppsala universitet,Avdelningen för datorteknik,Datorteknik
-
- Bouajjani, Ahmed (författare)
- Université Paris Cité
-
visa fler...
-
- Jonsson, Bengt, 1957- (författare)
- Uppsala universitet,Datorteknik,Avdelningen för datorteknik
-
- Kumar, K. Narayan (författare)
- Chennai Mathematical Institute, Chennai, India
-
- Saivasan, Prakash (författare)
- The Institute of Mathematical Sciences
-
visa färre...
-
(creator_code:org_t)
- 2022-12-29
- 2022
- Engelska.
-
Ingår i: Principles of Systems Design. - Cham : Springer. - 9783031223365 - 9783031223372 ; , s. 494-510
- Relaterad länk:
-
https://urn.kb.se/re...
-
visa fler...
-
https://doi.org/10.1...
-
visa färre...
Abstract
Ämnesord
Stäng
- We consider the verification of concurrent programs and, in particular, the challenges that arise because modern platforms only guarantee weak semantics, i.e., semantics that are weaker than the classical Sequential Consistency (SC). We describe two architectural concepts that give rise to weak semantics, namely weak consistency and weak persistency. The former defines the order in which operations issued by a given process become visible to the rest of the processes. The latter prescribes the order in which data becomes persistent. To deal with the extra complexity in program behaviors that arises due to weak semantics, we propose translating the program verification problem under weak semantics to SC. The main principle is to augment the program with a set of (unbounded) data structures that guarantee the equivalence of the source program’s behavior under the weak semantics with the augmented program’s behavior under the SC semantics. Such an equivalence opens the door to leverage, albeit in a non-trivial manner, the rich set of techniques that we have developed over the years for program verification under the SC semantics. We illustrate the framework’s potential by considering the persistent version of the well-known Total Store Order semantics. We show that we can capture the program behaviors on such a platform using a finite set of unbounded monotone FIFO buffers. The use of monotone FIFO buffers allows the use of the well-structured-systems framework to prove the decidability of the reachability problem.
Ämnesord
- NATURVETENSKAP -- Data- och informationsvetenskap -- Datavetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Computer Sciences (hsv//eng)
Nyckelord
- Computer Science
- Datavetenskap
Publikations- och innehållstyp
- vet (ämneskategori)
- kap (ämneskategori)
Hitta via bibliotek
Till lärosätets databas