research-article

Static serializability analysis for causal consistency

Authors:

Lucas Brutschy,

Dimitar Dimitrov,

Martin VechevAuthors Info & Claims

PLDI 2018: Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation

Pages 90 - 104

https://doi.org/10.1145/3192366.3192415

Published: 11 June 2018 Publication History

Abstract

Many distributed databases provide only weak consistency guarantees to reduce synchronization overhead and remain available under network partitions. However, this leads to behaviors not possible under stronger guarantees. Such behaviors can easily defy programmer intuition and lead to errors that are notoriously hard to detect.

In this paper, we propose a static analysis for detecting non-serializable behaviors of applications running on top of causally-consistent databases. Our technique is based on a novel, local serializability criterion and combines a generalization of graph-based techniques from the database literature with another, complementary analysis technique that encodes our serializability criterion into first-order logic formulas to be checked by an SMT solver. This analysis is more expensive yet more precise and produces concrete counter-examples.

We implemented our methods and evaluated them on a number of applications from two different domains: cloud-backed mobile applications and clients of a distributed database. Our experiments demonstrate that our analysis is able to detect harmful serializability violations while producing only a small number of false alarms.

References

[1]

Atul Adya. 1999. Weak Consistency: A Generalized Theory and Optimistic Implementations for Distributed Transactions. PhD Thesis. Massachusetts Institute of Technology, Dept. of Electrical Engineering and Computer Science.

Digital Library

[2]

Deepthi Devaki Akkoorath and Annette Bieniusa. 2016. Antidote: The Highly-Available Geo-Replicated Database with Strongest Guarantees. Technical Report. Tech. U. Kaiserslautern. https://syncfree.lip6.fr/ attachments/article/59/antidote-white-paper.pdf

[3]

Jade Alglave, Daniel Kroening, Vincent Nimal, and Daniel Poetzl. 2014. Don’t Sit on the Fence. In Lecture Notes in Computer Science (Lecture Notes in Computer Science). Springer, 508–524.

[4]

Jade Alglave, Daniel Kroening, and Michael Tautschnig. 2013. Partial Orders for Efficient Bounded Model Checking of Concurrent Software. In CAV’13. Springer, 141–157.

[5]

Rajeev Alur, Ken McMillan, and Doron Peled. 2000. Model-Checking of Correctness Conditions for Concurrent Objects. Inf. Comput. 160, 1 (2000), 167–188.

Digital Library

[6]

Hagit Attiya, Faith Ellen, and Adam Morrison. 2017. Limitations of Highly-Available Eventually-Consistent Data Stores. IEEE Transactions on Parallel and Distributed Systems 28, 1 (2017), 141–155.

Digital Library

[7]

Peter Bailis, Alan Fekete, Joseph M. Hellerstein, Ali Ghodsi, and Ion Stoica. 2014. Scalable Atomic Visibility with RAMP Transactions. In SIGMOD ’14. ACM, 27–38.

Digital Library

[8]

Peter Bailis, Ali Ghodsi, Joseph M. Hellerstein, and Ion Stoica. 2013. Bolt-on Causal Consistency. In SIGMOD ’13. ACM, 761–772.

Digital Library

[9]

Giovanni Bernardi and Alexey Gotsman. 2016. Robustness against Consistency Models with Atomic Visibility. In CONCUR’16.

[10]

Ahmed Bouajjani, Constantin Enea, and Jad Hamza. 2014. Verifying Eventual Consistency of Optimistic Replication Systems. In POPL ’14. ACM, 285–296.

Digital Library

[11]

Lucas Brutschy, Dimitar Dimitrov, Peter Müller, and Martin Vechev. 2017. Serializability for Eventual Consistency: Criterion, Analysis, and Applications. In POPL ’17. ACM, 458–472.

Digital Library

[12]

Lucas Brutschy, Dimitar Dimitrov, Peter Müller, and Martin Vechev. 2018. Static Serializability Analysis for Causal Consistency (extended version). Technical Report. ETH Zurich.

[13]

Lucas Brutschy, Pietro Ferrara, and Peter Müller. 2014. Static Analysis for Independent App Developers. In OOPSLA ’14. ACM, 847–860.

Digital Library

[14]

Sebastian Burckhardt. 2014. Principles of Eventual Consistency. Found. Trends Program. Lang. 1, 1-2 (2014), 1–150.

Digital Library

[15]

Sebastian Burckhardt, Rajeev Alur, and Milo M. K. Martin. 2007. CheckFence: Checking Consistency of Concurrent Data Types on Relaxed Memory Models. In PLDI ’07. ACM, 12–21.

Digital Library

[16]

Sebastian Burckhardt, Manuel Fähndrich, Daan Leijen, and Benjamin P. Wood. 2012. Cloud Types for Eventual Consistency. In ECOOP’12. Springer, 283–307.

Digital Library

[17]

Sebastian Burckhardt, Alexey Gotsman, Hongseok Yang, and Marek Zawirski. 2014. Replicated Data Types: Specification, Verification, Optimality. In POPL ’14. ACM, 271–284.

Digital Library

[18]

Sebastian Burckhardt, Daan Leijen, Jonathan Protzenko, and Manuel Fähndrich. 2015. Global Sequence Protocol: A Robust Abstraction for Replicated Shared State. In Leibniz International Proceedings in Informatics (LIPIcs), John Tang Boyland (Ed.), Vol. 37. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 568–590.

[19]

Giuseppe DeCandia, Deniz Hastorun, Madan Jampani, Gunavardhan Kakulapati, Avinash Lakshman, Alex Pilchin, Swaminathan Sivasubramanian, Peter Vosshall, and Werner Vogels. 2007. Dynamo: Amazon’s Highly Available Key-Value Store. In SOSP ’07. ACM, 205–220.

Digital Library

[20]

Xing Fang, Jaejin Lee, and Samuel P. Midkiff. 2003. Automatic Fence Insertion for Shared Memory Multiprocessing. In ICS ’03. ACM, 285– 294.

Digital Library

[21]

Azadeh Farzan and P. Madhusudan. 2008. Monitoring Atomicity in Concurrent Programs. In CAV ’08. Springer, 52–65.

Digital Library

[22]

Alan Fekete, Dimitrios Liarokapis, Elizabeth O’Neil, Patrick O’Neil, and Dennis Shasha. 2005. Making Snapshot Isolation Serializable. ACM Trans. Database Syst. 30, 2 (2005), 492–528.

Digital Library

[23]

Seth Gilbert and Nancy Lynch. 2002. Brewer’s Conjecture and the Feasibility of Consistent, Available, Partition-Tolerant Web Services. SIGACT News 33, 2 (2002), 51–59.

Digital Library

[24]

Alexey Gotsman, Hongseok Yang, Carla Ferreira, Mahsa Najafzadeh, and Marc Shapiro. 2016. ’Cause I’m Strong Enough: Reasoning About Consistency Choices in Distributed Systems. In POPL ’16. ACM, 371– 384.

Digital Library

[25]

Sudhir Jorwekar, Alan Fekete, Krithi Ramamritham, and S. Sudarshan. 2007. Automating the Detection of Snapshot Isolation Anomalies. In VLDB ’07. VLDB Endowment, 1263–1274.

Digital Library

[26]

Arvind Krishnamurthy and Katherine Yelick. 1996. Analyses and Optimizations for Shared Address Space Programs. J. Parallel Distrib. Comput. 38, 2 (1996), 130–144.

Digital Library

[27]

Michael Kuperstein, Martin Vechev, and Eran Yahav. 2010. Automatic Inference of Memory Fences. In FMCAD ’10. FMCAD Inc, 111–120.

Digital Library

[28]

Avinash Lakshman and Prashant Malik. 2010. Cassandra: A Decentralized Structured Storage System. SIGOPS Oper. Syst. Rev. 44, 2 (2010), 35–40.

Digital Library

