Document Open Access Logo

CRDTs, Coalgebraically (Early Ideas)

Authors Nathan Liittschwager , Stelios Tsampas , Jonathan Castello , Lindsey Kuper

PDF

File

Thumbnail PDF
PDF
LIPIcs.CALCO.2023.22.pdf
  • Filesize: 0.59 MB
  • 5 pages

Document Identifiers

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)
    0
    PDF Downloads
    0
    Metadata Views

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.

Cite As Get 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

Author Details

Nathan Liittschwager
  • University of California, Santa Cruz, CA, USA
Stelios Tsampas
  • Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany
Jonathan Castello
  • University of California, Santa Cruz, CA, USA
Lindsey Kuper
  • University of California, Santa Cruz, CA, USA

Funding

This material is based upon work supported by the National Science Foundation under Grant No. CCF-2145367. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation.

References

  1. 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.
  2. 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. Google Scholar
  3. 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.
  4. 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.
  5. 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.
  6. 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.
  7. 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.
  8. Friedemann Mattern. Virtual time and global states of distributed systems. In Parallel and Distributed Algorithms, pages 215-226. North-Holland, 1989. Google Scholar
  9. 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. Google Scholar
  10. 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.
  11. 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.
  12. 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.
  13. 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.
  14. 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. 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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact