Search: onr:"swepub:oai:DiVA.org:uu-366357" >
Replacing store buf...
Replacing store buffers by load buffers in TSO
-
- Abdulla, Parosh Aziz, Professor (author)
- Uppsala universitet,Datorteknik,Avdelningen för datorteknik
-
- Atig, Mohamed Faouzi (author)
- Uppsala universitet,Datorteknik,Avdelningen för datorteknik
-
Bouajjani, Ahmed (author)
-
show more...
-
- Ngo, Tuan Phong (author)
- Uppsala universitet,Datorteknik,Avdelningen för datorteknik
-
show less...
-
(creator_code:org_t)
- 2018-08-31
- 2018
- English.
-
In: Verification and Evaluation of Computer and Communication Systems. - Cham : Springer. - 9783030003586 - 9783030003593 ; , s. 22-28
- Related links:
-
https://urn.kb.se/re...
-
show more...
-
https://doi.org/10.1...
-
show less...
Abstract
Subject headings
Close
- We consider the weak memory model of Total Store Ordering (TSO). In the classical definition of TSO, an unbounded buffer is inserted between each process and the shared memory. The buffers contains pending store operations of the processes. We introduce a new model where we replace the store buffers by load buffers. In contrast to the classical model, the buffers now contain load operations. We show that the models have equivalent behaviors in the sense that the processes reach identical sets of states when the input program is run under the two models.
Subject headings
- TEKNIK OCH TEKNOLOGIER -- Elektroteknik och elektronik -- Datorsystem (hsv//swe)
- ENGINEERING AND TECHNOLOGY -- Electrical Engineering, Electronic Engineering, Information Engineering -- Computer Systems (hsv//eng)
Keyword
- Program verification
- Weak memory models
- TSO
Publication and Content Type
- ref (subject category)
- kon (subject category)
Find in a library
To the university's database