LIPIcs.CALCO.2023.22.pdf
- Filesize: 0.59 MB
- 5 pages
Document
CRDTs, Coalgebraically (Early Ideas)
Authors
Nathan Liittschwager 
,
Stelios Tsampas ,
Jonathan Castello ,
Lindsey Kuper
-
Part of:
Volume:
10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Conference on Algebra and Coalgebra in Computer Science (CALCO) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2023-09-02
File
Document Identifiers
Author Details
Cite AsGet BibTex
Nathan Liittschwager, Stelios Tsampas, Jonathan Castello, and Lindsey Kuper. CRDTs, Coalgebraically (Early Ideas). In 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 270, pp. 22:1-22:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.CALCO.2023.22
https://doi.org/10.4230/LIPIcs.CALCO.2023.22
Abstract
We describe ongoing work that models conflict-free replicated data types (CRDTs) from a coalgebraic point of view. CRDTs are data structures designed for replication across multiple physical locations in a distributed system. We show how to model a CRDT at the local replica level using a novel coalgebraic semantics for CRDTs. We believe this is the first step towards presenting a unified theory for specifying and verifying CRDTs and replicated state machines. As a case study, we consider emulation of CRDTs in terms of coalgebra.
Subject Classification
ACM Subject Classification
- Theory of computation
- Theory of computation → Semantics and reasoning
- Theory of computation → Distributed computing models
- Theory of computation → Concurrency
- Theory of computation → Formal languages and automata theory
Keywords
- Coalgebra
- Distributed Systems
- Concurrency
- Bisimulation
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- 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. Association for Computing Machinery. URL: https://doi.org/10.1145/2535838.2535848.
-
C. J. Fidge. Timestamps in message-passing systems that preserve the partial ordering. Proceedings of the 11th Australian Computer Science Conference, 10(1):56-66, 1988.
- 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), October 2017. URL: https://doi.org/10.1145/3133933.
- Bart Jacobs. Introduction to Coalgebra: Towards Mathematics of States and Observation, volume 59 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2016. URL: https://doi.org/10.1017/CBO9781316823187.
- 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.
- Hongjin Liang and Xinyu Feng. Abstraction for conflict-free replicated data types. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2021, pages 636-650, New York, NY, USA, 2021. Association for Computing Machinery. URL: https://doi.org/10.1145/3453483.3454067.
- Yiyun Liu, James Parker, Patrick Redmond, Lindsey Kuper, Michael Hicks, and Niki Vazou. Verifying replicated data types with typeclass refinements in Liquid Haskell. Proc. ACM Program. Lang., 4(OOPSLA), November 2020. URL: https://doi.org/10.1145/3428284.
-
Friedemann Mattern. Virtual time and global states of distributed systems. In Parallel and Distributed Algorithms, pages 215-226. North-Holland, 1989.
-
Kartik Nagar and Suresh Jagannathan. Automated parameterized verification of CRDTs. In Isil Dillig and Serdar Tasiran, editors, Computer Aided Verification, pages 459-477, Cham, 2019. Springer International Publishing.
- Abel Nieto, Léon Gondelman, Alban Reynaud, Amin Timany, and Lars Birkedal. Modular verification of op-based CRDTs in separation logic. Proc. ACM Program. Lang., 6(OOPSLA2), October 2022. URL: https://doi.org/10.1145/3563351.
- Fred B. Schneider. Implementing fault-tolerant services using the state machine approach: A tutorial. ACM Comput. Surv., 22(4):299-319, December 1990. URL: https://doi.org/10.1145/98163.98167.
- Reinhard Schwarz and Friedemann Mattern. Detecting causal relationships in distributed computations: In search of the holy grail. Distributed Computing, 7(3):149-174, March 1994. URL: https://doi.org/10.1007/BF02277859.
- Marc Shapiro, Nuno Preguiça, Carlos Baquero, and Marek Zawirski. A comprehensive study of Convergent and Commutative Replicated Data Types. Research Report RR-7506, Inria - Centre Paris-Rocquencourt; INRIA, January 2011. URL: https://hal.inria.fr/inria-00555588.
-
Marc Shapiro, Nuno Preguiça, Carlos Baquero, and Marek Zawirski. Conflict-free replicated data types. In Xavier Défago, Franck Petit, and Vincent Villain, editors, Stabilization, Safety, and Security of Distributed Systems, pages 386-400, Berlin, Heidelberg, 2011. Springer Berlin Heidelberg.