1 Search Results for "Groves, Lindsay"


Document
Defining Correctness Conditions for Concurrent Objects in Multicore Architectures

Authors: Brijesh Dongol, John Derrick, Lindsay Groves, and Graeme Smith

Published in: LIPIcs, Volume 37, 29th European Conference on Object-Oriented Programming (ECOOP 2015)


Abstract
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.

Cite as

Brijesh Dongol, John Derrick, Lindsay Groves, and Graeme Smith. Defining Correctness Conditions for Concurrent Objects in Multicore Architectures. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 470-494, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


Copy BibTex To Clipboard

@InProceedings{dongol_et_al:LIPIcs.ECOOP.2015.470,
  author =	{Dongol, Brijesh and Derrick, John and Groves, Lindsay and Smith, Graeme},
  title =	{{Defining Correctness Conditions for Concurrent Objects in Multicore Architectures}},
  booktitle =	{29th European Conference on Object-Oriented Programming (ECOOP 2015)},
  pages =	{470--494},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-86-6},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{37},
  editor =	{Boyland, John Tang},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.470},
  URN =		{urn:nbn:de:0030-drops-52348},
  doi =		{10.4230/LIPIcs.ECOOP.2015.470},
  annote =	{Keywords: Concurrent objects, correctness, relaxed memory, verification}
}
  • Refine by Author
  • 1 Derrick, John
  • 1 Dongol, Brijesh
  • 1 Groves, Lindsay
  • 1 Smith, Graeme

  • Refine by Classification

  • Refine by Keyword
  • 1 Concurrent objects
  • 1 correctness
  • 1 relaxed memory
  • 1 verification

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2015

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail