Composite Replicated Data Types

详细信息    查看全文

• 作者：Alexey Gotsman (14)
  Hongseok Yang (15)
  
  14. IMDEA Software Institute ; Madrid ; Spain
  15. University of Oxford ; Oxford ; UK
  
• 刊名：Lecture Notes in Computer Science
• 出版年：2015
• 出版时间：2015
• 年：2015
• 卷：9032
• 期：1
• 页码：585-609
• 全文大小：541 KB
• 参考文献：1. Extended version of this paper. Available from the submission system
  2. Microsoft TouchDevelop, https://www.touchdevelop.com/
  3. Abadi, D.: Consistency tradeoffs in modern distributed database system design: CAP is only part of the story. IEEE Computer (2012)
  4. Bailis, P., Davidson, A., Fekete, A., Ghodsi, A., Hellerstein, J.M., Stoica, I.: Highly Available Transactions: virtues and limitations. In: VLDB (2014)
  5. Bailis, P., Ghodsi, A.: Eventual consistency today: Limitations, extensions, and beyond. CACM聽56(5) (2013)
  6. Batty, M., Dodds, M., Gotsman, A.: Library abstraction for C/C++ concurrency. In: POPL (2013)
  7. Batty, M., Owens, S., Sarkar, S., Sewell, P., Weber, T.: Mathematizing C++ concurrency. In: POPL (2011)
  8. Bieniusa, A., Zawirski, M., Pregui莽a, N.M., Shapiro, M., Baquero, C., Balegas, V., Duarte, S.: Semantics of eventually consistent replicated sets. In: DISC (2012)
  9. Burckhardt, S., Gotsman, A., Musuvathi, M., Yang, H. Concurrent library correctness on the TSO memory model. In: Seidl, H. eds. (2012) Programming Languages and Systems. Springer, Heidelberg, pp. 87-107
  10. Burckhardt, S., Gotsman, A., Yang, H.: Understanding eventual consistency. Technical Report MSR-TR-2013-39, Microsoft (2013)
  11. Burckhardt, S., Gotsman, A., Yang, H., Zawirski, M.: Replicated data types: specification, verification, optimality. In: POPL (2014)
  12. Burckhardt, S., Leijen, D., F盲hndrich, M., Sagiv, M. Eventually consistent transactions. In: Seidl, H. eds. (2012) Programming Languages and Systems. Springer, Heidelberg, pp. 67-86
  13. Filipovic, I., O鈥橦earn, P.W., Rinetzky, N., Yang, H.: Abstraction for concurrent objects. Theor. Comput. Sci.聽411(51-52) (2010)
  14. Gilbert, S., Lynch, N.: Brewer鈥檚 conjecture and the feasibility of consistent, available, partition-tolerant web services. SIGACT News聽33(2) (2002)
  15. Hoare, C.A.R.: Proof of correctness of data representations. Acta. Inf.聽1 (1972)
  16. Jagadeesan, R., Petri, G., Pitcher, C., Riely, J. Quarantining weakness. In: Felleisen, M., Gardner, P. eds. (2013) Programming Languages and Systems. Springer, Heidelberg, pp. 492-511
  17. Li, C., Porto, D., Clement, A., Rodrigues, R., Pregui莽a, N., Gehrke, J.: Making geo-replicated systems fast if possible, consistent when necessary. In: OSDI (2012)
  18. Lloyd, W., Freedman, M.J., Kaminsky, M., Andersen, D.G.: Don鈥檛 settle for eventual: scalable causal consistency for wide-area storage with COPS. In: SOSP (2011)
  19. Lloyd, W., Freedman, M.J., Kaminsky, M., Andersen, D.G.: Stronger semantics for low-latency geo-replicated storage. In: NSDI (2013)
  20. Nielsen, M., Plotkin, G.D., Winskel, G.: Petri nets, event structures and domains. In: Semantics of Concurrent Computation (1979)
  21. Nielsen, M., Sassone, V., Winskel, G.: Relationships between models of concurrency. In: REX School/Symposium (1993)
  22. M.聽Shapiro, N.聽Pregui莽a, C.聽Baquero, and M.聽Zawirski. A comprehensive study of Convergent and Commutative Replicated Data Types. Technical Report 7506, INRIA (2011)
  23. Shapiro, M., Pregui莽a, N., Baquero, C., Zawirski, M. Conflict-free replicated data types. In: D茅fago, X., Petit, F., Villain, V. eds. (2011) Stabilization, Safety, and Security of Distributed Systems. Springer, Heidelberg, pp. 386-400
  24. Sovran, Y., Power, R., Aguilera, M.K., Li, J.: Transactional storage for geo-replicated systems. In: SOSP (2011)
  25. Turon, A., Dreyer, D., Birkedal, L.: Unifying refinement and Hoare-style reasoning in a logic for higher-order concurrency. In: ICFP (2013)
  26. Zawirski, M., Bieniusa, A., Balegas, V., Duarte, S., Baquero, C., Shapiro, M., Pregui莽a, N.: SwiftCloud: Fault-tolerant geo-replication integrated all the way to the client machine. Technical Report 8347, INRIA (2013)
  
• 作者单位：Programming Languages and Systems
• 丛书名：978-3-662-46668-1
• 刊物类别：Computer Science
• 刊物主题：Artificial Intelligence and Robotics
  Computer Communication Networks
  Software Engineering
  Data Encryption
  Database Management
  Computation by Abstract Devices
  Algorithm Analysis and Problem Complexity
  
• 出版者：Springer Berlin / Heidelberg
• ISSN：1611-3349

文摘

Modern large-scale distributed systems often rely on eventually consistent replicated stores, which achieve scalability in exchange for providing weak semantic guarantees. To compensate for this weakness, researchers have proposed various abstractions for programming on eventual consistency, such as replicated data types for resolving conflicting updates at different replicas and weak forms of transactions for maintaining relationships among objects. However, the subtle semantics of these abstractions makes using them correctly far from trivial. To address this challenge, we propose composite replicated data types, which formalise a common way of organising applications on top of eventually consistent stores. Similarly to an abstract data type, a composite data type encapsulates objects of replicated data types and operations used to access them, implemented using transactions.We develop a method for reasoning about programs with composite data types that reflects their modularity: the method allows abstracting away the internals of composite data type implementations when reasoning about their clients. We express the method as a denotational semantics for a programming language with composite data types. We demonstrate the effectiveness of our semantics by applying it to verify subtle data type examples and prove that it is sound and complete with respect to a standard non-compositional semantics.