[29]

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 ’11. ACM, 401–416.

Digital Library

[30]

Wyatt Lloyd, Michael J. Freedman, Michael Kaminsky, and David G. Andersen. 2013. Stronger Semantics for Low-Latency Geo-Replicated Storage. In NSDI ’13. USENIX Association, 313–328.

Digital Library

[31]

Dennis Shasha and Marc Snir. 1988. Efficient and Correct Execution of Parallel Programs That Share Memory. ACM Trans. Program. Lang. Syst. 10, 2 (1988), 282–312.

Digital Library

[32]

Yair Sovran, Russell Power, Marcos K. Aguilera, and Jinyang Li. 2011. Transactional Storage for Geo-Replicated Systems. In SOSP ’11. ACM, 385–400.

Digital Library

[33]

Zehra Sura, Xing Fang, Chi-Leung Wong, Samuel P. Midkiff, Jaejin Lee, and David Padua. 2005. Compiler Techniques for High Performance Sequentially Consistent Java Programs. In PPoPP ’05. ACM, 2–13.

Digital Library

[34]

Nikolai Tillmann, Michal Moskal, Jonathan de Halleux, and Manuel Fahndrich. 2011. TouchDevelop: Programming Cloud-Connected Mobile Devices via Touchscreen. In Onward! 2011. ACM, 49–60.

Digital Library

[35]

Raja Vallée-Rai, Phong Co, Etienne Gagnon, Laurie Hendren, Patrick Lam, and Vijay Sundaresan. 1999. Soot - a Java Bytecode Optimization Framework. In CASCON ’99. IBM Press.

[36]

Mandana Vaziri, Frank Tip, and Julian Dolby. 2006. Associating Synchronization Constraints with Data in an Object-Oriented Language. In POPL ’06. ACM, 334–345.

Digital Library

[37]

William E. Weihl. 1988. Commutativity-Based Concurrency Control for Abstract Data Types. IEEE Trans. Comput. 37, 12 (1988), 1488–1505.

Digital Library

[38]

John Wickerson, Mark Batty, Tyler Sorensen, and George A. Constantinides. 2017. Automatically Comparing Memory Consistency Models. In POPL 2017. ACM, 190–204.

Digital Library

Cited By

Geng CBlanas SBond MWang Y(2024)IsoPredict: Dynamic Predictive Analysis for Detecting Unserializable Behaviors in Weakly Isolated Data Store ApplicationsProceedings of the ACM on Programming Languages10.1145/36563918:PLDI(343-367)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656391
Bouajjani AEnea CRomán-Calvo E(2023)Dynamic Partial Order Reduction for Checking Correctness against Transaction Isolation LevelsProceedings of the ACM on Programming Languages10.1145/35912437:PLDI(565-590)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591243
Zhang JJi YMu STan CFedorova ANarayanan DDi Luna GQuerzoni L(2023)Viper: A Fast Snapshot Isolation CheckerProceedings of the Eighteenth European Conference on Computer Systems10.1145/3552326.3567492(654-671)Online publication date: 8-May-2023
https://dl.acm.org/doi/10.1145/3552326.3567492
Show More Cited By

Index Terms

Static serializability analysis for causal consistency
1. Information systems
  1. Data management systems
    1. Database management system engines
      1. Parallel and distributed DBMSs
2. Software and its engineering
  1. Software creation and management
    1. Software verification and validation

Recommendations

Serializability for eventual consistency: criterion, analysis, and applications
POPL '17: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages

Developing and reasoning about systems using eventually consistent data stores is a difficult challenge due to the presence of unexpected behaviors that do not occur under sequential consistency. A fundamental problem in this setting is to identify a ...
Static serializability analysis for causal consistency
PLDI '18

Many distributed databases provide only weak consistency guarantees to reduce synchronization overhead and remain available under network partitions. However, this leads to behaviors not possible under stronger guarantees. Such behaviors can easily defy ...
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 ACM Conferences

PLDI 2018: Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation

June 2018

825 pages

ISBN:9781450356985

DOI:10.1145/3192366

General Chair:
Jeffrey S. Foster
University of Maryland at College Park, USA
,
Program Chair:
Dan Grossman
University of Washington, USA

ACM SIGPLAN Notices Volume 53, Issue 4
PLDI '18
April 2018
834 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/3296979
Editor:
Matthew Fluet
Rodchester Institude of Technology
Issue’s Table of Contents

Copyright © 2018 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 the author(s) 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 2018

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Conference

PLDI '18

Sponsor:

SIGPLAN

PLDI '18: ACM SIGPLAN Conference on Programming Language Design and Implementation

June 18 - 22, 2018

PA, Philadelphia, USA

Acceptance Rates

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

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

18
Total Citations
View Citations
349
Total Downloads

Downloads (Last 12 months)27
Downloads (Last 6 weeks)5

Reflects downloads up to 14 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Geng CBlanas SBond MWang Y(2024)IsoPredict: Dynamic Predictive Analysis for Detecting Unserializable Behaviors in Weakly Isolated Data Store ApplicationsProceedings of the ACM on Programming Languages10.1145/36563918:PLDI(343-367)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656391
Bouajjani AEnea CRomán-Calvo E(2023)Dynamic Partial Order Reduction for Checking Correctness against Transaction Isolation LevelsProceedings of the ACM on Programming Languages10.1145/35912437:PLDI(565-590)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591243
Zhang JJi YMu STan CFedorova ANarayanan DDi Luna GQuerzoni L(2023)Viper: A Fast Snapshot Isolation CheckerProceedings of the Eighteenth European Conference on Computer Systems10.1145/3552326.3567492(654-671)Online publication date: 8-May-2023
https://dl.acm.org/doi/10.1145/3552326.3567492
Dou WCui ZDai QSong JWang DGao YWang WWei JChen LWang HZhong HHuang TGrundy JPollock LPenta M(2023)Detecting Isolation Bugs via Transaction Oracle ConstructionProceedings of the 45th International Conference on Software Engineering10.1109/ICSE48619.2023.00101(1123-1135)Online publication date: 14-May-2023
https://dl.acm.org/doi/10.1109/ICSE48619.2023.00101
Beillahi SBouajjani AEnea C(2023)Comparing Causal Convergence Consistency ModelsNetworked Systems10.1007/978-3-031-37765-5_5(62-77)Online publication date: 22-May-2023
https://dl.acm.org/doi/10.1007/978-3-031-37765-5_5
Lahav OBoker U(2022)What’s Decidable About Causally Consistent Shared Memory?ACM Transactions on Programming Languages and Systems10.1145/350527344:2(1-55)Online publication date: 6-Apr-2022
https://dl.acm.org/doi/10.1145/3505273
Rahmani KNagar KDelaware BJagannathan SFreund SYahav E(2021)Repairing serializability bugs in distributed database programs via automated schema refactoringProceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3453483.3454028(32-47)Online publication date: 19-Jun-2021
https://dl.acm.org/doi/10.1145/3453483.3454028
Margalit RLahav O(2021)Verifying observational robustness against a c11-style memory modelProceedings of the ACM on Programming Languages10.1145/34342855:POPL(1-33)Online publication date: 4-Jan-2021
https://dl.acm.org/doi/10.1145/3434285
Beillahi SBouajjani AEnea C(2021)Checking Robustness Between Weak Transactional Consistency ModelsProgramming Languages and Systems10.1007/978-3-030-72019-3_4(87-117)Online publication date: 27-Mar-2021
https://dl.acm.org/doi/10.1007/978-3-030-72019-3_4
Tan CZhao CMu SWalfish MLu SHowell J(2020)COBRAProceedings of the 14th USENIX Conference on Operating Systems Design and Implementation10.5555/3488766.3488770(63-80)Online publication date: 4-Nov-2020
https://dl.acm.org/doi/10.5555/3488766.3488770
Show More Cited By

View Options

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

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents