Designing a Planetary-Scale IMAP Service with Conflict-free Replicated Data Types

Authors Tim Jungnickel, Lennart Oldenburg, Matthias Loibl

Thumbnail PDF


  • Filesize: 0.55 MB
  • 17 pages

Document Identifiers

Author Details

Tim Jungnickel
Lennart Oldenburg
Matthias Loibl

Cite AsGet BibTex

Tim Jungnickel, Lennart Oldenburg, and Matthias Loibl. Designing a Planetary-Scale IMAP Service with Conflict-free Replicated Data Types. In 21st International Conference on Principles of Distributed Systems (OPODIS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 95, pp. 23:1-23:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


Modern geo-replicated software serving millions of users across the globe faces the consequences of the CAP dilemma, i.e., the inevitable conflicts that arise when multiple nodes accept writes on shared state. The underlying problem is commonly known as fault-tolerant multi-leader replica- tion; actively researched in the distributed systems and database communities. As a more recent theoretical framework, Conflict-free Replicated Data Types (CRDTs) propose a solution to this problem by offering a set of always converging primitives. However, modeling non-trivial system state with CRDT primitives is a challenging and error-prone task. In this work, we propose a solution for a geo-replicated online service with fault-tolerant multi-leader replication based on CRDTs. We chose IMAP as use case due to its prevalence and simplicity. Therefore, we modeled an IMAP-CRDT and verified its correctness with the interactive theorem prover Isabelle/HOL. In order to bridge the gap between theory and practice, we implemented an open-source proto- type pluto and an IMAP benchmark for write-intensive workloads. We evaluated our prototype against the standard IMAP server Dovecot on a multi-continent public cloud. The results ex- pose the limitations of Dovecot with respect to response time performance and replication lag. Our prototype was able to leverage its conceptual advantages and outperformed Dovecot. We find that our approach is promising when facing the multitude of potential concurrency bugs in development of systems at planetary scale.
  • Geo-Replication
  • CRDT
  • Distributed Systems
  • IMAP
  • Isabelle/HOL


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Mehdi Ahmed-Nacer, Claudia-Lavinia Ignat, Gérald Oster, Hyun-Gul Roh, and Pascal Urso. Evaluating CRDTs for Real-time Document Editing. In ACM Symposium on Document Engineering, DocEng'11, pages 103-112, 2011. Google Scholar
  2. Peter Bailis and Kyle Kingsbury. The Network is Reliable. Commun. ACM, 57(9):48-55, 2014. Google Scholar
  3. Carlos Baquero, Paulo Sérgio Almeida, and Ali Shoker. Making Operation-Based CRDTs Operation-Based. In Distributed Applications and Interoperable Systems, DAIS'14, pages 126-140, 2014. Google Scholar
  4. Eric Brewer. Spanner, TrueTime and the CAP Theorem. Technical report, Google, 2017. Google Scholar
  5. Fay Chang, Jeffrey Dean, Sanjay Ghemawat, et al. Bigtable: A Distributed Storage System for Structured Data. In USENIX Symposium on Operating Systems Design and Implementation, OSDI'06, pages 15-15, 2006. Google Scholar
  6. James C. Corbett, Jeffrey Dean, Michael Epstein, et al. Spanner: Google’s Globally-distributed Database. In USENIX Conference on Operating Systems Design and Implementation, OSDI'12, pages 251-264, 2012. Google Scholar
  7. Mark R. Crispin. INTERNET MESSAGE ACCESS PROTOCOL - VERSION 4rev1. RFC 3501, University of Washington, 2003. URL:
  8. Giuseppe DeCandia, Deniz Hastorun, Madan Jampani, et al. Dynamo: Amazon’s Highly Available Key-value Store. In ACM Symposium on Operating Systems Principles, SOSP'07, pages 205-220, 2007. Google Scholar
  9. C. A. Ellis and S. J. Gibbs. Concurrency Control in Groupware Systems. SIGMOD Rec., 18(2):399-407, 1989. Google Scholar
  10. Colin J. Fidge. Timestamps in Message-Passing Systems That Preserve the Partial Ordering. In Proceedings of the 11th Australian Computer Science Conference. Australian National University. Department of Computer Science, 1987. Google Scholar
  11. Seth Gilbert and Nancy Lynch. Brewer’s Conjecture and the Feasibility of Consistent, Available, Partition-tolerant Web Services. SIGACT News, 33(2):51-59, 2002. Google Scholar
  12. Victor B. F. Gomes, Martin Kleppmann, Dominic P. Mulligan, and Alastair R. Beresford. A framework for establishing Strong Eventual Consistency for Conflict-free Replicated Datatypes. Archive of Formal Proofs, 2017. URL:
  13. 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(109):1-28, 2017. Google Scholar
  14. Tim Jungnickel and Lennart Oldenburg. Pluto: The CRDT-Driven IMAP Server. In International Workshop on Principles and Practice of Consistency for Distributed Data, PaPoC'17, pages 1-5, 2017. Google Scholar
  15. Tim Jungnickel, Lennart Oldenburg, and Matthias Loibl. The IMAP CmRDT. Archive of Formal Proofs, 2017. URL:
  16. M. Kleppmann and A. R. Beresford. A Conflict-Free Replicated JSON Datatype. IEEE Transactions on Parallel and Distributed Systems, 28(10):2733-2746, 2017. Google Scholar
  17. Martin Kleppmann. Designing Data-Intensive Applications: The Big Ideas Behind Reliable, Scalable, and Maintainable Systems. O'Reilly Media, Inc., 2017. Google Scholar
  18. Avinash Lakshman and Prashant Malik. Cassandra: A Decentralized Structured Storage System. SIGOPS Oper. Syst. Rev., 44(2):35-40, 2010. Google Scholar
  19. Frederic Lardinois. Gmail Now Has More Than 1B Monthly Active Users., 2016. [Online; posted February 1, 2016]. URL:
  20. Mihai Letia, Nuno M. Preguiça, and Marc Shapiro. CRDTs: Consistency without concurrency control. Operating Systems Review, 44(2):29-34, 2010. URL:
  21. Friedemann Mattern. Virtual Time and Global States of Distributed Systems. International Workshop on Parallel and Distributed Algorithms, pages 215-226, 1989. Google Scholar
  22. Brice Nédelec, Pascal Molli, Achour Mostefaoui, and Emmanuel Desmontils. LSEQ: an Adaptive Structure for Sequences in Distributed Collaborative Editing. In ACM Symposium on Document Engineering, DocEng'13, pages 37-46, 2013. Google Scholar
  23. Marc Shapiro, Nuno Preguiça, Carlos Baquero, and Marek Zawirski. A comprehensive study of Convergent and Commutative Replicated Data Types. Technical report, Inria, 2011. URL:
  24. Marc Shapiro, Nuno Preguiça, Carlos Baquero, and Marek Zawirski. Conflict-Free Replicated Data Types. In International Symposium on Stabilization, Safety, and Security of Distributed Systems, SSS'11, pages 386-400, 2011. Google Scholar
  25. D. B. Terry, M. M. Theimer, Karin Petersen, A. J. Demers, M. J. Spreitzer, and C. H. Hauser. Managing Update Conflicts in Bayou, a Weakly Connected Replicated Storage System. In ACM Symposium on Operating Systems Principles, SOSP'95, pages 172-182, 1995. Google Scholar
  26. Werner Vogels. Eventually Consistent. Commun. ACM, 52(1):40-44, 2009. Google Scholar
  27. Peter Zeller, Annette Bieniusa, and Arnd Poetzsch-Heffter. Formal Specification and Verification of CRDTs. In Formal Techniques for Distributed Objects, FORTE'14, pages 33-48, 2014. Google Scholar
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail