Document Open Access Logo

Data Consistency in Transactional Storage Systems: A Centralised Semantics

Authors Shale Xiong, Andrea Cerone, Azalea Raad, Philippa Gardner

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2020.21.pdf
  • Filesize: 0.75 MB
  • 31 pages

Document Identifiers

Author Details

Shale Xiong
  • Department of Computing, Imperial College London, United Kingdom
Andrea Cerone
  • Department of Computing, Imperial College London, United Kingdom
Azalea Raad
  • MPI-SWS, Kaiserslautern, Germany
Philippa Gardner
  • Department of Computing, Imperial College London, United Kingdom

Funding

  • Xiong, Shale: The Department of Computing, Imperial College London, and EPSRC Fellowship VeTSpec: Verified Trustworthy Software Specification (EP/R034567/1)
  • Cerone, Andrea: EPSRC Programme Grant REMS: Rigorous Engineering for Mainstream Systems (EP/K008528/1), and EPSRC Fellowship VeTSpec: Verified Trustworthy Software Specification (EP/R034567/1)
  • Raad, Azalea: ERC Horizon 2020 Consolidator Grant "RustBelt" (grant agreement no. 683289)
  • Gardner, Philippa: EPSRC Programme Grant REMS: Rigorous Engineering for Mainstream Systems (EP/K008528/1), and EPSRC Fellowship VeTSpec: Verified Trustworthy Software Specification (EP/R034567/1)

Cite AsGet BibTex

Shale Xiong, Andrea Cerone, Azalea Raad, and Philippa Gardner. Data Consistency in Transactional Storage Systems: A Centralised Semantics. In 34th European Conference on Object-Oriented Programming (ECOOP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 166, pp. 21:1-21:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.ECOOP.2020.21

Abstract

We introduce an interleaving operational semantics for describing the client-observable behaviour of atomic transactions on distributed key-value stores. Our semantics builds on abstract states comprising centralised, global key-value stores and partial client views. Using our abstract states, we present operational definitions of well-known consistency models in the literature, and prove them to be equivalent to their existing declarative definitions using abstract executions. We explore two applications of our operational framework: 1) verifying that the COPS replicated database and the Clock-SI partitioned database satisfy their consistency models using trace refinement, and 2) proving invariant properties of client programs.

Subject Classification

ACM Subject Classification
  • Theory of computation → Operational semantics
Keywords
  • Operational Semantics
  • Consistency Models
  • Transactions
  • Distributed Key-value Stores

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Atul Adya. Weak Consistency: A Generalized Theory and Optimistic Implementations for Distributed Transactions. PhD thesis, Massachusetts Institute of Technology, Cambridge, MA, USA, 1999. URL: http://pmg.csail.mit.edu/papers/adya-phd.pdf.
  2. M. Alomari, M. Cahill, A. Fekete, and U. Rohm. The cost of serializability on platforms that use snapshot isolation. In 2008 IEEE 24th International Conference on Data Engineering, pages 576-585, April 2008. URL: https://doi.org/10.1109/ICDE.2008.4497466.
  3. Masoud Saeida Ardekani, Pierre Sutra, and Marc Shapiro. Non-monotonic snapshot isolation: Scalable and strong consistency for geo-replicated transactional systems. In Proceedings of the 2013 IEEE 32nd International Symposium on Reliable Distributed Systems, SRDS ’13, page 163–172, USA, 2013. IEEE Computer Society. URL: https://doi.org/10.1109/SRDS.2013.25.
  4. Peter Bailis, Alan Fekete, Ali Ghodsi, Joseph M. Hellerstein, and Ion Stoica. Scalable atomic visibility with ramp transactions. ACM Trans. Database Syst., 41(3), July 2016. URL: https://doi.org/10.1145/2909870.
  5. Sidi Mohamed Beillahi, Ahmed Bouajjani, and Constantin Enea. Checking robustness against snapshot isolation. CoRR, abs/1905.08406, 2019. URL: http://arxiv.org/abs/1905.08406.
  6. Hal Berenson, Phil Bernstein, Jim Gray, Jim Melton, Elizabeth O'Neil, and Patrick O'Neil. A Critique of ANSI SQL Isolation Levels. In Proceedings of the 1995 ACM SIGMOD International Conference on Management of Data, SIGMOD'95, pages 1-10. ACM, 1995. URL: https://doi.org/10.1145/223784.223785.
  7. Giovanni Bernardi and Alexey Gotsman. Robustness against Consistency Models with Atomic Visibility. In Proceedings of the 27superscriptth International Conference on Concurrency Theory, pages 7:1-7:15, 2016. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2016.7.
  8. Carsten Binnig, Stefan Hildenbrand, Franz Färber, Donald Kossmann, Juchang Lee, and Norman May. Distributed Snapshot Isolation: Global Transactions Pay Globally, Local Transactions Pay Locally. The VLDB Journal, 23(6):987-1011, December 2014. URL: https://doi.org/10.1007/s00778-014-0359-9.
  9. Sebastian Burckhardt, Manuel Fahndrich, Daan Leijen, and Mooly Sagiv. Eventually Consistent Transactions. In Proceedings of the 21superscriptnd European Symposium on Programming. Springer, March 2012. URL: https://doi.org/10.1007/978-3-642-28869-2_4.
  10. Sebastian Burckhardt, Daan Leijen, Jonathan Protzenko, and Manuel Fähndrich. Global sequence protocol: A robust abstraction for replicated shared state. In 29th European Conference on Object-Oriented Programming, ECOOP 2015, July 5-10, 2015, Prague, Czech Republic, pages 568-590, 2015. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2015.568.
  11. Andrea Cerone, Giovanni Bernardi, and Alexey Gotsman. A Framework for Transactional Consistency Models with Atomic Visibility. In Luca Aceto and David de Frutos Escrig, editors, 26th International Conference on Concurrency Theory (CONCUR 2015), volume 42 of Leibniz International Proceedings in Informatics (LIPIcs), pages 58-71, Dagstuhl, Germany, 2015. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2015.58.
  12. Andrea Cerone and Alexey Gotsman. Analysing Snapshot Isolation. In Proceedings of the 2016 ACM SIGACT-SIGOPS Symposium on Principles of Distributed Computing, PODC'16, pages 55-64. ACM, 2016. URL: https://doi.org/10.1145/2933057.2933096.
  13. Andrea Cerone, Alexey Gotsman, and Hongseok Yang. Transaction chopping for parallel snapshot isolation. In Proceedings of the 29th International Symposium on Distributed Computing - Volume 9363, DISC 2015, page 388–404, Berlin, Heidelberg, 2015. Springer-Verlag. URL: https://doi.org/10.1007/978-3-662-48653-5_26.
  14. Andrea Cerone, Alexey Gotsman, and Hongseok Yang. Algebraic Laws for Weak Consistency. In Roland Meyer and Uwe Nestmann, editors, Proceedings of the 27superscriptth International Conference on Concurrency Theory, volume 85 of Leibniz International Proceedings in Informatics (LIPIcs), pages 26:1-26:18, Dagstuhl, Germany, 2017. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2017.26.
  15. Nathan Chong, Tyler Sorensen, and John Wickerson. The semantics of transactions and weak memory in x86, power, arm, and C++. In Jeffrey S. Foster and Dan Grossman, editors, Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, Philadelphia, PA, USA, June 18-22, 2018, pages 211-225. ACM, 2018. URL: https://doi.org/10.1145/3192366.3192373.
  16. Natacha Crooks, Youer Pu, Lorenzo Alvisi, and Allen Clement. Seeing is Believing: A Client-Centric Specification of Database Isolation. In Proceedings of the 2017 ACM SIGACT-SIGOPS Symposium on Principles of Distributed Computing, PODC'17, pages 73-82, New York, NY, USA, 2017. ACM. URL: https://doi.org/10.1145/3087801.3087802.
  17. Pedro da Rocha Pinto, Thomas Dinsdale-Young, and Philippa Gardner. TaDA: A Logic for Time and Data Abstraction. In Richard E. Jones, editor, Proceedings of the 28superscriptth European Conference on Object-Oriented Programming, volume 8586 of Lecture Notes in Computer Science, pages 207-231. Springer, July 2014. URL: https://doi.org/10.1007/978-3-662-44202-9_9.
  18. Khuzaima Daudjee and Kenneth Salem. Lazy database replication with snapshot isolation. In Proceedings of the 32nd International Conference on Very Large Data Bases, VLDB ’06, page 715–726. VLDB Endowment, 2006. URL: https://doi.org/10.5555/1182635.1164189.
  19. Thomas Dinsdale-Young, Mike Dodds, Philippa Gardner, Matthew J. Parkinson, and Viktor Vafeiadis. Concurrent Abstract Predicates. In Proceedings of the 24superscriptth European Conference on Object-Oriented Programming, ECOOP'10, pages 504-528. Springer-Verlag, 2010. URL: https://doi.org/10.1007/978-3-642-14107-2_24.
  20. Simon Doherty, Brijesh Dongol, Heike Wehrheim, and John Derrick. Verifying C11 programs operationally. In Proceedings of the 24th Symposium on Principles and Practice of Parallel Programming, PPoPP '19, pages 355-365, New York, NY, USA, 2019. ACM. URL: https://doi.org/10.1145/3293883.3295702.
  21. Jiaqing Du, Sameh Elnikety, and Willy Zwaenepoel. Clock-SI: Snapshot Isolation for Partitioned Data Stores Using Loosely Synchronized Clocks. In Proceedings of the 32superscriptnd Leibniz International Proceedings in Informatics (LIPIcs), SRDS'13, pages 173-184, Washington, DC, USA, 2013. IEEE Computer Society. URL: https://doi.org/10.1109/SRDS.2013.26.
  22. Sameh Elnikety, Willy Zwaenepoel, and Fernando Pedone. Database replication using generalized snapshot isolation. In Proceedings of the 24th IEEE Symposium on Reliable Distributed Systems, SRDS ’05, page 73–84, USA, 2005. IEEE Computer Society. URL: https://doi.org/10.1109/RELDIS.2005.14.
  23. Alan Fekete, Dimitrios Liarokapis, Elizabeth O'Neil, Patrick O'Neil, and Dennis Shasha. Making Snapshot Isolation Serializable. ACM Transactions on Database Systems, 30(2):492-528, June 2005. URL: https://doi.org/10.1145/1071610.1071615.
  24. Alexey Gotsman, Hongseok Yang, Carla Ferreira, Mahsa Najafzadeh, and Marc Shapiro. ’cause i’m strong enough: Reasoning about consistency choices in distributed systems. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’16, page 371–384, New York, NY, USA, 2016. Association for Computing Machinery. URL: https://doi.org/10.1145/2837614.2837625.
  25. Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, and Derek Dreyer. Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning. In Proceedings of the 42superscriptnd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'15, pages 637-650. ACM, 2015. URL: https://doi.org/10.1145/2676726.2676980.
  26. Gowtham Kaki, Kapil Earanky, KC Sivaramakrishnan, and Suresh Jagannathan. Safe replication through bounded concurrency verification. Proc. ACM Program. Lang., 2(OOPSLA), October 2018. URL: https://doi.org/10.1145/3276534.
  27. Gowtham Kaki, Kartik Nagar, Mahsa Najafzadeh, and Suresh Jagannathan. Alone Together: Compositional Reasoning and Inference for Weak Isolation. Proceedings of the ACM on Programming Languages, 2(POPL):27:1-27:34, December 2017. URL: https://doi.org/10.1145/3158115.
  28. Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, and Derek Dreyer. A Promising Semantics for Relaxed-memory Concurrency. In Proceedings of the 44superscriptth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'17, pages 175-189, New York, NY, USA, 2017. ACM. URL: https://doi.org/10.1145/3009837.3009850.
  29. Eric Koskinen and Matthew Parkinson. The push/pull model of transactions. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’15, page 186–195, New York, NY, USA, 2015. Association for Computing Machinery. URL: https://doi.org/10.1145/2737924.2737995.
  30. Cheng Li, Daniel Porto, Allen Clement, Johannes Gehrke, Nuno Preguiça, and Rodrigo Rodrigues. Making geo-replicated systems fast as possible, consistent when necessary. In Proceedings of the 10th USENIX Conference on Operating Systems Design and Implementation, OSDI’12, page 265–278, USA, 2012. USENIX Association. URL: http://www.cs.otago.ac.nz/cosc440/readings/osdi12-final-162.pdf.
  31. Richard J. Lipton. Reduction: A method of proving properties of parallel programs. Commun. ACM, 18(12):717-721, December 1975. URL: https://doi.org/10.1145/361227.361234.
  32. Si Liu, Peter Csaba Ölveczky, Keshav Santhanam, Qi Wang, Indranil Gupta, and José Meseguer. ROLA: A New Distributed Transaction Protocol and Its Formal Analysis. In Alessandra Russo and Andy Schürr, editors, Fundamental Approaches to Software Engineering, pages 77-93, Cham, 2018. Springer. URL: https://doi.org/10.1007/978-3-319-89363-1_5.
  33. Wyatt Lloyd, Michael J. Freedman, Michael Kaminsky, and David G. Andersen. Don’t settle for eventual: Scalable causal consistency for wide-area storage with cops. In Proceedings of the Twenty-Third ACM Symposium on Operating Systems Principles, SOSP ’11, page 401–416, New York, NY, USA, 2011. Association for Computing Machinery. URL: https://doi.org/10.1145/2043556.2043593.
  34. Wyatt Lloyd, Michael J. Freedman, Michael Kaminsky, and David G. Andersen. Stronger Semantics for Low-Latency Geo-Replicated Storage. In Presented as part of the 10superscriptth USENIX Symposium on Networked Systems Design and Implementation, pages 313-328, Lombard, IL, 2013. USENIX. URL: https://www.usenix.org/conference/nsdi13/technical-sessions/presentation/lloyd.
  35. Kartik Nagar and Suresh Jagannathan. Automated Detection of Serializability Violations Under Weak Consistency. In Proceedings of the 29superscriptth International Conference on Concurrency Theory, pages 41:1-41:18, 2018. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2018.41.
  36. Aleksandar Nanevski, Yuy Ley-wild, Ilya Sergey, and Germán Andrés Delbianco. Communicating State Transition Systems for fine-grained concurrent resources, pages 290-310. Lecture Notes in Computer Science. springer-verlag, 2014. URL: https://doi.org/10.1007/978-3-642-54833-8_16.
  37. Christos H. Papadimitriou. The serializability of concurrent database updates. J. ACM, 26(4):631-653, October 1979. URL: https://doi.org/10.1145/322154.322158.
  38. Azalea Raad, Ori Lahav, and Viktor Vafeiadis. On Parallel Snapshot Isolation and Release/Acquire Consistency. In Amal Ahmed, editor, Proceedings of the 27superscriptth European Symposium on Programming, pages 940-967, Cham, 2018. Lecture Notes in Computer Science. URL: https://doi.org/10.1007/978-3-319-89884-1_33.
  39. The RUBiS benchmark, 2008. URL: https://rubis.ow2.org/index.html.
  40. Marc Shapiro, Nuno Preguiça, Carlos Baquero, and Marek Zawirski. Conflict-free replicated data types. In Proceedings of the 13th International Conference on Stabilization, Safety, and Security of Distributed Systems, SSS’11, page 386–400, Berlin, Heidelberg, 2011. Springer-Verlag. URL: https://doi.org/10.1007/978-3-642-24550-3_29.
  41. Dennis Shasha, Francois Llirbat, Eric Simon, and Patrick Valduriez. Transaction Chopping: Algorithms and Performance Studies. ACM Transactions on Database Systems, 20(3):325-363, September 1995. URL: https://doi.org/10.1145/211414.211427.
  42. Yair Sovran, Russell Power, Marcos K. Aguilera, and Jinyang Li. Transactional Storage for Geo-replicated Systems. In Proceedings of the 23superscriptrd ACM Symposium on Operating Systems Principles, SOSP'11, pages 385-400, New York, NY, USA, 2011. ACM. URL: https://doi.org/10.1145/2043556.2043592.
  43. Kristina Spirovska, Diego Didona, and Willy Zwaenepoel. Wren: Nonblocking Reads in a Partitioned Transactional Causally Consistent Data Store. In Proceedings of the 48superscriptth Annual IEEE/IFIP International Conference on Dependable Systems and Networks, DSN'18, pages 1-12, 2018. URL: https://doi.org/10.1109/DSN.2018.00014.
  44. The TPC-C benchmark, 1992. URL: http://www.tpc.org/tpcc/.
  45. Werner Vogels. Eventually consistent. Commun. ACM, 52(1):40–44, January 2009. URL: https://doi.org/10.1145/1435417.1435432.
  46. Shale Xiong. Parametric Operational Semantics for Consistency Models. PhD thesis, Imperial College London, April 2021. URL: http://www.shalexiong.com/thesis.pdf.
  47. Peter Zeller. Testing properties of weakly consistent programs with repliss. In Proceedings of the 3superscriptrd International Workshop on Principles and Practice of Consistency for Distributed Data, PaPoC'17, pages 3:1-3:5, New York, NY, USA, 2017. ACM. URL: https://doi.org/10.1145/3064889.3064893.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact