Conflict-free Replicated Data Types

Replicating data under Eventual Consistency (EC) allows any replica to accept updates without remote synchronisation. This ensures performance and scalability in large-scale distributed systems (e.g., clouds). However, published EC approaches are ad-hoc and error-prone. Under a formal Strong Eventual Consistency (SEC) model, we study sufficient conditions for convergence. A data type that satisfies these conditions is called a Conflict-free Replicated Data Type (CRDT). Replicas of any CRDT are guaranteed to converge in a self-stabilising manner, despite any number of failures. This paper formalises two popular approaches (state- and operation-based) and their relevant sufficient conditions. We study a number of useful CRDTs, such as sets with clean semantics, supporting both add and remove operations, and consider in depth the more complex Graph data type. CRDT types can be composed to develop large-scale distributed applications, and have interesting theoretical properties.La réplication selon la politique de cohérence à terme (Eventual Consistency ou EC) autorise toute réplique à accepter des mises à jour sans se synchroniser avec les autres. Cette approche ne bride pas les performances et permet le passage à l'échelle dans les systèmes distribués, par ex. dans l'informatique en nuage. Cependant, les algorithmes EC précédemment publiés sont ad-hoc et sujets aux erreurs. Nous proposons un modèle formel, la cohérence à terme forte (Strong Eventual Consistency ou SEC), dans lequel nous étudions des conditions suffisantes de converegence. Un type de données satisfaisant ces conditions sera dit sans conflit (Conflict-free Replicated Data Type ou CRDT). Les répliques d'un CRDT convergent de façon auto-stabilisante, quel que soit le nombre de fautes. Cet article formalise deux approches courantes, celle basée sur les états et celle basée sur les données, et les conditions suffisantes correspondantes. Nous étudions un certain nombre de CRDT génériques, comme des ensembles, avec une sémantique appropriée pour les opérations add et remove, et approfondissons un type plus complexe, le graphe. Les CRDT peuvent être composés, de façon à développer des applications réparties à grande échelle, et ont des propriétés théoriques intéressantes