Document Open Access Logo

Defining Correctness Conditions for Concurrent Objects in Multicore Architectures

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

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2015.470.pdf
  • Filesize: 0.72 MB
  • 25 pages

Document Identifiers

Author Details

Brijesh Dongol
John Derrick
Lindsay Groves
Graeme Smith

Cite AsGet BibTex

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)
https://doi.org/10.4230/LIPIcs.ECOOP.2015.470

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.
Keywords
  • Concurrent objects
  • correctness
  • relaxed memory
  • verification

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. S. V. Adve and K. Gharachorloo. Shared memory consistency models: A tutorial. IEEE Computer, 29(12):66-76, 1996. Google Scholar
  2. J. Alglave, L. Maranget, and M. Tautschnig. Herding cats: Modelling, simulation, testing, and data mining for weak memory. ACM Trans. Program. Lang. Syst., 36(2):7, 2014. Google Scholar
  3. H. Attiya, R. Guerraoui, D. Hendler, P. Kuznetsov, M. M. Michael, and M. T. Vechev. Laws of order: expensive synchronization in concurrent algorithms cannot be eliminated. In T. Ball and M. Sagiv, editors, POPL, pages 487-498. ACM, 2011. Google Scholar
  4. H. Attiya and J. L. Welch. Sequential consistency versus linearizability. ACM Trans. Comput. Syst., 12(2):91-122, 1994. Google Scholar
  5. M. Batty, M. Dodds, and A. Gotsman. Library abstraction for C/C++ concurrency. In R. Giacobazzi and R. Cousot, editors, POPL, pages 235-248. ACM, 2013. Google Scholar
  6. S. Burckhardt, A. Gotsman, M. Musuvathi, and H. Yang. Concurrent library correctness on the TSO memory model. In H. Seidl, editor, ESOP 2012, volume 7211 of LNCS, pages 87-107. Springer, 2012. Google Scholar
  7. D. Chase and Y. Lev. Dynamic circular work-stealing deque. In P. B. Gibbons and P. G. Spirakis, editors, SPAA, pages 21-28. ACM, 2005. Google Scholar
  8. R. Colvin, L. Groves, V. Luchangco, and M. Moir. Formal verification of a lazy concurrent list-based set. In CAV, volume 4144 of LNCS 4144, pages 475-488. Springer, 2006. Google Scholar
  9. J. Derrick, B. Dongol, G. Schellhorn, B. Tofan, O. Travkin, and H. Wehrheim. Quiescent consistency: Defining and verifying relaxed linearizability. In C. B. Jones, P. Pihlajasaari, and J. Sun, editors, FM, pages 200-214. Springer, 2014. Google Scholar
  10. J. Derrick, G. Schellhorn, and H. Wehrheim. Mechanically verified proof obligations for linearizability. ACM Trans. Program. Lang. Syst., 33(1):4, 2011. Google Scholar
  11. J. Derrick, G. Schellhorn, and H. Wehrheim. Verifying linearisabilty with potential linearisation points. In M. Butler and W. Schulte, editors, FM 2011, volume 6664 of LNCS, pages 323-337. Springer, 2011. Google Scholar
  12. J. Derrick, G. Smith, and B. Dongol. Verifying linearizability on TSO architectures. In E. Albert and E. Sekerinski, editors, iFM, pages 341-356. Springer, 2014. Google Scholar
  13. S. Doherty, D. Detlefs, L. Groves, C. H. Flood, V. Luchangco, P. A. Martin, M. Moir, N. Shavit, and G. L. Steele Jr. Dcas is not a silver bullet for nonblocking algorithm design. In P. B. Gibbons and M. Adler, editors, SPAA, pages 216-224. ACM, 2004. Google Scholar
  14. B. Dongol, O. Travkin, J. Derrick, and H. Wehrheim. A high-level semantics for program execution under Total Store Order memory. In Z. Liu, J. Woodcock, and H. Zhu, editors, ICTAC, volume 8049 of LNCS, pages 177-194. Springer, 2013. Google Scholar
  15. I. Filipovic, P. W. O'Hearn, N. Rinetzky, and H. Yang. Abstraction for concurrent objects. Theor. Comput. Sci., 411(51-52):4379-4398, 2010. Google Scholar
  16. M. Frigo, C. E. Leiserson, and K. H. Randall. The implementation of the cilk-5 multithreaded language. In J. W. Davidson, K. D. Cooper, and A. Michael Berman, editors, PLDI, pages 212-223. ACM, 1998. Google Scholar
  17. A. Gotsman, M. Musuvathi, and H. Yang. Show no weakness: Sequentially consistent specifications of TSO libraries. In M. Aguilera, editor, DISC 2012, volume 7611 of LNCS, pages 31-45. Springer, 2012. Google Scholar
  18. A. Gotsman and H. Yang. Linearizability with ownership transfer. Logical Methods in Computer Science, 9(3), 2013. Google Scholar
  19. R. Guerraoui and M. Kapalka. Principles of Transactional Memory. Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers, 2010. Google Scholar
  20. T. A. Henzinger, C. M. Kirsch, H. Payer, A. Sezgin, and Sokolova A. Quantitative relaxation of concurrent data structures. In R. Giacobazzi and R.dhia Cousot, editors, POPL, pages 317-328. ACM, 2013. Google Scholar
  21. T. A. Henzinger, A. Sezgin, and V. Vafeiadis. Aspect-oriented linearizability proofs. In P. R. D'Argenio and H. C. Melgratti, editors, CONCUR, pages 242-256. Springer, 2013. Google Scholar
  22. M. Herlihy and N. Shavit. \hspace*-0.5mmThe Art of Multiprocessor Programming. \hspace*-0.5mmMorgan Kaufmann, \hspace*-0.6mm2008. Google Scholar
  23. M. Herlihy and J. M. Wing. Linearizability: A correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst., 12(3):463-492, 1990. Google Scholar
  24. R. Jagadeesan, G. Petri, C. Pitcher, and J. Riely. Quarantining weakness - compositional reasoning under relaxed memory models (extended abstract). In Felleisen M and P. Gardner, editors, ESOP, volume 7792 of LNCS, pages 492-511. Springer, 2013. Google Scholar
  25. R. Jagadeesan and J. Riely. Between linearizability and quiescent consistency - quantitative quiescent consistency. In J. Esparza, P. Fraigniaud, T. Husfeldt, and E. Koutsoupias, editors, ICALP II, volume 8573 of LNCS, pages 220-231. Springer, 2014. Google Scholar
  26. L. Lamport. How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Computers, 28(9):690-691, 1979. Google Scholar
  27. F. Liu, N. Nedev, N. Prisadnikov, M. T. Vechev, and E. Yahav. Dynamic synthesis for relaxed memory models. In J. Vitek, H. Lin, and F. Tip, editors, PLDI, pages 429-440. ACM, 2012. Google Scholar
  28. S. Owens. Reasoning about the implementation of concurrency abstractions on x86-TSO. In T. D'Hondt, editor, ECOOP 2010, volume 6183 of LNCS, pages 478-503. Springer, 2010. Google Scholar
  29. G. Schellhorn, H. Wehrheim, and J. Derrick. A sound and complete proof technique for linearizability of concurrent data structures. ACM Trans. on Computational Logic, 2014. Google Scholar
  30. P. Sewell, S. Sarkar, S. Owens, F.Z. Nardelli, and M.O. Myreen. x86-TSO: a rigorous and usable programmer’s model for x86 multiprocessors. Commun. ACM, 53(7):89-97, 2010. Google Scholar
  31. N. Shavit. Data structures in the multicore age. Commun. ACM, 54(3):76-84, 2011. Google Scholar
  32. G. Smith, J. Derrick, and B. Dongol. Admit your weakness: Verifying correctness on TSO architectures. In FACS. Springer, 2014. To appear (accepted 21 July, 2014). Google Scholar
  33. D. J. Sorin, M. D. Hill, and D. A. Wood. A Primer on Memory Consistency and Cache Coherence. Synthesis Lectures on Computer Architecture. Morgan & Claypool, 2011. Google Scholar
  34. J.M. Spivey. The Z Notation: A Reference Manual. Prentice Hall, 1992. Google Scholar
  35. O. Travkin, A. Mütze, and H. Wehrheim. SPIN as a linearizability checker under weak memory models. In V. Bertacco and A. Legay, editors, HVC, volume 8244 of LNCS, pages 311-326. Springer, 2013. Google Scholar
  36. W. Vogels. Eventually consistent. Commun. ACM, 52(1):40-44, 2009. Google Scholar
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
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact