Mergeable Replicated Data Types

被引:12
|
作者
Kaki, Gowtham [1 ]
Priya, Swarn [1 ]
Sivaramakrishnan, K. C. [2 ]
Jagannathan, Suresh [1 ]
机构
[1] Purdue Univ, W Lafayette, IN 47907 USA
[2] IIT Madras, Chennai, Tamil Nadu, India
来源
关键词
Replication; Weak Consistency; CRDTs; Git; Version Control;
D O I
10.1145/3360580
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
Programming geo-replicated distributed systems is challenging given the complexity of reasoning about different evolving states on different replicas. Existing approaches to this problem impose significant burden on application developers to consider the effect of how operations performed on one replica are witnessed and applied on others. To alleviate these challenges, we present a fundamentally different approach to programming in the presence of replicated state. Our insight is based on the use of invertible relational specifications of an inductively-defined data type as a mechanism to capture salient aspects of the data type relevant to how its different instances can be safely merged in a replicated environment. Importantly, because these specifications only address a data type's (static) structural properties, their formulation does not require exposing low-level system-level details concerning asynchrony, replication, visibility, etc. As a consequence, our framework enables the correct-by-construction synthesis of rich merge functions over arbitrarily complex ( i.e., composable) data types. We show that the use of a rich relational specification language allows us to extract sufficient conditions to automatically derive merge functions that have meaningful non-trivial convergence properties. We incorporate these ideas in a tool called Quark, and demonstrate its utility via a detailed evaluation study on real-world benchmarks.
引用
收藏
页数:29
相关论文
共 50 条
  • [1] Certified Mergeable Replicated Data Types
    Soundarapandian, Vimala
    Kamath, Adharsh
    Nagar, Kartik
    Sivaramakrishnan, K. C.
    [J]. PROCEEDINGS OF THE 43RD ACM SIGPLAN INTERNATIONAL CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION (PLDI '22), 2022, : 332 - 347
  • [2] Composite Replicated Data Types
    Gotsman, Alexey
    Yang, Hongseok
    [J]. PROGRAMMING LANGUAGES AND SYSTEMS, 2015, 9032 : 585 - 609
  • [3] A Denotational View of Replicated Data Types
    Gadducci, Fabio
    Melgratti, Hernan
    Roldan, Christian
    [J]. COORDINATION MODELS AND LANGUAGES, COORDINATION 2017, 2017, 10319 : 138 - 156
  • [4] HAMBAND: RDMA Replicated Data Types
    Houshmand, Farzin
    Saberlatibari, Javad
    Lesani, Mohsen
    [J]. PROCEEDINGS OF THE 43RD ACM SIGPLAN INTERNATIONAL CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION (PLDI '22), 2022, : 348 - 363
  • [5] Bounded Implementations of Replicated Data Types
    Mukund, Madhavan
    Shenoy, Gautham R.
    Suresh, S. P.
    [J]. VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION (VMCAI 2015), 2015, 8931 : 355 - 372
  • [6] Delta State replicated data types
    Almeida, Paulo Sergio
    Shoker, Ali
    Baquero, Carlos
    [J]. JOURNAL OF PARALLEL AND DISTRIBUTED COMPUTING, 2018, 111 : 162 - 173
  • [7] On the semantics and implementation of replicated data types
    Gadducci, Fabio
    Melgratti, Hernan
    Roldan, Christian
    [J]. SCIENCE OF COMPUTER PROGRAMMING, 2018, 167 : 91 - 113
  • [8] CONVERGENT AND COMMUTATIVE REPLICATED DATA TYPES
    Fatourou, Panagiota
    Shapiro, Marc
    Preguica, Nuno
    Baquero, Carlos
    Zawirski, Marek
    [J]. BULLETIN OF THE EUROPEAN ASSOCIATION FOR THEORETICAL COMPUTER SCIENCE, 2011, (104): : 67 - 88
  • [9] Data Structures for Mergeable Trees
    Georgiadis, Loukas
    Kaplan, Haim
    Shafrir, Nira
    Tarjan, Robert E.
    Werneck, Renato F.
    [J]. ACM TRANSACTIONS ON ALGORITHMS, 2011, 7 (02)
  • [10] Conflict-Free Replicated Data Types
    Shapiro, Marc
    Preguica, Nuno
    Baquero, Carlos
    Zawirski, Marek
    [J]. STABILIZATION, SAFETY, AND SECURITY OF DISTRIBUTED SYSTEMS, 2011, 6976 : 386 - +