Defining correctness conditions for concurrent objects in multicore architectures

Dongol, Brijesh, Derrick, John, Groves, Lindsay and Smith, Graeme (2015). Defining correctness conditions for concurrent objects in multicore architectures. In: John Tang Boyland, 29th European Conference on Object-Oriented Programming, ECOOP 2015. 29th European Conference on Object-Oriented Programming, ECOOP 2015, Prague, Czech Republic, (470-494). 5-10 July 2015. doi:10.4230/LIPIcs.ECOOP.2015.470


Author Dongol, Brijesh
Derrick, John
Groves, Lindsay
Smith, Graeme
Title of paper Defining correctness conditions for concurrent objects in multicore architectures
Conference name 29th European Conference on Object-Oriented Programming, ECOOP 2015
Conference location Prague, Czech Republic
Conference dates 5-10 July 2015
Convener Boyland, John Tang
Proceedings title 29th European Conference on Object-Oriented Programming, ECOOP 2015   Check publisher's open access policy
Journal name Leibniz International Proceedings in Informatics, LIPIcs   Check publisher's open access policy
Series Leibniz International Proceedings in Informatics, LIPIcs
Place of Publication Wadern, Germany
Publisher Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Publication Year 2015
Sub-type Fully published paper
DOI 10.4230/LIPIcs.ECOOP.2015.470
Open Access Status DOI
ISBN 9783939897866
ISSN 1868-8969
Editor John Tang Boyland
Volume 37
Start page 470
End page 494
Total pages 25
Chapter number 23
Total chapters 35
Collection year 2016
Language eng
Abstract/Summary Correctness of concurrent objects is defined in terms of conditions that determine allowable relationships between histories of a concurrent object and those of the corresponding sequential object. Numerous correctness conditions have been proposed over the years, and more have been proposed recently as the algorithms implementing concurrent objects have been adapted to cope with multicore processors with relaxed memory architectures. We present a formal framework for defining correctness conditions for multicore architectures, covering both standard conditions for totally ordered memory and newer conditions for relaxed memory, which allows them to be expressed in uniform manner, simplifying comparison. Our framework distinguishes between order and commitment properties, which in turn enables a hierarchy of correctness conditions to be established. We consider the Total Store Order (TSO) memory model in detail, formalise known conditions for TSO using our framework, and develop sequentially consistent variations of these. We present a work-stealing deque for TSO memory that is not linearizable, but is correct with respect to these new conditions. Using our framework, we identify a new non-blocking compositional condition, fence consistency, which lies between known conditions for TSO, and aims to capture the intention of a programmer-specified fence.
Keyword Concurrent objects
Correctness
Relaxed memory
Verification
Q-Index Code C1
Q-Index Status Provisional Code
Institutional Status UQ

 
Versions
Version Filter Type
Citation counts: Scopus Citation Count Cited 4 times in Scopus Article | Citations
Google Scholar Search Google Scholar
Created: Tue, 08 Mar 2016, 14:22:29 EST by System User on behalf of School of Information Technol and Elec Engineering