Farzin Houshmand
Skip Abstract Section
Skip Supplemental Material SectionAbstract
Distributed system replication is widely used as a means of fault-tolerance and scalability. However, it provides a spectrum of consistency choices that impose a dilemma for clients between correctness, responsiveness and availability. Given a sequential object and its integrity properties, we automatically synthesize a replicated object that guarantees state integrity and convergence and avoids unnecessary coordination. Our approach is based on a novel sufficient condition for integrity and convergence called well-coordination that requires certain orders between conflicting and dependent operations. We statically analyze the given sequential object to decide its conflicting and dependent methods and use this information to avoid coordination. We present novel coordination protocols that are parametric in terms of the analysis results and provide the well-coordination requirements. We implemented a tool called Hamsaz that can automatically analyze the given object, instantiate the protocols and synthesize replicated objects. We have applied Hamsaz to a suite of use-cases and synthesized replicated objects that are significantly more responsive than the strongly consistent baseline.
Supplemental Material
- Daniel Abadi. 2012. Consistency Tradeoffs in Modern Distributed Database System Design. Computer 45, 2 (2012), 6. Google Scholar
Digital Library
- Mustaque Ahamad, Gil Neiger, James E Burns, Prince Kohli, and Phillip W Hutto. 1995. Causal memory: Definitions, implementation, and programming. Distributed Computing 9, 1 (1995). Google ScholarDigital Library
- Peter Alvaro, Neil Conway, Joseph M. Hellerstein, and David Maier. 2017. Blazes: Coordination Analysis and Placement for Distributed Programs. ACM Trans. Database Syst. 42, 4, Article 23 (Oct. 2017), 31 pages. Google ScholarDigital Library
- Zachary R. Anderson, David Gay, and Mayur Naik. 2009. Lightweight annotations for controlling sharing in concurrent data structures. In Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2009, Dublin, Ireland, June 15-21, 2009. 98–109. Google ScholarDigital Library
- Appendix. 2018. Appendix. https://www.cs.ucr.edu/~lesani/companion/popl19/Appendix.pdf . (2018).Google Scholar
- Peter Bailis, Alan Fekete, Michael J. Franklin, Ali Ghodsi, Joseph M. Hellerstein, and Ion Stoica. 2014. Coordination Avoidance in Database Systems. Proc. VLDB Endow. 8, 3 (Nov. 2014), 185–196. Google ScholarDigital Library
- Peter Bailis, Alan Fekete, Michael J Franklin, Ali Ghodsi, Joseph M Hellerstein, and Ion Stoica. 2015. Feral concurrency control: An empirical investigation of modern application integrity. In Proceedings of the 2015 ACM SIGMOD International Conference on Management of Data. ACM, 1327–1342. Google ScholarDigital Library
- Peter Bailis, Alan Fekete, Ali Ghodsi, Joseph M Hellerstein, and Ion Stoica. 2012a. The potential dangers of causal consistency and an explicit solution. In Proceedings of the Third ACM Symposium on Cloud Computing. ACM, 22. Google ScholarDigital Library
- Peter Bailis, Shivaram Venkataraman, Michael J Franklin, Joseph M Hellerstein, and Ion Stoica. 2012b. Probabilistically bounded staleness for practical partial quorums. Proceedings of the VLDB Endowment 5, 8 (2012), 776–787. Google ScholarDigital Library
- Valter Balegas, Sérgio Duarte, Carla Ferreira, Rodrigo Rodrigues, Nuno Preguica, Mahsa Najafzadeh, and Marc Shapiro. 2015a. Putting Consistency Back into Eventual Consistency. In Proceedings of the Tenth European Conference on Computer Systems (EuroSys ’15). ACM, New York, NY, USA, Article 6, 16 pages. Google ScholarDigital Library
- Valter Balegas, Sérgio Duarte, Carla Ferreira, Rodrigo Rodrigues, Nuno Preguica, Mahsa Najafzadeh, and Marc Shapiro. 2015b. Towards Fast Invariant Preservation in Geo-replicated Systems. SIGOPS Oper. Syst. Rev. 49, 1 (Jan. 2015), 121–125. Google ScholarDigital Library
- Kshitij Bansal, Andrew Reynolds, Clark Barrett, and Cesare Tinelli. 2016. A new decision procedure for finite sets and cardinality constraints in SMT. In International Joint Conference on Automated Reasoning. Springer, 82–98. Google ScholarDigital Library
- Clark Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovi’c, Tim King, Andrew Reynolds, and Cesare Tinelli. 2011. CVC4. In Proceedings of the 23rd International Conference on Computer Aided Verification (CAV ’11) (Lecture Notes in Computer Science), Ganesh Gopalakrishnan and Shaz Qadeer (Eds.), Vol. 6806. Springer, 171–177. http://www.cs.stanford.edu/~barrett/pubs/BCD+11.pdf Snowbird, Utah. Google ScholarDigital Library
- Clark Barrett, Aaron Stump, and Cesare Tinelli. 2010. The SMT-LIB Standard: Version 2.0. In Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (Edinburgh, UK), A. Gupta and D. Kroening (Eds.).Google Scholar
- Nalini Belaramani, Mike Dahlin, Lei Gao, Amol Nayate, Arun Venkataramani, Praveen Yalagandula, and Jiandan Zheng. 2006. PRACTI Replication. In Proc. NSDI. Google ScholarDigital Library
- Giovanni Bernardi and Alexey Gotsman. 2016. Robustness against consistency models with atomic visibility. In LIPIcs-Leibniz International Proceedings in Informatics, Vol. 59. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik.Google Scholar
- Kenneth P. Birman. 1985. Replication and Fault-Tolerance in the ISIS System. In Proc. SOSP. Google ScholarDigital Library
- A. Bouajjani, C. Enea, and J. Hamza. 2014. Verifying Eventual Consistency of Optimistic Replication Systems. In Proc. POPL. Google ScholarDigital Library
- Coen Bron and Joep Kerbosch. 1973. Algorithm 457: Finding All Cliques of an Undirected Graph. Commun. ACM 16, 9 (Sept. 1973), 575–577. Google ScholarDigital Library
- Lucas Brutschy, Dimitar Dimitrov, Peter Müller, and Martin Vechev. 2017. Serializability for Eventual Consistency: Criterion, Analysis, and Applications. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017). ACM, New York, NY, USA, 458–472. Google ScholarDigital Library
- Sebastian Burckhardt, Alexey Gotsman, Hongseok Yang, and Marek Zawirski. 2014. Replicated Data Types: Specification, Verification, Optimality. In Proc. POPL. Google ScholarDigital Library
- Christian Cachin, Rachid Guerraoui, and Lus Rodrigues. 2011. Introduction to Reliable and Secure Distributed Programming (2nd ed.). Springer Publishing Company, Incorporated. Google ScholarDigital Library
- Domenico Cantone, Eugenio Omodeo, and Alberto Policriti. 2013. Set theory for computing: from decision procedures to declarative programming with sets. Springer Science & Business Media.Google Scholar
- Domenico Cantone and Calogero G Zarba. 2000. A new fast tableau-based decision procedure for an unquantified fragment of set theory. In Automated Deduction in Classical and Non-Classical Logics. Springer, 126–136. Google ScholarDigital Library
- Nuno Carvalho and et. al. 2011. APPIA Framework. http://appia.di.fc.ul.pt/wiki/index.php?title=Main_Page . (2011). Accessed: 2018-06-23.Google Scholar
- Andrea Cerone, Giovanni Bernardi, and Alexey Gotsman. 2015. A framework for transactional consistency models with atomic visibility. In LIPIcs-Leibniz International Proceedings in Informatics, Vol. 42. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik.Google Scholar
- Kevin Clancy and Heather Miller. 2017. Monotonicity Types for Distributed Dataflow. In Proceedings of the Programming Models and Languages for Distributed Computing. ACM, 2. Google ScholarDigital Library
- Brian F. Cooper, Raghu Ramakrishnan, Utkarsh Srivastava, Adam Silberstein, Philip Bohannon, Hans-Arno Jacobsen, Nick Puz, Daniel Weaver, and Ramana Yerneni. 2008. PNUTS: Yahoo!’s Hosted Data Serving Platform. Proc. VLDB Endow. 1, 2 (2008), 12. Google ScholarDigital Library
- 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 Proc. SOSP. Google ScholarDigital Library
- Michael Emmi and Constantin Enea. 2018. Monitoring Weak Consistency. In Proc. CAV.Google ScholarCross Ref
- Alan Fekete. 2005. Allocating Isolation Levels to Transactions. In Proceedings of the Twenty-fourth ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems (PODS ’05). ACM, New York, NY, USA, 206–215. Google ScholarDigital Library
- Alan Fekete, Dimitrios Liarokapis, Elizabeth O’Neil, Patrick O’Neil, and Dennis Shasha. 2005. Making Snapshot Isolation Serializable. ACM Trans. Database Syst. 30, 2 (June 2005), 492–528. Google ScholarDigital Library
- Michael J. Fischer, Nancy A. Lynch, and Michael S. Paterson. 1985. Impossibility of Distributed Consensus with One Faulty Process. J. ACM 32, 2 (April 1985), 374–382. Google ScholarDigital Library
- Seth Gilbert and Nancy Lynch. 2002. Brewer’s Conjecture and the Feasibility of Consistent, Available, Partition-tolerant Web Services. SIGACT News 33, 2 (June 2002), 9. Google ScholarDigital Library
- Seth Gilbert and Nancy A. Lynch. 2012. Perspectives on the CAP Theorem. IEEE Computer 45, 2 (2012), 30–36. Google ScholarDigital Library
- 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 Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’16). ACM, New York, NY, USA, 371–384. Google ScholarDigital Library
- Rachid Guerraoui, Matej Pavlovic, and Dragos-Adrian Seredinschi. 2016. Incremental Consistency Guarantees for Replicated Objects.. In OSDI. 169–184. Google ScholarDigital Library
- Jan Hoffmann, Michael Marmar, and Zhong Shao. 2013. Quantitative reasoning for proving lock-freedom. In Proceedings of the 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science. IEEE Computer Society, 124–133. Google ScholarDigital Library
- Brandon Holt, James Bornholt, Irene Zhang, Dan Ports, Mark Oskin, and Luis Ceze. 2016. Disciplined Inconsistency with Consistency Types. In Proceedings of the Seventh ACM Symposium on Cloud Computing (SoCC ’16). ACM, New York, NY, USA, 279–293. Google ScholarDigital Library
- Xin Jin, Xiaozhou Li, Haoyu Zhang, Nate Foster, Jeongkeun Lee, Robert Soule, Changhoon Kim, and Ion Stoica. 2018. NetChain: Scale-Free Sub-RT T Coordination. In 15th USENIX Symposium on Networked Systems Design and Implementation (NSDI 18). USENIX Association.Google Scholar
- Cliff B. Jones. 1983. Tentative steps toward a development method for interfering programs. ACM Transactions on Programming Languages and Systems (TOPLAS) 5, 4 (1983), 596–619. Google ScholarDigital Library
- Gowtham Kaki, Kartik Nagar, Mahsa Najafzadeh, and Suresh Jagannathan. 2017. Alone Together: Compositional Reasoning and Inference for Weak Isolation. Proc. ACM Program. Lang. 2, POPL, Article 27 (Dec. 2017), 34 pages. Google ScholarDigital Library
- Tim Kraska, Martin Hentschel, Gustavo Alonso, and Donald Kossmann. 2009. Consistency Rationing in the Cloud: Pay Only when It Matters. Proc. VLDB Endow. 2, 1 (Aug. 2009), 253–264. Google ScholarDigital Library
- Viktor Kuncak and Martin Rinard. 2007. Towards efficient satisfiability checking for Boolean Algebra with Presburger Arithmetic. In International Conference on Automated Deduction. Springer, 215–230. Google ScholarDigital Library
- Rivka Ladin, Barbara Liskov, Liuba Shrira, and Sanjay Ghemawat. 1992. Providing High Availability Using Lazy Replication. ACM Trans. Comput. Syst. 10, 4 (1992), 32. Google ScholarDigital Library
- Ori Lahav and Viktor Vafeiadis. 2015. Owicki-Gries reasoning for weak memory models. In International Colloquium on Automata, Languages, and Programming. Springer, 311–323. Google ScholarDigital Library
- Leslie Lamport. 1978. Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21, 7 (1978). Google ScholarDigital Library
- Leslie Lamport. 1998. The Part-time Parliament. ACM Trans. Comput. Syst. 16, 2 (1998). Google ScholarDigital Library
- Cheng Li, João Leitão, Allen Clement, Nuno Preguica, Rodrigo Rodrigues, and Viktor Vafeiadis. 2014. Automating the Choice of Consistency Levels in Replicated Systems. In Proceedings of the 2014 USENIX Conference on USENIX Annual Technical Conference (USENIX ATC’14). USENIX Association, Berkeley, CA, USA, 281–292. http://dl.acm.org/citation. cfm?id=2643634.2643664 Google ScholarDigital Library
- Cheng Li, João Leitão, Allen Clement, Nuno Preguica, and Rodrigo Rodrigues. 2015. Minimizing coordination in replicated systems. In Proceedings of the First Workshop on Principles and Practice of Consistency for Distributed Data. ACM, 8. Google ScholarDigital Library
- Cheng Li, Daniel Porto, Allen Clement, Johannes Gehrke, Nuno Preguica, and Rodrigo Rodrigues. 2012. Making Georeplicated Systems Fast As Possible, Consistent when Necessary. In Proceedings of the 10th USENIX Conference on Operating Systems Design and Implementation (OSDI’12). USENIX Association, Berkeley, CA, USA, 265–278. http: //dl.acm.org/citation.cfm?id=2387880.2387906 Google ScholarDigital Library
- Richard J. Lipton. 1975. Reduction: A Method of Proving Properties of Parallel Programs. Commun. ACM 18, 12 (Dec. 1975), 717–721. Google ScholarDigital Library
- Jed Liu, Tom Magrino, Owen Arden, Michael D. George, and Andrew C. Myers. 2014. Warranties for Faster Strong Consistency. In Proceedings of the 11th USENIX Conference on Networked Systems Design and Implementation (NSDI’14). USENIX Association, Berkeley, CA, USA, 503–517. http://dl.acm.org/citation.cfm?id=2616448.2616495 Google ScholarDigital Library
- 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 Proc. SOSP. Google ScholarDigital Library
- Wyatt Lloyd, Michael J. Freedman, Michael Kaminsky, and David G. Andersen. 2013. Stronger Semantics for Low-latency Geo-replicated Storage. In Proc. NSDI. Google ScholarDigital Library
- Shiyong Lu, Arthur Bernstein, and Philip Lewis. 2004. Correct execution of transactions at different isolation levels. IEEE Transactions on Knowledge and Data Engineering 16, 9 (2004), 1070–1081. Google ScholarDigital Library
- P. Madhusudan and P.S. Thiagarajan. 2001. Distributed Controller Synthesis for Local Specifications. In Automata, Languages and Programming, Fernando Orejas, Paul G. Spirakis, and Jan van Leeuwen (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 396–407. Google ScholarDigital Library
- Baoluo Meng, Andrew Reynolds, Cesare Tinelli, and Clark Barrett. 2017. Relational Constraint Solving in SMT. In International Conference on Automated Deduction. Springer, 148–165.Google Scholar
- Matthew Milano and Andrew C Myers. 2018. MixT: A Language for Mixing Consistency in Geodistributed Transactions. (2018).Google Scholar
- Mahsa Najafzadeh, Alexey Gotsman, Hongseok Yang, Carla Ferreira, and Marc Shapiro. 2016. The CISE Tool: Proving Weakly-consistent Applications Correct. In Proceedings of the 2Nd Workshop on the Principles and Practice of Consistency for Distributed Data (PaPoC ’16). ACM, New York, NY, USA, Article 2, 3 pages. Google ScholarDigital Library
- Francesco Zappa Nardelli, Peter Sewell, Jaroslav Sevcik, Susmit Sarkar, Scott Owens, Luc Maranget, Mark Batty, and Jade Alglave. 2009. Relaxed memory models must be rigorous. In Exploiting Concurrency Efficiently and Correctly Workshop.Google Scholar
- Peter W. OHearn. 2007. Resources, concurrency, and local reasoning. Theor. Comput. Sci. 375, 1-3 (2007), 271–307. Google ScholarDigital Library
- Brian M. Oki and Barbara H. Liskov. 1988. Viewstamped Replication: A New Primary Copy Method to Support HighlyAvailable Distributed Systems. In Proceedings of the Seventh Annual ACM Symposium on Principles of Distributed Computing (PODC ’88). ACM, New York, NY, USA, 8–17. Google ScholarDigital Library
- Diego Ongaro and John Ousterhout. 2014. In Search of an Understandable Consensus Algorithm. In Proceedings of the 2014 USENIX Conference on USENIX Annual Technical Conference (USENIX ATC’14). USENIX Association, Berkeley, CA, USA, 305–320. http://dl.acm.org/citation.cfm?id=2643634.2643666 Google ScholarDigital Library
- Susan Owicki and David Gries. 1976. An axiomatic proof technique for parallel programs I. Acta Informatica 6, 4 (1976), 319–340. Google ScholarDigital Library
- Karin Petersen, Mike J. Spreitzer, Douglas B. Terry, Marvin M. Theimer, and Alan J. Demers. 1997. Flexible Update Propagation for Weakly Consistent Replication. In Proc. SOSP. Google ScholarDigital Library
- Krithi Ramamritham and Calton Pu. 1995. A formal characterization of epsilon serializability. IEEE Transactions on Knowledge and Data Engineering 7, 6 (1995), 997–1007. Google ScholarDigital Library
- Sudip Roy, Lucja Kot, Gabriel Bender, Bailu Ding, Hossein Hojjat, Christoph Koch, Nate Foster, and Johannes Gehrke. 2015. The Homeostasis Protocol: Avoiding Transaction Coordination Through Program Analysis. In Proceedings of the 2015 ACM SIGMOD International Conference on Management of Data (SIGMOD ’15). ACM, New York, NY, USA, 1311–1326. Google ScholarDigital Library
- Marc Shapiro, Nuno Preguica, Carlos Baquero, and Marek Zawirski. 2011. A comprehensive study of Convergent and Commutative Replicated Data Types. Technical Report RR-7506. INRIA.Google Scholar
- KC Sivaramakrishnan, Gowtham Kaki, and Suresh Jagannathan. 2015. Declarative Programming over Eventually Consistent Data Stores. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’15). ACM, New York, NY, USA, 413–424. Google ScholarDigital Library
- Yair Sovran, Russell Power, Marcos K. Aguilera, and Jinyang Li. 2011. Transactional Storage for Geo-replicated Systems. In Proceedings of the Twenty-Third ACM Symposium on Operating Systems Principles (SOSP ’11). ACM, New York, NY, USA, 385–400. Google ScholarDigital Library
- Philippe Suter, Robin Steiger, and Viktor Kuncak. 2011. Sets with cardinality constraints in satisfiability modulo theories. In International Workshop on Verification, Model Checking, and Abstract Interpretation. Springer, 403–418. Google ScholarDigital Library
- Douglas B. Terry, Vijayan Prabhakaran, Ramakrishna Kotla, Mahesh Balakrishnan, Marcos K. Aguilera, and Hussam AbuLibdeh. 2013. Consistency-based Service Level Agreements for Cloud Storage. In Proceedings of the Twenty-Fourth ACM Symposium on Operating Systems Principles (SOSP ’13). ACM, New York, NY, USA, 309–324. Google ScholarDigital Library
- Shuji Tsukiyama, Mikio Ide, Hiromu Ariyoshi, and Isao Shirakawa. 1977. A New Algorithm for Generating All the Maximal Independent Sets. SIAM J. Comput. 6, 3 (1977), 505–517. http://scitation.aip.org/getabs/servlet/GetabsServlet?prog= normal&id=SMJCAT000006000003000505000001&idtype=cvips&gifs=yesGoogle ScholarDigital Library
- Werner Vogels. 2008. Eventually consistent. ACM Queue 6, 6 (2008). Google ScholarDigital Library
- Haifeng Yu and Amin Vahdat. 2000. Design and evaluation of a continuous consistency model for replicated services. In Proceedings of the 4th Conference on Symposium on Operating System Design & Implementation-Volume 4. USENIX Association, 21. Google ScholarDigital Library
Index Terms
- Hamsaz: replication coordination analysis and synthesis
Recommendations
Adaptive trade-off between consistency and performance in data replication
Replication is widely adopted in modern Internet applications and distributed systems to improve the reliability and performance. Though maintaining the strong consistency among replicas can guarantee the correctness of application behaviors, however, ...
Replication-aware linearizability
PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and ImplementationDistributed systems often replicate data at multiple locations to achieve availability despite network partitions. These systems accept updates at any replica and propagate them asynchronously to every other replica. Conflict-Free Replicated Data Types (...
Optimistic replication
Data replication is a key technology in distributed systems that enables higher availability and performance. This article surveys optimistic replication algorithms. They allow replica contents to diverge in the short term to support concurrent work ...
Comments