More Web Proxy on the site http://driver.im/

research-article

Open access

On library correctness under weak memory consistency: specifying and verifying concurrent libraries under declarative consistency models

Authors:

Viktor VafeiadisAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 3, Issue POPL

Article No.: 68, Pages 1 - 31

https://doi.org/10.1145/3290381

Published: 02 January 2019 Publication History

Abstract

Concurrent libraries are the building blocks for concurrency. They encompass a range of abstractions (locks, exchangers, stacks, queues, sets) built in a layered fashion: more advanced libraries are built out of simpler ones. While there has been a lot of work on verifying such libraries in a sequentially consistent (SC) environment, little is known about how to specify and verify them under weak memory consistency (WMC).

We propose a general declarative framework that allows us to specify concurrent libraries declaratively, and to verify library implementations against their specifications compositionally. Our framework is sufficient to encode standard models such as SC, (R)C11 and TSO. Additionally, we specify several concurrent libraries, including mutual exclusion locks, reader-writer locks, exchangers, queues, stacks and sets. We then use our framework to verify multiple weakly consistent implementations of locks, exchangers, queues and stacks.

Supplementary Material

WEBM File (a68-raad.webm)

Download
81.30 MB

References

[1]

Parosh Aziz Abdulla, Stavros Aronis, Mohamed Faouzi Atig, Bengt Jonsson, Carl Leonardsson, and Konstantinos Sagonas. 2017. Stateless model checking for TSO and PSO. Acta Inf. 54, 8 (2017), 789–818.

Digital Library

[2]

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bengt Jonsson, and Tuan Phong Ngo. 2018. Optimal stateless model checking under the release-acquire semantics. Proc. ACM Program. Lang. 2, OOPSLA, Article 135 (Oct. 2018), 29 pages.

Digital Library

[3]

Jade Alglave and Patrick Cousot. 2017. Ogre and Pythia: An invariance proof method for weak consistency models. In POPL 2017. ACM, New York, NY, USA, 3–18.

Digital Library

[4]

Jade Alglave, Luc Maranget, Paul E. McKenney, Andrea Parri, and Alan S. Stern. 2018. Frightening small children and disconcerting grown-ups: Concurrency in the Linux kernel. In ASPLOS 2018. ACM, New York, NY, USA, 405–418.

Digital Library

[5]

Jade Alglave, Luc Maranget, and Michael Tautschnig. 2014. Herding cats: Modelling, simulation, testing, and data mining for weak memory. ACM Trans. Program. Lang. Syst. 36, 2, Article 7 (July 2014), 74 pages.

Digital Library

[6]

Mark Batty, Mike Dodds, and Alexey Gotsman. 2013. Library abstraction for C/C++ concurrency. In POPL 2013. ACM, New York, NY, USA, 235–248.

Digital Library

[7]

Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, and Tjark Weber. 2011. Mathematizing C++ concurrency. In POPL 2011. ACM, New York, NY, USA, 55–66.

Digital Library

[8]

Hans-J. Boehm and Brian Demsky. 2014. Outlawing ghosts: Avoiding out-of-thin-air results. In MSPC 2014. ACM, New York, NY, USA, Article 7, 6 pages.

Digital Library

[9]

Ahmed Bouajjani, Egor Derevenetc, and Roland Meyer. 2013. Checking and enforcing robustness against TSO. In ESOP (LNCS), Vol. 7792. Springer, Heidelberg, Germany, 533–553.

Digital Library

[10]

Ahmed Bouajjani, Constantin Enea, and Chao Wang. 2017. Checking linearizability of concurrent priority queues. In CONCUR 2017 (LIPIcs), Vol. 85. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 16:1–16:16.

[11]

Ahmed Bouajjani, Roland Meyer, and Eike Möhlmann. 2011. Deciding robustness against total store ordering. In ICALP (2) (LNCS), Vol. 6756. Springer, Heidelberg, Germany, 428–440.

Digital Library

[12]

Sebastian Burckhardt, Alexey Gotsman, Madanlal Musuvathi, and Hongseok Yang. 2012. Concurrent Library Correctness on the TSO Memory Model. In ESOP 2012 (LNCS), Vol. 7211. Springer, Heidelberg, Germany, 87–107.

Digital Library

[13]

Sebastian Burckhardt, Alexey Gotsman, Hongseok Yang, and Marek Zawirski. 2014. Replicated data types: Specification, verification, optimality. In POPL 2014. ACM, New York, NY, USA, 271–284.

Digital Library

[14]

Armando Castañeda, Sergio Rajsbaum, and Michel Raynal. 2015. Specifying concurrent problems: Beyond linearizability and up to tasks. In DISC 2015 (LNCS), Vol. 9363. Springer, Heidelberg, Germany, 420–435.

Digital Library

[15]

Andrea Cerone, Giovanni Bernardi, and Alexey Gotsman. 2015. A framework for transactional consistency models with atomic visibility. In CONCUR 2015 (LIPIcs), Vol. 42. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 58–71.

[16]

Soham Chakraborty, Thomas A. Henzinger, Ali Sezgin, and Viktor Vafeiadis. 2015. Aspect-oriented linearizability proofs. Logical Methods in Computer Science 11, 1 (2015).

[17]

Thomas Dinsdale-Young, Mike Dodds, Philippa Gardner, Matthew J. Parkinson, and Viktor Vafeiadis. 2010. Concurrent abstract predicates. In ECOOP 2010 (LNCS), Vol. 6183. Springer, Heidelberg, Germany, 504–528.

Digital Library

[18]

Simon Doherty, Brijesh Dongol, Heike Wehrheim, and John Derrick. 2018. Making linearizability compositional for partially ordered executions. In IFM 2018 (LNCS), Vol. 11023. Springer, Heidelberg, Germany, 110–129.

[19]

Marko Doko and Viktor Vafeiadis. 2016. A program logic for C11 memory fences. In VMCAI 2016 (LNCS), Vol. 9583. Springer, Heidelberg, Germany, 413–430.

Digital Library

[20]

Marko Doko and Viktor Vafeiadis. 2017. Tackling real-life relaxed concurrency with FSL++. In ESOP 2017 (LNCS), Vol. 10201. Springer, Heidelberg, Germany, 448–475.

[21]

Brijesh Dongol, Radha Jagadeesan, James Riely, and Alasdair Armstrong. 2018. On abstraction and compositionality for weak-memory linearisability. In VMCAI 2018 (LNCS), Vol. 10747. Springer, Heidelberg, Germany, 183–204.

[22]

Nir Hemed, Noam Rinetzky, and Viktor Vafeiadis. 2015. Modular verification of concurrency-aware linearizability. In DISC 2015 (LNCS), Vol. 9363. Springer, Heidelberg, Germany, 371–387.

Digital Library

[23]

Danny Hendler, Nir Shavit, and Lena Yerushalmi. 2004. A scalable lock-free stack algorithm. In SPAA 2004. ACM, New York, NY, USA, 206–215.

Digital Library

[24]

Maurice Herlihy and Jeannette M. Wing. 1990. Linearizability: A correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. 12, 3 (1990), 463–492.

Digital Library

[25]

Jan-Oliver Kaiser, Hoang-Hai Dang, Derek Dreyer, Ori Lahav, and Viktor Vafeiadis. 2017. Strong logic for weak memory: Reasoning about release-acquire consistency in Iris. In ECOOP 2017 (LIPIcs), Vol. 74. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 17:1–17:29.

[26]

Michalis Kokologiannakis, Ori Lahav, Konstantinos Sagonas, and Viktor Vafeiadis. 2018. Effective stateless model checking for C/C++ concurrency. Proc. ACM Program. Lang. 2, POPL (2018), 17:1–17:32.

Digital Library

[27]

Robbert Krebbers, Ralf Jung, Aleš Bizjak, Jacques-Henri Jourdan, Derek Dreyer, and Lars Birkedal. 2017. The essence of higher-order concurrent separation logic. In ESOP 2017 (LNCS), Vol. 10201. Springer, Heidelberg, Germany, 696–723.

Digital Library

[28]

Ori Lahav, Nick Giannarakis, and Viktor Vafeiadis. 2016. Taming release-acquire consistency. In POPL 2016. ACM, New York, NY, USA, 649–662.

Digital Library

[29]

Ori Lahav and Viktor Vafeiadis. 2015. Owicki-Gries reasoning for weak memory models. In ICALP 2015 (LNCS), Vol. 9135. Springer, Heidelberg, Germany, 311–323.

Digital Library

[30]

Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, and Derek Dreyer. 2017. Repairing sequential consistency in C/C++11. In PLDI 2017. ACM, New York, NY, USA, 618–632.

Digital Library

[31]

Leslie Lamport. 1979. How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Computers 28, 9 (Sept. 1979), 690–691.

Digital Library

[32]

Leslie Lamport. 1986. On interprocess communication. Distributed Computing 1, 2 (01 Jun 1986), 77–85.

[33]

Xavier Leroy. 2009. A formally verified compiler back-end. J. Autom. Reasoning 43, 4 (2009), 363–446.

Digital Library

[34]

Jeremy Manson, William Pugh, and Sarita V. Adve. 2005. The Java memory model. In POPL’05. ACM, New York, NY, USA, 378–391.

Digital Library

[35]

Aleksandar Nanevski, Ruy Ley-Wild, Ilya Sergey, and Germán Andrés Delbianco. 2014. Communicating state transition systems for fine-grained concurrent resources. In ESOP 2014 (LNCS), Vol. 8410. Springer, Heidelberg, Germany, 290–310.

Digital Library

[36]

Gil Neiger. 1994. Set-Linearizability. In PODC 1994. ACM, New York, NY, USA, 396.

Digital Library

[37]

Brian Norris and Brian Demsky. 2016. A practical approach for model checking C/C++11 code. ACM Trans. Program. Lang. Syst. 38, 3, Article 10 (May 2016), 51 pages.

Digital Library

[38]

Scott Owens, Susmit Sarkar, and Peter Sewell. 2009. A Better x86 Memory Model: x86-TSO. In TPHOLs 2009. Springer, Heidelberg, Germany, 391–407.

Digital Library

[39]

Matthieu Perrin, Achour Mostéfaoui, and Claude Jard. 2015. Update consistency for wait-free concurrent objects. In IPDPS 2015. IEEE Computer Society, Piscataway, NJ, USA, 219–228.

Digital Library

[40]

Christopher Pulte, Shaked Flur, Will Deacon, Jon French, Susmit Sarkar, and Peter Sewell. 2018. Simplifying ARM concurrency: Multicopy-atomic axiomatic and operational models for ARMv8. Proc. ACM Program. Lang. 2, POPL (2018), 19:1–19:29.

Digital Library

[41]

Azalea Raad, Marko Doko, Lovro Rožić, Ori Lahav, and Viktor Vafeiadis. 2018. Technical appendix. http://plv.mpi- sws.org/ yacovet/

[42]

Azalea Raad, Jules Villard, and Philippa Gardner. 2015. CoLoSL: Concurrent local subjective logic. In ESOP 2015 (LNCS), Vol. 9032. Springer, Heidelberg, Germany, 710–735.

[43]

Tom Ridge. 2010. A rely-guarantee proof system for x86-TSO. In VSTTE 2010 (LNCS), Vol. 6217. Springer, Heidelberg, Germany, 55–70.

Digital Library

[44]

Amr Sabry and Matthias Felleisen. 1993. Reasoning about programs in continuation-passing style. LISP and Symbolic Computation 6, 3 (01 Nov 1993), 289–360.

Digital Library

[45]

Ilya Sergey, Aleksandar Nanevski, and Anindya Banerjee. 2015. Specifying and verifying concurrent algorithms with histories and subjectivity. In ESOP 2015 (LNCS), Vol. 9032. Springer, Heidelberg, Germany, 333–358.

Digital Library

[46]

Nir Shavit. 2011. Data structures in the multicore age. Commun. ACM 54, 3 (March 2011), 76–84.

Digital Library

[47]

Filip Sieczkowski, Kasper Svendsen, Lars Birkedal, and Jean Pichon-Pharabod. 2015. A separation logic for fictional sequential consistency. In ESOP 2015 (LNCS), Vol. 9032. Springer, Heidelberg, Germany, 736–761.

[48]

Kasper Svendsen, Jean Pichon-Pharabod, Marko Doko, Ori Lahav, and Viktor Vafeiadis. 2018. A separation logic for a promising semantics. In ESOP 2018 (LNCS), Vol. 10801. Springer, Heidelberg, Germany, 357–384.

[49]

Joseph Tassarotti, Derek Dreyer, and Viktor Vafeiadis. 2015. Verifying read-copy-update in a logic for weak memory. In PLDI 2015. ACM, New York, NY, USA, 110–120.

Digital Library

[50]

Aaron Turon, Viktor Vafeiadis, and Derek Dreyer. 2014. GPS: Navigating weak memory with ghosts, protocols, and separation. In OOPSLA 2014. ACM, New York, NY, USA, 691–707.

Digital Library

[51]

Viktor Vafeiadis. 2010. Automatically proving linearizability. In CAV (LNCS), Vol. 6174. Springer, Heidelberg, Germany, 450–464.

Digital Library

[52]

Viktor Vafeiadis and Chinmay Narayan. 2013. Relaxed Separation Logic: A program logic for C11 concurrency. In OOPSLA 2013. ACM, New York, NY, USA, 867–884.

Digital Library

[53]

He Zhu, Gustavo Petri, and Suresh Jagannathan. 2015. Poling: SMT aided linearizability proofs. In CAV 2015 (LNCS), Vol. 9207. Springer, Heidelberg, Germany, 3–19.

Cited By

Nagar KSahoo AChowdhury RJagannathan S(2024)Automated Robustness Verification of Concurrent Data Structure Libraries against Relaxed Memory ModelsProceedings of the ACM on Programming Languages10.1145/36898028:OOPSLA2(2578-2605)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689802
Park SKim JMulder IJung JLee JKrebbers RKang J(2024)A Proof Recipe for Linearizability in Relaxed Memory Separation LogicProceedings of the ACM on Programming Languages10.1145/36563848:PLDI(175-198)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656384
Vafeiadi Bila EDongol B(2024)A verified durable transactional mutex lock for persistent x86-TSOFormal Methods in System Design10.1007/s10703-024-00462-1Online publication date: 31-Jul-2024
https://doi.org/10.1007/s10703-024-00462-1
Show More Cited By

Index Terms

On library correctness under weak memory consistency: specifying and verifying concurrent libraries under declarative consistency models
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
2. Theory of computation
  1. Models of computation
    1. Concurrency
  2. Semantics and reasoning

Recommendations

Using temporal logics for specifying weak memory consistency models

The formal verification of multithreaded programs is not just more difficult due to the concurrent behaviours, but also due to the used underlying weak memory consistency models. Weak memory models arise from techniques like store buffering that were ...
Verifying C11-style weak memory libraries
PPoPP '21: Proceedings of the 26th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming

Deductive verification of concurrent programs under weak memory has thus far been limited to simple programs over a monolithic state space. For scalabiility, we also require modular techniques with verifiable library abstractions. We address this ...
Virtual world consistency: A condition for STM systems (with a versatile protocol with invisible read operations)

The aim of a Software Transactional Memory (STM) is to discharge the programmers from the management of synchronization in multiprocess programs that access concurrent objects. To that end, an STM system provides the programmer with the concept of a ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 3, Issue POPL

January 2019

2275 pages

EISSN:2475-1421

DOI:10.1145/3302515

Issue’s Table of Contents

Copyright © 2019 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 02 January 2019

Published in PACMPL Volume 3, Issue POPL

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Funding Sources

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

22
Total Citations
View Citations
1,060
Total Downloads

Downloads (Last 12 months)160
Downloads (Last 6 weeks)15

Reflects downloads up to 21 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Nagar KSahoo AChowdhury RJagannathan S(2024)Automated Robustness Verification of Concurrent Data Structure Libraries against Relaxed Memory ModelsProceedings of the ACM on Programming Languages10.1145/36898028:OOPSLA2(2578-2605)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689802
Park SKim JMulder IJung JLee JKrebbers RKang J(2024)A Proof Recipe for Linearizability in Relaxed Memory Separation LogicProceedings of the ACM on Programming Languages10.1145/36563848:PLDI(175-198)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656384
Vafeiadi Bila EDongol B(2024)A verified durable transactional mutex lock for persistent x86-TSOFormal Methods in System Design10.1007/s10703-024-00462-1Online publication date: 31-Jul-2024
https://doi.org/10.1007/s10703-024-00462-1
Lee SCho MMargalit RHur CLahav O(2023)Putting Weak Memory in Order via a Promising Intermediate RepresentationProceedings of the ACM on Programming Languages10.1145/35912977:PLDI(1872-1895)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591297
Singh ALahav O(2023)An Operational Approach to Library Abstraction under Relaxed Memory ConcurrencyProceedings of the ACM on Programming Languages10.1145/35712467:POPL(1542-1572)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571246
D'Osualdo ERaad AVafeiadis V(2023)The Path to Durable LinearizabilityProceedings of the ACM on Programming Languages10.1145/35712197:POPL(748-774)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571219
Coughlin NWinter KSmith G(2022)Compositional Reasoning for Non-multicopy Atomic ArchitecturesFormal Aspects of Computing10.1145/357413735:2(1-30)Online publication date: 14-Dec-2022
https://dl.acm.org/doi/10.1145/3574137
Dalvandi SDongol B(2022)Implementing and verifying release-acquire transactional memory in C11Proceedings of the ACM on Programming Languages10.1145/35633526:OOPSLA2(1817-1844)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563352
Lesani MXia LKaseorg ABell CChlipala APierce BZdancewic S(2022)C4: verified transactional objectsProceedings of the ACM on Programming Languages10.1145/35273246:OOPSLA1(1-31)Online publication date: 29-Apr-2022
https://dl.acm.org/doi/10.1145/3527324
Dang HJung JChoi JNguyen DMansky WKang JDreyer DJhala RDillig I(2022)Compass: strong and compositional library specifications in relaxed memory separation logicProceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3519939.3523451(792-808)Online publication date: 9-Jun-2022
https://dl.acm.org/doi/10.1145/3519939.3523451
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents