[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ skip to main content
10.1007/978-3-030-67087-0_17guideproceedingsArticle/Chapter ViewAbstractPublication PagesConference Proceedingsacm-pubtype
Article

Verifying Weakly Consistent Transactional Programs Using Symbolic Execution

Published: 03 June 2020 Publication History

Abstract

We present a method for verifying whether all executions of a set of transactions satisfy a given invariant when run on weakly consistent systems. Existing approaches check that all executions under weak consistency are equivalent to some serial execution of the transactions, and separately that the serial executions satisfy the invariant. While sound, this can be overly strict. Programs running on systems with weak guarantees are usually designed to tolerate some anomalies w.r.t. the serial semantics and yet maintain some expected program invariants even on executions that are not serializable. In contrast, our technique does not restrict possible executions to be serializable, but directly checks whether given program properties hold w.r.t. all executions allowed under varying consistency models.
Our approach uses symbolic execution techniques and satisfiability checkers. We summarize the effects of transactions using symbolic execution and build a satisfiability formula that precisely captures all possible valuations of the data variables under a given consistency model. Then, we check whether the program invariants hold on the resulting symbolic set of behaviors. Our encoding is parameterized over the underlying consistency specification. Hence, the programmer can check the correctness of a program under several consistency models—eventual consistency, causal consistency, (parallel) snapshot isolation, serializability— and identify the level of consistency needed to satisfy the application-level invariants.

References

[1]
Ahamad M, Neiger G, Burns JE, Kohli P, and Hutto PW Causal memory: definitions, implementation, and programming Distributed Comput. 1995 9 1 37-49
[2]
Balegas, V., et al.: Putting consistency back into eventual consistency. In: The 10th European Conference on Computer Systems, EuroSys, pp. 6:1–6:16. ACM (2015)
[3]
Barnett M, Chang B-YE, DeLine R, Jacobs B, and Leino KRM de Boer FS, Bonsangue MM, Graf S, and de Roever W-P Boogie: a modular reusable verifier for object-oriented programs Formal Methods for Components and Objects 2006 Heidelberg Springer 364-387
[4]
Beillahi SM, Bouajjani A, and Enea C Dillig I and Tasiran S Checking robustness against snapshot isolation Computer Aided Verification 2019 Cham Springer 286-304
[5]
Beillahi, S.M., Bouajjani, A., Enea, C.: Robustness against transactional causal consistency. In: 30th International Conference on Concurrency Theory, CONCUR. LIPIcs, vol. 140, pp. 30:1–30:18 (2019)
[6]
Berenson, H., Bernstein, P.A., Gray, J., Melton, J., O’Neil, E.J., O’Neil, P.E.: A critique of ANSI SQL isolation levels. In: ACM SIGMOD International Conference on Management of Data, pp. 1–10. ACM Press (1995)
[7]
Bernardi, G., Gotsman, A.: Robustness against consistency models with atomic visibility. In: 27th International Conference on Concurrency Theory, CONCUR. LIPIcs, vol. 59, pp. 7:1–7:15 (2016)
[8]
Bernstein, P.A., Hadzilacos, V., Goodman, N.: Concurrency Control and Recovery in Database Systems. Addison-Wesley (1987)
[9]
Brewer, E.A.: Towards robust distributed systems (abstract). In: The 9th Annual ACM Symposium on Principles of Distributed Computing, p. 7. ACM (2000)
[10]
Brutschy, L., Dimitrov, D., Müller, P., Vechev, M.T.: Serializability for eventual consistency: criterion, analysis, and applications. In: The 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL, pp. 458–472. ACM (2017)
[11]
Brutschy, L., Dimitrov, D., Müller, P., Vechev, M.T.: Static serializability analysis for causal consistency. In: The 39th ACM SIGPLAN Conf. on Programming Language Design and Implementation, PLD, pp. 90–104. ACM (2018)
[12]
Burckhardt S Principles of eventual consistency Found. Trends Program. Lang. 2014 1 1–2 1-150
[13]
Burckhardt, S., Gotsman, A., Yang, H., Zawirski, M.: Replicated data types: specification, verification, optimality. In: The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL, pp. 271–284. ACM (2014)
[14]
Burckhardt, S., Leijen, D., Protzenko, J., Fähndrich, M.: Global sequence protocol: a robust abstraction for replicated shared state. In: 29th European Conference on Object-Oriented Programming, ECOOP, LIPIcs, vol. 37, pp. 568–590 (2015)
[15]
Cahill, M.J., Röhm, U., Fekete, A.D.: Serializable isolation for snapshot databases. ACM Trans. Database Syst. 34(4), 20:1–20:42 (2009)
[16]
Cerone, A., Bernardi, G., Gotsman, A.: A framework for transactional consistency models with atomic visibility. In: 26th International Conference on Concurrency Theory, CONCUR. LIPIcs, vol. 42, pp. 58–71 (2015)
[17]
Cerone, A., Gotsman, A.: Analysing snapshot isolation. J. ACM 65(2), 11:1–11:41 (2018)
[18]
Dabaghchian M, Rakamaric Z, Kulahcioglu Ozkan B, Mutlu E, and Tasiran S Consistency-aware scheduling for weakly consistent programs ACM SIGSOFT Softw. Eng. Notes 2017 42 4 1-5
[19]
Fekete A, Liarokapis D, O’Neil EJ, O’Neil PE, and Shasha DE Making snapshot isolation serializable ACM Trans. Database Syst. 2005 30 2 492-528
[20]
Gotsman, A., Yang, H., Ferreira, C., Najafzadeh, M., Shapiro, M.: ’cause i’m strong enough: reasoning about consistency choices in distributed systems. In: The 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL, pp. 371–384. ACM (2016)
[21]
Holt, B., Bornholt, J., Zhang, I., Ports, D.R.K., Oskin, M., Ceze, L.: Disciplined inconsistency with consistency types. In: The 7th ACM Symposium on Cloud Computing, pp. 279–293. ACM (2016)
[22]
Kaki, G., Nagar, K., Najafzadeh, M., Jagannathan, S.: Alone together: compositional reasoning and inference for weak isolation. In: Proceedings ACM Programming Language, vol. 2(POPL), pp. 27:1–27:34 (2018)
[23]
Kuru, I., Kulahcioglu Ozkan, B., Mutluergil, S.O., Tasiran, S., Elmas, T., Cohen, E.: Verifying programs under snapshot isolation and similar relaxed consistency models. In: The 9th ACM SIGPLAN Workshop on Transactional Computing (2014)
[24]
Lakshman A and Malik P Cassandra: a decentralized structured storage system Operating Syst. Rev. 2010 44 2 35-40
[25]
Lamport L Time, clocks, and the ordering of events in a distributed system Commun. ACM 1978 21 7 558-565
[26]
Liew, D., Cadar, C., Donaldson, A.F.: Symbooglix: a symbolic execution engine for boogie programs. In: 2016 IEEE International Conference on Software Testing, Verification and Validation, ICST, pp. 45–56. IEEE Computer Society (2016)
[27]
Lloyd, W., Freedman, M.J., Kaminsky, M., Andersen, D.G.: Don’t settle for eventual: scalable causal consistency for wide-area storage with COPS. In: The 23rd ACM Symposium on Operating Systems Principles 2011, SOSP, pp. 401–416. ACM (2011)
[28]
Nagar, K., Jagannathan, S.: Automated detection of serializability violations under weak consistency. In: 29th International Conference on Concurrency Theory, CONCUR. LIPIcs, vol. 118, pp. 41:1–41:18 (2018)
[29]
Nair SS, Petri G, and Shapiro M Proving the safety of highly-available distributed objects Programming Languages and Systems 2020 Cham Springer 544-571
[30]
Najafzadeh, M., Gotsman, A., Yang, H., Ferreira, C., Shapiro, M.: The CISE tool: proving weakly-consistent applications correct. In: The 2nd Workshop on the Principles and Practice of Consistency for Distributed Data, pp. 2:1–2:3. ACM (2016)
[31]
Shapiro M, Preguiça N, Baquero C, and Zawirski M Défago X, Petit F, and Villain V Conflict-free replicated data types Stabilization, Safety, and Security of Distributed Systems 2011 Heidelberg Springer 386-400
[32]
Sovran, Y., Power, R., Aguilera, M.K., Li, J.: Transactional storage for geo-replicated systems. In: The 23rd ACM Symposium on Operating System Principles 2011, SOSP, pp. 385–400. ACM (2011)
[33]
Zellag, K., Kemme, B.: How consistent is your cloud application? In: ACM Symposium on Cloud Computing, SOCC, p. 6 (2012)
[34]
Zeller, P.: Testing properties of weakly consistent programs with repliss. In: The 3rd International Workshop on Principles and Practice of Consistency for Distributed Data. pp. 3:1–3:5 (2017)

Cited By

View all
  • (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
  • (2021)MonkeyDB: effectively testing correctness under weak isolation levelsProceedings of the ACM on Programming Languages10.1145/34855465:OOPSLA(1-27)Online publication date: 15-Oct-2021

Recommendations

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings
Networked Systems: 8th International Conference, NETYS 2020, Marrakech, Morocco, June 3–5, 2020, Proceedings
Jun 2020
387 pages
ISBN:978-3-030-67086-3
DOI:10.1007/978-3-030-67087-0

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 03 June 2020

Author Tags

  1. Weak consistency
  2. Transactions
  3. Symbolic execution
  4. Satisfiability

Qualifiers

  • Article

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)0
  • Downloads (Last 6 weeks)0
Reflects downloads up to 01 Jan 2025

Other Metrics

Citations

Cited By

View all
  • (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
  • (2021)MonkeyDB: effectively testing correctness under weak isolation levelsProceedings of the ACM on Programming Languages10.1145/34855465:OOPSLA(1-27)Online publication date: 15-Oct-2021

View Options

View options

Media

Figures

Other

Tables

Share

Share

Share this Publication link

Share on social media