Reasoning algebraically about refinement on TSO architectures

Dongol, Brijesh, Derrick, John and Smith, Graeme (2014). Reasoning algebraically about refinement on TSO architectures. In: Gabriel Ciobanu and Dominique Méry, Theoretical Aspects of Computing – ICTAC 2014. International Colloquium on Theoretical Aspects of Computing, Bucharest, Romania, (151-168). 17-19 September 2014. doi:10.1007/978-3-319-10882-7_10

Attached Files (Some files may be inaccessible until you login with your UQ eSpace credentials)
Name Description MIMEType Size Downloads

Author Dongol, Brijesh
Derrick, John
Smith, Graeme
Title of paper Reasoning algebraically about refinement on TSO architectures
Conference name International Colloquium on Theoretical Aspects of Computing
Conference location Bucharest, Romania
Conference dates 17-19 September 2014
Proceedings title Theoretical Aspects of Computing – ICTAC 2014   Check publisher's open access policy
Journal name Lecture Notes in Computer Science   Check publisher's open access policy
Series Lecture Notes in Computer Science
Place of Publication Cham, Switzerland
Publisher Springer
Publication Year 2014
Sub-type Fully published paper
DOI 10.1007/978-3-319-10882-7_10
Open Access Status Not Open Access
ISBN 9783319108810
ISSN 1611-3349
Editor Gabriel Ciobanu
Dominique Méry
Volume 8687
Start page 151
End page 168
Total pages 18
Abstract/Summary The Total Store Order memory model is widely implemented by modern multicore architectures such as x86, where local buffers are used for optimisation, allowing limited forms of instruction reordering. The presence of buffers and hardware-controlled buffer flushes increases the level of non-determinism from the level specified by a program, complicating the already difficult task of concurrent programming. This paper presents a new notion of refinement for weak memory models, based on the observation that pending writes to a process’ local variables may be treated as if the effect of the update has already occurred in shared memory. We develop an interval-based model with algebraic rules for various programming constructs. In this framework, several decomposition rules for our new notion of refinement are developed. We apply our approach to verify the spinlock algorithm from the literature.
Q-Index Code C1
Q-Index Status Confirmed Code
Institutional Status UQ

Version Filter Type
Citation counts: Scopus Citation Count Cited 0 times in Scopus Article
Google Scholar Search Google Scholar
Created: Mon, 02 Mar 2015, 19:50:30 EST by Graeme Smith on behalf of School of Information Technol and Elec Engineering