Document Open Access Logo

Toward Domain-Specific Solvers for Distributed Consistency

Authors Lindsey Kuper, Peter Alvaro

PDF
Thumbnail PDF

File

LIPIcs.SNAPL.2019.10.pdf
  • Filesize: 0.89 MB
  • 14 pages

Document Identifiers

Author Details

Lindsey Kuper
  • University of California, Santa Cruz, USA
Peter Alvaro
  • University of California, Santa Cruz, USA

Cite As Get BibTex

Lindsey Kuper and Peter Alvaro. Toward Domain-Specific Solvers for Distributed Consistency. In 3rd Summit on Advances in Programming Languages (SNAPL 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 136, pp. 10:1-10:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.SNAPL.2019.10

Abstract

To guard against machine failures, modern internet services store multiple replicas of the same application data within and across data centers, which introduces the problem of keeping geo-distributed replicas consistent with one another in the face of network partitions and unpredictable message latency. To avoid costly and conservative synchronization protocols, many real-world systems provide only weak consistency guarantees (e.g., eventual, causal, or PRAM consistency), which permit certain kinds of disagreement among replicas.
There has been much recent interest in language support for specifying and verifying such consistency properties. Although these properties are usually beyond the scope of what traditional type checkers or compiler analyses can guarantee, solver-aided languages are up to the task. Inspired by systems like Liquid Haskell [Vazou et al., 2014] and Rosette [Torlak and Bodik, 2014], we believe that close integration between a language and a solver is the right path to consistent-by-construction distributed applications. Unfortunately, verifying distributed consistency properties requires reasoning about transitive relations (e.g., causality or happens-before), partial orders (e.g., the lattice of replica states under a convergent merge operation), and properties relevant to message processing or API invocation (e.g., commutativity and idempotence) that cannot be easily or efficiently carried out by general-purpose SMT solvers that lack native support for this kind of reasoning.
We argue that domain-specific SMT-based tools that exploit the mathematical foundations of distributed consistency would enable both more efficient verification and improved ease of use for domain experts. The principle of exploiting domain knowledge for efficiency and expressivity that has borne fruit elsewhere - such as in the development of high-performance domain-specific languages that trade off generality to gain both performance and productivity - also applies here. Languages augmented with domain-specific, consistency-aware solvers would support the rapid implementation of formally verified programming abstractions that guarantee distributed consistency. In the long run, we aim to democratize the development of such domain-specific solvers by creating a framework for domain-specific solver development that brings new theory solver implementation within the reach of programmers who are not necessarily SMT solver internals experts.

Subject Classification

ACM Subject Classification
  • Theory of computation → Distributed computing models
  • Software and its engineering → Consistency
  • Software and its engineering → Software verification
Keywords
  • distributed consistency
  • SMT solving
  • theory solvers

Metrics

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

References

  1. Mustaque Ahamad, Gil Neiger, James E. Burns, Prince Kohli, and Phillip W. Hutto. Causal memory: definitions, implementation, and programming. Distributed Computing, 9(1):37-49, March 1995. URL: https://doi.org/10.1007/BF01784241.
  2. Peter Alvaro, Neil Conway, Joseph M. Hellerstein, and William R. Marczak. Consistency analysis in Bloom: A CALM and collected approach. In In Proceedings 5th Biennial Conference on Innovative Data Systems Research, pages 249-260, 2011. Google Scholar
  3. Peter Alvaro, Joshua Rosen, and Joseph M. Hellerstein. Lineage-driven Fault Injection. In Proceedings of the 2015 ACM SIGMOD International Conference on Management of Data, SIGMOD '15, pages 331-346, New York, NY, USA, 2015. ACM. URL: https://doi.org/10.1145/2723372.2723711.
  4. Hagit Attiya, Sebastian Burckhardt, Alexey Gotsman, Adam Morrison, Hongseok Yang, and Marek Zawirski. Specification and Complexity of Collaborative Text Editing. In Proceedings of the 2016 ACM Symposium on Principles of Distributed Computing, PODC '16, pages 259-268, New York, NY, USA, 2016. ACM. URL: https://doi.org/10.1145/2933057.2933090.
  5. Clark Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanović, Tim King, Andrew Reynolds, and Cesare Tinelli. CVC4. In Proceedings of the 23rd International Conference on Computer Aided Verification, CAV'11, pages 171-177, Berlin, Heidelberg, 2011. Springer-Verlag. URL: http://dl.acm.org/citation.cfm?id=2032305.2032319.
  6. Ahmed Bouajjani, Constantin Enea, and Jad Hamza. Verifying Eventual Consistency of Optimistic Replication Systems. SIGPLAN Not., 49(1):285-296, January 2014. URL: https://doi.org/10.1145/2578855.2535877.
  7. Kevin J. Brown, Arvind K. Sujeeth, Hyouk Joong Lee, Tiark Rompf, Hassan Chafi, Martin Odersky, and Kunle Olukotun. A Heterogeneous Parallel Framework for Domain-Specific Languages. In Proceedings of the 2011 International Conference on Parallel Architectures and Compilation Techniques, PACT '11, pages 89-100, Washington, DC, USA, 2011. IEEE Computer Society. URL: https://doi.org/10.1109/PACT.2011.15.
  8. Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, and Roberto Sebastiani. The MathSAT 4 SMT Solver. In Proceedings of the 20th International Conference on Computer Aided Verification, CAV '08, pages 299-303, Berlin, Heidelberg, 2008. Springer-Verlag. URL: https://doi.org/10.1007/978-3-540-70545-1_28.
  9. Sebastian Burckhardt, Manuel Fähndrich, Daan Leijen, and Benjamin P. Wood. Cloud Types for Eventual Consistency. In Proceedings of the 26th European Conference on Object-Oriented Programming, ECOOP'12, pages 283-307, Berlin, Heidelberg, 2012. Springer-Verlag. URL: https://doi.org/10.1007/978-3-642-31057-7_14.
  10. Sebastian Burckhardt, Alexey Gotsman, Hongseok Yang, and Marek Zawirski. Replicated Data Types: Specification, Verification, Optimality. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, pages 271-284, New York, NY, USA, 2014. ACM. URL: https://doi.org/10.1145/2535838.2535848.
  11. Luca Cardelli. A Semantics of Multiple Inheritance. In Information and Computation, pages 51-67. Springer-Verlag, 1988. Google Scholar
  12. Hassan Chafi, Arvind K. Sujeeth, Kevin J. Brown, HyoukJoong Lee, Anand R. Atreya, and Kunle Olukotun. A Domain-specific Approach to Heterogeneous Parallelism. In Proceedings of the 16th ACM Symposium on Principles and Practice of Parallel Programming, PPoPP '11, pages 35-46, New York, NY, USA, 2011. ACM. URL: https://doi.org/10.1145/1941553.1941561.
  13. Neil Conway, William R. Marczak, Peter Alvaro, Joseph M. Hellerstein, and David Maier. Logic and Lattices for Distributed Programming. In Proceedings of the Third ACM Symposium on Cloud Computing, SoCC '12, pages 1:1-1:14, New York, NY, USA, 2012. ACM. URL: https://doi.org/10.1145/2391229.2391230.
  14. Patrick Cousot and Radhia Cousot. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL '77, pages 238-252, New York, NY, USA, 1977. ACM. URL: https://doi.org/10.1145/512950.512973.
  15. Leonardo De Moura and Nikolaj Bjørner. Z3: An efficient SMT solver. In Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS'08/ETAPS'08, pages 337-340, Berlin, Heidelberg, 2008. Springer-Verlag. URL: http://dl.acm.org/citation.cfm?id=1792734.1792766.
  16. Giuseppe DeCandia, Deniz Hastorun, Madan Jampani, Gunavardhan Kakulapati, Avinash Lakshman, Alex Pilchin, Swaminathan Sivasubramanian, Peter Vosshall, and Werner Vogels. Dynamo: Amazon’s Highly Available Key-value Store. In Proceedings of Twenty-first ACM SIGOPS Symposium on Operating Systems Principles, SOSP '07, pages 205-220, New York, NY, USA, 2007. ACM. URL: https://doi.org/10.1145/1294261.1294281.
  17. Dorothy E. Denning. A Lattice Model of Secure Information Flow. Commun. ACM, 19(5):236-243, May 1976. URL: https://doi.org/10.1145/360051.360056.
  18. Cunjing Ge, Feifei Ma, Jeff Huang, and Jian Zhang. SMT solving for the theory of ordering constraints. In Revised Selected Papers of the 28th International Workshop on Languages and Compilers for Parallel Computing - Volume 9519, LCPC 2015, pages 287-302, Berlin, Heidelberg, 2016. Springer-Verlag. URL: https://doi.org/10.1007/978-3-319-29778-1_18.
  19. Victor B. F. Gomes, Martin Kleppmann, Dominic P. Mulligan, and Alastair R. Beresford. Verifying Strong Eventual Consistency in Distributed Systems. Proc. ACM Program. Lang., 1(OOPSLA):109:1-109:28, October 2017. URL: https://doi.org/10.1145/3133933.
  20. Brandon Holt, James Bornholt, Irene Zhang, Dan Ports, Mark Oskin, and Luis Ceze. Disciplined Inconsistency with Consistency Types. In Proceedings of the Seventh ACM Symposium on Cloud Computing, SoCC '16, pages 279-293, New York, NY, USA, 2016. ACM. URL: https://doi.org/10.1145/2987550.2987559.
  21. Guy Katz and Clark Barrett. Personal communication, 2017. Google Scholar
  22. Guy Katz, Clark W. Barrett, David L. Dill, Kyle Julian, and Mykel J. Kochenderfer. Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. In Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I, pages 97-117, 2017. URL: https://doi.org/10.1007/978-3-319-63387-9_5.
  23. Lindsey Kuper, Guy Katz, Justin Gottschlich, Kyle Julian, Clark Barrett, and Mykel J. Kochenderfer. Toward Scalable Verification for Safety-Critical Deep Networks. CoRR, abs/1801.05950, 2018. URL: http://arxiv.org/abs/1801.05950.
  24. Lindsey Kuper and Ryan R. Newton. LVars: Lattice-based data structures for deterministic parallelism. In Proceedings of the 2nd ACM SIGPLAN Workshop on Functional High-performance Computing, FHPC '13, pages 71-84, New York, NY, USA, 2013. ACM. URL: https://doi.org/10.1145/2502323.2502326.
  25. Lindsey Kuper, Aaron Todd, Sam Tobin-Hochstadt, and Ryan R. Newton. Taming the Parallel Effect Zoo: Extensible Deterministic Parallelism with LVish. In Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '14, pages 2-14, New York, NY, USA, 2014. ACM. URL: https://doi.org/10.1145/2594291.2594312.
  26. Lindsey Kuper, Aaron Turon, Neelakantan R. Krishnaswami, and Ryan R. Newton. Freeze After Writing: Quasi-deterministic Parallel Programming with LVars. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, pages 257-270, New York, NY, USA, 2014. ACM. URL: https://doi.org/10.1145/2535838.2535842.
  27. Leslie Lamport. Time, Clocks, and the Ordering of Events in a Distributed System. Commun. ACM, 21(7):558-565, July 1978. URL: https://doi.org/10.1145/359545.359563.
  28. Tanakorn Leesatapornwongsa, Jeffrey F. Lukman, Shan Lu, and Haryadi S. Gunawi. TaxDC: A Taxonomy of Non-Deterministic Concurrency Bugs in Datacenter Distributed Systems. In Proceedings of the Twenty-First International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS '16, pages 517-530, New York, NY, USA, 2016. ACM. URL: https://doi.org/10.1145/2872362.2872374.
  29. 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, pages 265-278, Berkeley, CA, USA, 2012. USENIX Association. URL: http://dl.acm.org/citation.cfm?id=2387880.2387906.
  30. R.J. Lipton and J.S. Sandberg. PRAM: A scalable shared memory. Technical Report no. 180, Princeton University, Department of Computer Science, 1988. Google Scholar
  31. 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, pages 401-416, New York, NY, USA, 2011. ACM. URL: https://doi.org/10.1145/2043556.2043593.
  32. Mae Milano and Andrew C. Myers. MixT: A language for mixing consistency in geodistributed transactions. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, pages 226-241, New York, NY, USA, 2018. ACM. URL: https://doi.org/10.1145/3192366.3192375.
  33. Kunle Olukotun. High Performance Embedded Domain Specific Languages. In Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming, ICFP '12, pages 139-140, New York, NY, USA, 2012. ACM. URL: https://doi.org/10.1145/2364527.2364548.
  34. Matthieu Perrin, Achour Mostefaoui, and Claude Jard. Causal Consistency: Beyond Memory. In Proceedings of the 21st ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP '16, pages 26:1-26:12, New York, NY, USA, 2016. ACM. URL: https://doi.org/10.1145/2851141.2851170.
  35. Luca Pulina and Armando Tacchella. An Abstraction-refinement Approach to Verification of Artificial Neural Networks. In Proceedings of the 22nd International Conference on Computer Aided Verification, CAV'10, pages 243-257, Berlin, Heidelberg, 2010. Springer-Verlag. URL: https://doi.org/10.1007/978-3-642-14295-6_24.
  36. Hyun-Gul Roh, Myeongjae Jeon, Jinsoo Kim, and Joonwon Lee. Replicated abstract data types: Building blocks for collaborative applications. J. Parallel Distrib. Comput., 71(3):354-368, 2011. URL: https://doi.org/10.1016/j.jpdc.2010.12.006.
  37. Patrick M. Rondon, Ming Kawaguci, and Ranjit Jhala. Liquid Types. In Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '08, pages 159-169, New York, NY, USA, 2008. ACM. URL: https://doi.org/10.1145/1375581.1375602.
  38. 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, pages 386-400, Berlin, Heidelberg, 2011. Springer-Verlag. URL: http://dl.acm.org/citation.cfm?id=2050613.2050642.
  39. KC Sivaramakrishnan, Gowtham Kaki, and Suresh Jagannathan. Declarative Programming over Eventually Consistent Data Stores. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '15, pages 413-424, New York, NY, USA, 2015. ACM. URL: https://doi.org/10.1145/2737924.2737981.
  40. Douglas B. Terry, Alan J. Demers, Karin Petersen, Mike Spreitzer, Marvin Theimer, and Brent W. Welch. Session Guarantees for Weakly Consistent Replicated Data. In Proceedings of the Third International Conference on Parallel and Distributed Information Systems, PDIS '94, pages 140-149, Washington, DC, USA, 1994. IEEE Computer Society. URL: http://dl.acm.org/citation.cfm?id=645792.668302.
  41. Emina Torlak and Rastislav Bodik. Growing Solver-aided Languages with Rosette. In Proceedings of the 2013 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming & Software, Onward! 2013, pages 135-152, New York, NY, USA, 2013. ACM. URL: https://doi.org/10.1145/2509578.2509586.
  42. Emina Torlak and Rastislav Bodik. A Lightweight Symbolic Virtual Machine for Solver-aided Host Languages. In Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '14, pages 530-541, New York, NY, USA, 2014. ACM. URL: https://doi.org/10.1145/2594291.2594340.
  43. Niki Vazou, Eric L. Seidel, and Ranjit Jhala. LiquidHaskell: Experience with refinement types in the real world. In Proceedings of the 2014 ACM SIGPLAN Symposium on Haskell, Haskell '14, pages 39-51, New York, NY, USA, 2014. ACM. URL: https://doi.org/10.1145/2633357.2633366.
  44. Niki Vazou, Anish Tondwalkar, Vikraman Choudhury, Ryan G. Scott, Ryan R. Newton, Philip Wadler, and Ranjit Jhala. Refinement Reflection: Complete Verification with SMT. Proc. ACM Program. Lang., 2(POPL):53:1-53:31, December 2017. URL: https://doi.org/10.1145/3158141.
  45. Paolo Viotti and Marko Vukolić. Consistency in Non-Transactional Distributed Storage Systems. ACM Comput. Surv., 49(1):19:1-19:34, June 2016. URL: https://doi.org/10.1145/2926965.
  46. Werner Vogels. Eventually Consistent. Commun. ACM, 52(1):40-44, January 2009. URL: https://doi.org/10.1145/1435417.1435432.
  47. Pamela Zave. Using Lightweight Modeling to Understand Chord. SIGCOMM Comput. Commun. Rev., 42(2):49-57, March 2012. URL: https://doi.org/10.1145/2185376.2185383.
  48. Peter Zeller, Annette Bieniusa, and Arnd Poetzsch-Heffter. Formal Specification and Verification of CRDTs. In Erika Ábrahám and Catuscia Palamidessi, editors, Formal Techniques for Distributed Objects, Components, and Systems, pages 33-48, Berlin, Heidelberg, 2014. Springer Berlin Heidelberg. Google Scholar
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 About DROPS Imprint Privacy Contact