Ori Lahav
Udi Boker
ABSTRACT
Causal consistency is one of the most fundamental and widely used consistency models weaker than sequential consistency. In this paper, we study the verification of safety properties for finite-state concurrent programs running under a causally consistent shared memory model. We establish the decidability of this problem for a standard model of causal consistency (called also "Causal Convergence" and "Strong-Release-Acquire"). Our proof proceeds by developing an alternative operational semantics, based on the notion of a thread potential, that is equivalent to the existing declarative semantics and constitutes a well-structured transition system. In particular, our result allows for the verification of a large family of programs in the Release/Acquire fragment of C/C++11 (RA). Indeed, while verification under RA was recently shown to be undecidable for general programs, since RA coincides with the model we study here for write/write-race-free programs, the decidability of verification under RA for this widely used class of programs follows from our result. The novel operational semantics may also be of independent use in the investigation of weakly consistent shared memory models and their verification.
- Ori Lahav and Udi Boker. 2020. Supplementary material for this paper. https://www.cs.tau.ac.il/~orilahav/papers/pldi20full.pdfGoogle Scholar
- Parosh Aziz Abdulla. 2010. Well (and better) quasi-ordered transition systems. The Bulletin of Symbolic Logic 16, 4 (2010), 457–515. http: //www.jstor.org/stable/40961367Google ScholarCross Ref
- Parosh Aziz Abdulla, Jatin Arora, Mohamed Faouzi Atig, and Shankaranarayanan Krishna. 2019. Verification of programs under the releaseacquire semantics. In PLDI. ACM, New York, NY, USA, 1117–1132.Google Scholar
- Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, and Tuan Phong Ngo. 2018. A load-buffer semantics for total store ordering. Logical Methods in Computer Science Volume 14, Issue 1 (Jan. 2018). Google ScholarCross Ref
- 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. Google ScholarDigital Library
- Parosh Aziz Abdulla, Mohamed Faouzi Atig, and Rojin Rezvan. 2019.Google Scholar
- Parameterized verification under TSO is PSPACE-complete. Proc. ACM Program. Lang. 4, POPL, Article 26 (Dec. 2019), 29 pages. Google ScholarDigital Library
- Parosh Aziz Abdulla, K¯ arlis Čer¯ ans, Bengt Jonsson, and Yih-Kuen Tsay. 2000. Algorithmic analysis of programs with well quasi-ordered domains. Information and Computation 160, 1 (2000), 109 – 127. Google ScholarDigital Library
- Sarita V. Adve and Mark D. Hill. 1990. Weak ordering—a new definition. In ISCA. ACM, New York, NY, USA, 2–14. 325164.325100 Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Masoud Saeida Ardekani, Pierre Sutra, and Marc Shapiro. 2013. Nonmonotonic snapshot isolation: Scalable and strong consistency for geo-replicated transactional systems. In SRDS. IEEE Computer Society, Washington, DC, USA, 163–172. Google ScholarDigital Library
- Mohamed Faouzi Atig, Ahmed Bouajjani, Sebastian Burckhardt, and Madanlal Musuvathi. 2010.Google Scholar
- On the verification problem for weak Decidable Verification under a Causally Consistent Shared Memory PLDI ’20, June 15–20, 2020, London, UK memory models. In POPL. ACM, New York, NY, USA, 7–18. Google ScholarDigital Library
- Mohamed Faouzi Atig, Ahmed Bouajjani, Sebastian Burckhardt, and Madanlal Musuvathi. 2012.Google Scholar
- What’s decidable about weak memory models?. In ESOP. Springer-Verlag, Berlin, Heidelberg, 26–46. Google ScholarDigital Library
- Mark Batty, Kayvan Memarian, Kyndylan Nienhuis, Jean Pichon-Pharabod, and Peter Sewell. 2015.Google Scholar
- The problem of programming language concurrency semantics. In ESOP. Springer, Berlin, Heidelberg, 283–307. Google ScholarCross Ref
- Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, and Tjark Weber. 2011. Mathematizing C++ concurrency. In POPL. ACM, New York, NY, USA, 55–66. Google ScholarDigital Library
- Giovanni Bernardi and Alexey Gotsman. 2016. Robustness against consistency models with atomic visibility. In CONCUR. Schloss Dagstuhl– Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 7:1–7:15. Google ScholarCross Ref
- Ahmed Bouajjani, Constantin Enea, Rachid Guerraoui, and Jad Hamza. 2017. On verifying causal consistency. In POPL. ACM, New York, NY, USA, 626–638. Google ScholarDigital Library
- Lucas Brutschy, Dimitar Dimitrov, Peter Müller, and Martin Vechev. 2018.Google Scholar
- Static serializability analysis for causal consistency. In PLDI. ACM, New York, NY, USA, 90–104. Google ScholarDigital Library
- 3192415Google Scholar
- Sebastian Burckhardt. 2014. Principles of eventual consistency. Found. Trends Program. Lang. 1, 1-2 (Oct. 2014), 1–150. 1561/2500000011 Google ScholarDigital Library
- Andrea Cerone, Alexey Gotsman, and Hongseok Yang. 2015. Transaction chopping for parallel snapshot isolation. In DISC. Springer-Verlag, Berlin, Heidelberg, 388–404. 5_26 Google ScholarDigital Library
- Andrea Cerone, Alexey Gotsman, and Hongseok Yang. 2017. Algebraic laws for weak consistency. In CONCUR, Vol. 85. Schloss Dagstuhl– Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 26:1–26:18. Google ScholarCross Ref
- Simon Doherty, Brijesh Dongol, Heike Wehrheim, and John Derrick. 2019.Google Scholar
- Verifying C11 programs operationally. In PPoPP. ACM, New York, NY, USA, 355–365. Google ScholarDigital Library
- Alain Finkel and Philippe Schnoebelen. 2001. Well-structured transition systems everywhere! Theoretical Computer Science 256, 1 (2001), 63 – 92. Google ScholarDigital Library
- ISO/IEC 14882:2011. 2011. Programming language C++.Google Scholar
- ISO/IEC 9899:2011. 2011. Programming language C.Google Scholar
- Jan-Oliver Kaiser, Hoang-Hai Dang, Derek Dreyer, Ori Lahav, and Viktor Vafeiadis. 2017.Google Scholar
- Strong logic for weak memory: Reasoning about release-acquire consistency in Iris. In ECOOP. Schloss Dagstuhl– Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 17:1–17:29. Google ScholarCross Ref
- Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, and Derek Dreyer. 2017.Google Scholar
- A Promising Semantics for Relaxed-Memory Concurrency. In POPL. ACM, New York, NY, USA, 175–189. Google ScholarDigital Library
- Michalis Kokologiannakis, Ori Lahav, Konstantinos Sagonas, and Viktor Vafeiadis. 2017. Effective stateless model checking for C/C++ concurrency. Proc. ACM Program. Lang. 2, POPL, Article 17 (Dec. 2017), 32 pages. Google ScholarDigital Library
- Michael Kuperstein, Martin Vechev, and Eran Yahav. 2011.Google Scholar
- Partialcoherence abstractions for relaxed memory models. In PLDI. ACM, New York, NY, USA, 187–198. Google ScholarDigital Library
- Ori Lahav. 2019. Verification under causally consistent shared memory. ACM SIGLOG News 6, 2 (April 2019), 43–56. 3326938.3326942 Google ScholarDigital Library
- Ori Lahav, Nick Giannarakis, and Viktor Vafeiadis. 2016.Google Scholar
- Taming release-acquire consistency. In POPL. ACM, New York, NY, USA, 649– 662. Google ScholarDigital Library
- Ori Lahav and Roy Margalit. 2019. Robustness against release/acquire semantics. In PLDI. ACM, New York, NY, USA, 126–141. org/10.1145/3314221.3314604 Google ScholarDigital Library
- Ori Lahav and Viktor Vafeiadis. 2015.Google Scholar
- Owicki-Gries reasoning for weak memory models. In ICALP. Springer-Verlag, Berlin, Heidelberg, 311–323. Google ScholarDigital Library
- Ori Lahav and Viktor Vafeiadis. 2016.Google Scholar
- Explaining relaxed memory models with program transformations. In FM. Springer, Cham, 479–495. Google ScholarCross Ref
- Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, and Derek Dreyer. 2017. Repairing sequential consistency in C/C++11. In PLDI. ACM, New York, NY, USA, 618–632. Google ScholarDigital Library
- 3062352Google Scholar
- Mohsen Lesani, Christian J. Bell, and Adam Chlipala. 2016. Chapar: Certified causally consistent distributed key-value stores. In POPL. ACM, New York, NY, USA, 357–370. Google ScholarDigital Library
- 2837622Google Scholar
- Cheng Li, Daniel Porto, Allen Clement, Johannes Gehrke, Nuno Preguiça, and Rodrigo Rodrigues. 2012.Google Scholar
- Making geo-replicated systems fast as possible, consistent when necessary. In OSDI. USENIX Association, Berkeley, CA, USA, 265–278. http://dl.acm.org/citation. cfm?id=2387880.2387906Google Scholar
- Wyatt Lloyd, Michael J. Freedman, Michael Kaminsky, and David G. Andersen. 2011. Don’t settle for eventual: Scalable causal consistency for wide-area storage with COPS. In SOSP. ACM, New York, NY, USA, 401–416. Google ScholarDigital Library
- Mapping 2019. C/C++11 mappings to processors. Retrieved July 3, 2019 from http://www.cl.cam.ac.uk/~pes20/cpp/cpp0xmappings.htmlGoogle Scholar
- Luc Maranget, Susmit Sarkar, and Peter Sewell. 2012.Google Scholar
- A tutorial introduction to the ARM and POWER relaxed memory models. http://www.cl.cam.ac.uk/~pes20/ppc-supplemental/test7.pdf.Google Scholar
- MongoDB Manual 4.2 2019. Causal consistency and read and write concerns. Retrieved November 19, 2019 from https://docs.mongodb. com/manual/core/causal-consistency-read-write-concernsGoogle Scholar
- Kartik Nagar and Suresh Jagannathan. 2018. Automated detection of serializability violations under weak consistency. In CONCUR, Vol. 118. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 41:1–41:18. Google ScholarCross Ref
- Scott Owens, Susmit Sarkar, and Peter Sewell. 2009.Google Scholar
- A better x86 memory model: x86-TSO. In TPHOLs. Springer, Heidelberg, 391–407. Google ScholarDigital Library
- Azalea Raad, Ori Lahav, and Viktor Vafeiadis. 2018.Google Scholar
- On parallel snapshot isolation and release/acquire consistency. In ESOP. Springer, Berlin, Heidelberg, 940–967. 1_33 Google ScholarCross Ref
- Sylvain Schmitz and Philippe Schnoebelen. 2012.Google Scholar
- Algorithmic aspects of WQO theory. (Aug. 2012). https://cel.archives-ouvertes.fr/cel- 00727025 Lecture notes.Google Scholar
- Yair Sovran, Russell Power, Marcos K. Aguilera, and Jinyang Li. 2011.Google Scholar
- Transactional storage for geo-replicated systems. In SOSP. ACM, New York, NY, USA, 385–400. Google ScholarDigital Library
- Thibault Suzanne and Antoine Miné. 2016.Google Scholar
- From array domains to abstract interpretation under store-buffer-based memory models. In SAS. Springer, Berlin, Heidelberg, 469–488.Google Scholar
- Douglas B. Terry, Alan J. Demers, Karin Petersen, Mike Spreitzer, Marvin Theimer, and Brent W. Welch. 1994. Session guarantees for weakly consistent replicated data. In PDIS. IEEE Computer Society, Washington, DC, USA, 140–149. http://dl.acm.org/citation.cfm?id= 645792.668302Google ScholarDigital Library
- Aaron Turon, Viktor Vafeiadis, and Derek Dreyer. 2014. GPS: Navigating weak memory with ghosts, protocols, and separation. In OOPSLA. ACM, New York, NY, USA, 691–707. Google ScholarDigital Library
- 2660243 PLDI ’20, June 15–20, 2020, London, UK Ori Lahav and Udi BokerGoogle Scholar
- Viktor Vafeiadis and Chinmay Narayan. 2013.Google Scholar
- Relaxed separation logic: A program logic for C11 concurrency. In OOPSLA. ACM, New York, NY, USA, 867–884. Google ScholarDigital Library
Index Terms
- Decidable verification under a causally consistent shared memory
Recommendations
What’s Decidable About Causally Consistent Shared Memory?
While causal consistency is one of the most fundamental consistency models weaker than sequential consistency, the decidability of safety verification for (finite-state) concurrent programs running under causally consistent shared memories is still ...
Chapar: certified causally consistent distributed key-value stores
POPL '16Today’s Internet services are often expected to stay available and render high responsiveness even in the face of site crashes and network partitions. Theoretical results state that causal consistency is one of the strongest consistency guarantees that ...
Verifying read-copy-update in a logic for weak memory
PLDI '15: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and ImplementationRead-Copy-Update (RCU) is a technique for letting multiple readers safely access a data structure while a writer concurrently modifies it. It is used heavily in the Linux kernel in situations where fast reads are important and writes are infrequent. ...
Comments