research-article

Open access

Decidable verification under a causally consistent shared memory

Authors:

Udi BokerAuthors Info & Claims

PLDI 2020: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation

Pages 211 - 226

https://doi.org/10.1145/3385412.3385966

Published: 11 June 2020 Publication History

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.

References

[1]

Ori Lahav and Udi Boker. 2020. Supplementary material for this paper. https://www.cs.tau.ac.il/~orilahav/papers/pldi20full.pdf

[2]

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/40961367

[3]

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.

[4]

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

[5]

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

[6]

Parosh Aziz Abdulla, Mohamed Faouzi Atig, and Rojin Rezvan. 2019.

[7]

Parameterized verification under TSO is PSPACE-complete. Proc. ACM Program. Lang. 4, POPL, Article 26 (Dec. 2019), 29 pages.

Digital Library

[8]

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.

Digital Library

[9]

Sarita V. Adve and Mark D. Hill. 1990. Weak ordering—a new definition. In ISCA. ACM, New York, NY, USA, 2–14. 325164.325100

Digital Library

[10]

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

[11]

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.

Digital Library

[12]

Mohamed Faouzi Atig, Ahmed Bouajjani, Sebastian Burckhardt, and Madanlal Musuvathi. 2010.

[13]

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.

Digital Library

[14]

Mohamed Faouzi Atig, Ahmed Bouajjani, Sebastian Burckhardt, and Madanlal Musuvathi. 2012.

[15]

What’s decidable about weak memory models?. In ESOP. Springer-Verlag, Berlin, Heidelberg, 26–46.

Digital Library

[16]

Mark Batty, Kayvan Memarian, Kyndylan Nienhuis, Jean Pichon-Pharabod, and Peter Sewell. 2015.

[17]

The problem of programming language concurrency semantics. In ESOP. Springer, Berlin, Heidelberg, 283–307.

[18]

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

Digital Library

[19]

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.

[20]

Ahmed Bouajjani, Constantin Enea, Rachid Guerraoui, and Jad Hamza. 2017. On verifying causal consistency. In POPL. ACM, New York, NY, USA, 626–638.

Digital Library

[21]

Lucas Brutschy, Dimitar Dimitrov, Peter Müller, and Martin Vechev. 2018.

[22]

Static serializability analysis for causal consistency. In PLDI. ACM, New York, NY, USA, 90–104.

Digital Library

[23]

3192415

[24]

Sebastian Burckhardt. 2014. Principles of eventual consistency. Found. Trends Program. Lang. 1, 1-2 (Oct. 2014), 1–150. 1561/2500000011

Digital Library

[25]

Andrea Cerone, Alexey Gotsman, and Hongseok Yang. 2015. Transaction chopping for parallel snapshot isolation. In DISC. Springer-Verlag, Berlin, Heidelberg, 388–404. 5_26

Digital Library

[26]

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.

[27]

Simon Doherty, Brijesh Dongol, Heike Wehrheim, and John Derrick. 2019.

[28]

Verifying C11 programs operationally. In PPoPP. ACM, New York, NY, USA, 355–365.

Digital Library

[29]

Alain Finkel and Philippe Schnoebelen. 2001. Well-structured transition systems everywhere! Theoretical Computer Science 256, 1 (2001), 63 – 92.

Digital Library

[30]

ISO/IEC 14882:2011. 2011. Programming language C++.

[31]

ISO/IEC 9899:2011. 2011. Programming language C.

[32]

Jan-Oliver Kaiser, Hoang-Hai Dang, Derek Dreyer, Ori Lahav, and Viktor Vafeiadis. 2017.

[33]

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.

[34]

Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, and Derek Dreyer. 2017.

[35]

A Promising Semantics for Relaxed-Memory Concurrency. In POPL. ACM, New York, NY, USA, 175–189.

Digital Library

[36]

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.

Digital Library

[37]

Michael Kuperstein, Martin Vechev, and Eran Yahav. 2011.

[38]

Partialcoherence abstractions for relaxed memory models. In PLDI. ACM, New York, NY, USA, 187–198.

Digital Library

[39]

Ori Lahav. 2019. Verification under causally consistent shared memory. ACM SIGLOG News 6, 2 (April 2019), 43–56. 3326938.3326942

Digital Library

[40]

Ori Lahav, Nick Giannarakis, and Viktor Vafeiadis. 2016.

[41]

Taming release-acquire consistency. In POPL. ACM, New York, NY, USA, 649– 662.

Digital Library

[42]

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

Digital Library

[43]

Ori Lahav and Viktor Vafeiadis. 2015.

[44]

Owicki-Gries reasoning for weak memory models. In ICALP. Springer-Verlag, Berlin, Heidelberg, 311–323.

Digital Library

[45]

Ori Lahav and Viktor Vafeiadis. 2016.

[46]

Explaining relaxed memory models with program transformations. In FM. Springer, Cham, 479–495.

[47]

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.

Digital Library

[48]

3062352

[49]

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.

Digital Library

[50]

2837622

[51]

Cheng Li, Daniel Porto, Allen Clement, Johannes Gehrke, Nuno Preguiça, and Rodrigo Rodrigues. 2012.

[52]

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

[53]

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.

Digital Library

[54]

Mapping 2019. C/C++11 mappings to processors. Retrieved July 3, 2019 from http://www.cl.cam.ac.uk/~pes20/cpp/cpp0xmappings.html

[55]

Luc Maranget, Susmit Sarkar, and Peter Sewell. 2012.

[56]

A tutorial introduction to the ARM and POWER relaxed memory models. http://www.cl.cam.ac.uk/~pes20/ppc-supplemental/test7.pdf.

[57]

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-concerns

[58]

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.

[59]

Scott Owens, Susmit Sarkar, and Peter Sewell. 2009.

[60]

A better x86 memory model: x86-TSO. In TPHOLs. Springer, Heidelberg, 391–407.

Digital Library

[61]

Azalea Raad, Ori Lahav, and Viktor Vafeiadis. 2018.

[62]

On parallel snapshot isolation and release/acquire consistency. In ESOP. Springer, Berlin, Heidelberg, 940–967. 1_33

[63]

Sylvain Schmitz and Philippe Schnoebelen. 2012.

[64]

Algorithmic aspects of WQO theory. (Aug. 2012). https://cel.archives-ouvertes.fr/cel- 00727025 Lecture notes.

[65]

Yair Sovran, Russell Power, Marcos K. Aguilera, and Jinyang Li. 2011.

[66]

Transactional storage for geo-replicated systems. In SOSP. ACM, New York, NY, USA, 385–400.

Digital Library

[67]

Thibault Suzanne and Antoine Miné. 2016.

[68]

From array domains to abstract interpretation under store-buffer-based memory models. In SAS. Springer, Berlin, Heidelberg, 469–488.

[69]

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

Digital Library

[70]

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.

Digital Library

[71]

2660243 PLDI ’20, June 15–20, 2020, London, UK Ori Lahav and Udi Boker

[72]

Viktor Vafeiadis and Chinmay Narayan. 2013.

[73]

Relaxed separation logic: A program logic for C11 concurrency. In OOPSLA. ACM, New York, NY, USA, 867–884.

Digital Library

Cited By

Ambal GDongol BEran HKlimis VLahav ORaad A(2024)Semantics of Remote Direct Memory Access: Operational and Declarative Models of RDMA on TSO ArchitecturesProceedings of the ACM on Programming Languages10.1145/36897818:OOPSLA2(1982-2009)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689781
Abdulla PAtig MBouajjani AKumar KSaivasan P(2024)Verification under Intel-x86 with PersistencyProceedings of the ACM on Programming Languages10.1145/36564258:PLDI(1189-1212)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656425
Bargmann LWehrheim H(2024)View-Based Axiomatic Reasoning for the Weak Memory Models PSO and SRAScience of Computer Programming10.1016/j.scico.2024.103225(103225)Online publication date: Oct-2024
https://doi.org/10.1016/j.scico.2024.103225
Show More Cited By

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 '16

Today’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 Implementation

Read-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

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

PLDI 2020: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation

June 2020

1174 pages

ISBN:9781450376136

DOI:10.1145/3385412

General Chair:
Alastair F. Donaldson
Imperial College London, UK
,
Program Chair:
Emina Torlak
University of Washington, USA

Copyright © 2020 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 11 June 2020

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Funding Sources

Israel Science Foundation

Conference

PLDI '20

Sponsor:

SIGPLAN

PLDI '20: 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation

June 15 - 20, 2020

London, UK

Acceptance Rates

Overall Acceptance Rate 406 of 2,067 submissions, 20%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

22
Total Citations
View Citations
479
Total Downloads

Downloads (Last 12 months)81
Downloads (Last 6 weeks)9

Reflects downloads up to 24 Oct 2024

Other Metrics

View Author Metrics

Citations

Cited By

Ambal GDongol BEran HKlimis VLahav ORaad A(2024)Semantics of Remote Direct Memory Access: Operational and Declarative Models of RDMA on TSO ArchitecturesProceedings of the ACM on Programming Languages10.1145/36897818:OOPSLA2(1982-2009)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689781
Abdulla PAtig MBouajjani AKumar KSaivasan P(2024)Verification under Intel-x86 with PersistencyProceedings of the ACM on Programming Languages10.1145/36564258:PLDI(1189-1212)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656425
Bargmann LWehrheim H(2024)View-Based Axiomatic Reasoning for the Weak Memory Models PSO and SRAScience of Computer Programming10.1016/j.scico.2024.103225(103225)Online publication date: Oct-2024
https://doi.org/10.1016/j.scico.2024.103225
Bargmann LDongol BWehrheim H(2024)Unifying Weak Memory Verification Using PotentialsFormal Methods10.1007/978-3-031-71162-6_27(519-537)Online publication date: 9-Sep-2024
https://dl.acm.org/doi/10.1007/978-3-031-71162-6_27
Dongol BLahav OWehrheim H(2024)A Rely-Guarantee Framework for Proving Deadlock Freedom Under Causal ConsistencyThe Practice of Formal Methods10.1007/978-3-031-66676-6_5(88-108)Online publication date: 4-Sep-2024
https://doi.org/10.1007/978-3-031-66676-6_5
Singh ALahav O(2024)Decidable Verification under Localized Release-Acquire ConcurrencyTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-031-57256-2_12(235-254)Online publication date: 6-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-57256-2_12
Bouajjani A(2024)On Verifying Concurrent Programs Under Weak Consistency Models: Decidability and ComplexityTaming the Infinities of Concurrency10.1007/978-3-031-56222-8_7(133-147)Online publication date: 20-Mar-2024
https://doi.org/10.1007/978-3-031-56222-8_7
Haas TMaseli RMeyer RPonce de León H(2023)Static Analysis of Memory Models for SMT EncodingsProceedings of the ACM on Programming Languages10.1145/36228557:OOPSLA2(1618-1647)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622855
Beillahi SBouajjani AEnea C(2023)Comparing Causal Convergence Consistency ModelsNetworked Systems10.1007/978-3-031-37765-5_5(62-77)Online publication date: 7-Jul-2023
https://doi.org/10.1007/978-3-031-37765-5_5
Lahav ODongol BWehrheim H(2023)Rely-Guarantee Reasoning for Causally Consistent Shared MemoryComputer Aided Verification10.1007/978-3-031-37706-8_11(206-229)Online publication date: 17-Jul-2023
https://dl.acm.org/doi/10.1007/978-3-031-37706-8_11
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Get Access

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 Publication

Media

Figures

Other

Tables

View Table of Contents