Search

International audience; A conflict-free replicated data type (CRDT) is an abstract data type, with a well defined interface, designed to be replicated at multiple processes and exhibiting the following properties: (1) any replica can be modified without coordinating with another replicas; (2) when any two replicas have received the same set of updates, they reach the same state, deterministically, by adopting mathematically sound rules to guarantee state convergence.

International audience; Edge applications, such as gaming, cooperative engineering, or in-the-field information sharing, enjoy immediate response, autonomy and availability by distributing and replicating data at the edge. However, application developers and users demand the highest possible consistency guarantees, and specific support for group collaboration. To address this challenge, Colony guarantees Transactional Causal Plus Consistency (TCC+) globally, strengthened to Snapshot Isolation within edge groups. To help with scalability, fault tolerance and security, its logical communication topology is forest-like, with replicated roots in the core cloud, but with the flexibility to migrate a node or a group. Despite this hybrid approach, applications enjoy the same semantics everywhere in the topology. Our experiments show that local caching and peer groups improve throughput and response time significantly, performance is not affected in offline mode, and that migration is seamless.

The tree is an essential data structure in many applications. In a distributed application, such as a distributed file system, the tree is replicated.To improve performance and availability, different clients should be able to update their replicas concurrently and without coordination. Such concurrent updates converge if the effects commute, but nonetheless, concurrent moves can lead to incorrect states and even data loss. Such a severe issue cannot be ignored; ultimately, only one of the conflicting moves may be allowed to take effect. However, as it is rare, a solution should be lightweight. Previous approaches would require preventative cross-replica coordination, or totally order move operations after-the-fact, requiring roll-back and compensation operations. In this paper, we present a novel replicated tree that supports coordination-free concurrent atomic moves, and provably maintains the tree invariant. Our analysis identifies cases where concurrent moves are inherently safe, and we devise a lightweight, coordination-free, rollback-free algorithm for the remaining cases, such that a maximal safe subset of moves takes effect. We present a detailed analysis of the concurrency issues with trees, justifying our replicated tree data structure. We provide mechanized proof that the data structure is convergent and maintains the tree invariant. Finally, we compare the response time and availability of our design against the literature.; L’arbre est une structure de données essentielle. Quand l’application est distribuée, par exemple dans un système de fichiers distribué, l’arbre est répliqué. Pour améliorer les performances et la disponibilité, les différents clients doivent pouvoir mettre à jour leurs répliques simultanément et sans coordination. Celles-ci convergent si les mises à jour commutent entre elles ; néanmoins, même dans ce cas, des opérations “move” concurrentes peuvent conduire à des états incorrects, et même à la perte de données. Au bout du compte, entre deux opérations “move” en conflit, seule l’une des deux peut être autorisée à prendre effet. Cependant, comme ce cas est rare, la solution doit être légère. Les approches précédentes nécessitaient une coordination préventive des répliques, ou des retours en arrière a posteriori. Dans cet article, nous présentons un nouvel arbre répliqué, qui met en œuvre une opération “move” atomique sans coordination, et dont nous prouvons qu’il maintient l’invariant d’arbre.Notre analyse identifie les cas où les “move” concurrents sont intrinsèquement sûrs, et proposons un algorithme léger, sans coordination et sans retour-arrière, pour les autres cas, de sorte qu’un sous-ensemble maximal et sûr de “move” prenne effet. Nous présentons une analyse détaillée des problèmes de cohérence dans les arbres. Nous fournissons une preuve mécanisée que la structure des données est convergente et maintientl’invariant d’arbre. Enfin, nous comparons le temps de réponse et la disponibilité de notre concept à la littérature.

The tree is an essential data structure in many applications. In a distributed application, such as a distributed file system, the tree is replicated.To improve performance and availability, different clients should be able to update their replicas concurrently and without coordination. Such concurrent updates converge if the effects commute, but nonetheless, concurrent moves can lead to incorrect states and even data loss. Such a severe issue cannot be ignored; ultimately, only one of the conflicting moves may be allowed to take effect. However, as it is rare, a solution should be lightweight. Previous approaches would require preventative cross-replica coordination, or totally order move operations after-the-fact, requiring roll-back and compensation operations. In this paper, we present a novel replicated tree that supports coordination-free concurrent atomic moves, and provably maintains the tree invariant. Our analysis identifies cases where concurrent moves are inherently safe, and we devise a lightweight, coordination-free, rollback-free algorithm for the remaining cases, such that a maximal safe subset of moves takes effect. We present a detailed analysis of the concurrency issues with trees, justifying our replicated tree data structure. We provide mechanized proof that the data structure is convergent and maintains the tree invariant. Finally, we compare the response time and availability of our design against the literature.; L’arbre est une structure de données essentielle. Quand l’application est distribuée, par exemple dans un système de fichiers distribué, l’arbre est répliqué. Pour améliorer les performances et la disponibilité, les différents clients doivent pouvoir mettre à jour leurs répliques simultanément et sans coordination. Celles-ci convergent si les mises à jour commutent entre elles ; néanmoins, même dans ce cas, des opérations “move” concurrentes peuvent conduire à des états incorrects, et même à la perte de données. Au bout du compte, entre deux opérations “move” en conflit, seule l’une des deux peut être autorisée à prendre effet. Cependant, comme ce cas est rare, la solution doit être légère. Les approches précédentes nécessitaient une coordination préventive des répliques, ou des retours en arrière a posteriori. Dans cet article, nous présentons un nouvel arbre répliqué, qui met en œuvre une opération “move” atomique sans coordination, et dont nous prouvons qu’il maintient l’invariant d’arbre.Notre analyse identifie les cas où les “move” concurrents sont intrinsèquement sûrs, et proposons un algorithme léger, sans coordination et sans retour-arrière, pour les autres cas, de sorte qu’un sous-ensemble maximal et sûr de “move” prenne effet. Nous présentons une analyse détaillée des problèmes de cohérence dans les arbres. Nous fournissons une preuve mécanisée que la structure des données est convergente et maintientl’invariant d’arbre. Enfin, nous comparons le temps de réponse et la disponibilité de notre concept à la littérature.

The tree is an essential data structure in many applications. In a distributed application, such as a distributed file system, the tree is replicated.To improve performance and availability, different clients should be able to update their replicas concurrently and without coordination. Such concurrent updates converge if the effects commute, but nonetheless, concurrent moves can lead to incorrect states and even data loss. Such a severe issue cannot be ignored; ultimately, only one of the conflicting moves may be allowed to take effect. However, as it is rare, a solution should be lightweight. Previous approaches would require preventative cross-replica coordination, or totally order move operations after-the-fact, requiring roll-back and compensation operations. In this paper, we present a novel replicated tree that supports coordination-free concurrent atomic moves, and provably maintains the tree invariant. Our analysis identifies cases where concurrent moves are inherently safe, and we devise a lightweight, coordination-free, rollback-free algorithm for the remaining cases, such that a maximal safe subset of moves takes effect. We present a detailed analysis of the concurrency issues with trees, justifying our replicated tree data structure. We provide mechanized proof that the data structure is convergent and maintains the tree invariant. Finally, we compare the response time and availability of our design against the literature.; L’arbre est une structure de données essentielle. Quand l’application est distribuée, par exemple dans un système de fichiers distribué, l’arbre est répliqué. Pour améliorer les performances et la disponibilité, les différents clients doivent pouvoir mettre à jour leurs répliques simultanément et sans coordination. Celles-ci convergent si les mises à jour commutent entre elles ; néanmoins, même dans ce cas, des opérations “move” concurrentes peuvent conduire à des états incorrects, et même à la perte de données. Au bout du compte, entre deux opérations “move” en conflit, seule l’une des deux peut être autorisée à prendre effet. Cependant, comme ce cas est rare, la solution doit être légère. Les approches précédentes nécessitaient une coordination préventive des répliques, ou des retours en arrière a posteriori. Dans cet article, nous présentons un nouvel arbre répliqué, qui met en œuvre une opération “move” atomique sans coordination, et dont nous prouvons qu’il maintient l’invariant d’arbre.Notre analyse identifie les cas où les “move” concurrents sont intrinsèquement sûrs, et proposons un algorithme léger, sans coordination et sans retour-arrière, pour les autres cas, de sorte qu’un sous-ensemble maximal et sûr de “move” prenne effet. Nous présentons une analyse détaillée des problèmes de cohérence dans les arbres. Nous fournissons une preuve mécanisée que la structure des données est convergente et maintientl’invariant d’arbre. Enfin, nous comparons le temps de réponse et la disponibilité de notre concept à la littérature.

To provide high availability in distributed systems, object replicas allow concurrent updates. Although replicas eventually converge, they may diverge temporarily, for instance when the network fails. This makes it difficult for the developer to reason about the object's properties , and in particular, to prove invariants over its state. For the sub-class of state-based distributed systems, we propose a proof methodology for establishing that a given object maintains a given invariant, taking into account any concurrency control. Our approach allows reasoning about individual operations separately. We demonstrate that our rules are sound, and we illustrate their use with some representative examples. We automate the rule using Boogie, an SMT-based tool.

We study a proof methodology for verifying the safety of data invariants of highly-available distributed applications that replicate state. The proof is (1) modular: one can reason about each individual operation separately, and (2) sequential: one can reason about a distributed application as if it were sequential. We automate the methodology and illustrate the use of the tool with a representative example., Comment: Workshop on Principles and Practice of Consistency for Distributed Data (PaPoC), Mar 2019, Dresden, Germany. https://novasys.di.fct.unl.pt/conferences/papoc19/

International audience; A data store allows application processes to put and get data from a shared memory. In general, a data store cannot be modelled as a strictly sequential process. Applications observe non-sequential behaviours, called anomalies. The set of possible behaviours, and conversely of possible anomalies, constitutes the consistency model of the data store.

International audience; This paper studies the costs and trade-offs of providing transactional consistent reads in a distributed storage system. We identify the following dimensions: read consistency, read delay (latency), and data freshness. We show that there is a three-way trade-off between them, which can be summarised as follows: (i) it is not possible to ensure at the same time order-preserving (e.g., causally-consistent) or atomic reads, Minimal Delay, and maximal freshness; thus, reading data that is the most fresh without delay is possible only in a weakly-isolated mode; (ii) to ensure atomic or order-preserving reads at Minimal Delay imposes to read data from the past (not fresh); (iii) however, order-preserving minimal-delay reads can be fresher than atomic; (iv) reading atomic or order-preserving data at maximal freshness may block reads or writes indefinitely. Our impossibility results hold independently of other features of the database, such as update semantics (totally ordered or not) or data model (structured or unstructured). Guided by these results, we modify an existing protocol to ensure minimal-delay reads (at the cost of freshness) under atomic-visibility and causally-consistent semantics. Our experimental evaluation supports the theoretical results.

Preserving invariants while designing distributed applications under weak consistency models is difficult. The CEC (Correct Eventual Consistency Tool) is meant to aid the application designer in this task. It provides information about the errors during concurrent operations and suggestions on how and where to synchronize operations. This report presents two features of the tool: providing a counterexample for debugging and concurrency control suggestions.

International audience; For decades distributed computing has been mainly an academic subject. Today, it has become mainstream: our connected world demands applications that are inherently distributed, and the usage of shared, distributed, peer-to-peer or cloud-computing infrastructures are increasingly common. However, writing distributed applications that are both correct and well distributed (e.g., highly available) is extremely challenging. In fact, there exists a fundamental trade-off between data consistency, availability, and the ability to tolerate failures. This trade-off has implications on the design of the entire distributed computing infrastructure, including storage systems, compilers and runtimes, application development frameworks and programming languages. Unfortunately, this also has significant implications on the programming model exposed to the designers and developers of applications. We need to enable programmers who are not experts in these subtle aspects to build distributed applications that remain correct in the presence of concurrency, failures, churn, replication, dynamically-changing and partial information, high load, absence of a single line of time, etc. This Dagstuhl Seminar proposes to bring together researchers and practitioners in the areas of distributed systems, programming languages, verifications, and databases. We would like to understand the lessons learnt in building scalable and correct distributed systems, the design patterns that have emerged, and explore opportunities for distilling these into programming methodologies, programming tools, and languages to make distributed computing easier and more accessible. Main issues in discussion: Application writers are constantly making trade-offs between consistency and availability. What kinds of tools and methodologies can we provide to simplify this decision making? How does one understand the implications of a design choice? Available systems are hard to design, test and debug. Do existing testing and debugging tools suffice for identifying and isolating bugs due to weak consistency? How can these problems be identified in production using live monitoring? Can we formalize commonly desired (generic) correctness (or performance) properties? How can we teach programmers about these formalisms and make them accessible to a wide audience? Can we build verification or testing tools to check that systems have these desired correctness properties? How do applications achieve the required properties, while ensuring adequate performance, in practice? What design patterns and idioms work well? To what degree can these properties be guaranteed by the platform (programming language, libraries, and runtime system)? What are the responsibilities of the application developer, and what tools and information does she have?

International audience; Referential integrity (RI) is an important correctness property of a shared, distributed object storage system. It is sometimes thought that enforcing RI requires a strong form of consistency. In this paper, we argue that causal consistency suffices to maintain RI. We support this argument with pseudocode for a reference CRDT data type that maintains RI under causal consistency. QuickCheck has not found any errors in the model.

International audience; Most distributed storage systems provide limited abilities for querying data by attributes other than their primary keys. Supporting efficient search on secondary attributes is challenging as applications pose varying requirements to query processing systems, and no single system design can be suitable for all needs. In this paper, we show how to overcome these challenges in order to extend distributed data stores to support queries on secondary attributes. We propose a modular architecture that is flexible and allows query processing systems to make trade-offs according to different use case requirements. We describe adap-tive mechanisms that make use of this flexibility to enable query processing systems to dynamically adjust to query and write operation workloads.

By the CAP Theorem, a distributed data storage system can ensure either Consistency under Partition (CP) or Availability under Partition (AP), but not both. This has led to a split between CP databases, in which updates are synchronous, and AP databases, where they are asynchronous. However, there is no inherent reason to treat all updates identically: simply, the system should be as available as possible, and synchronised just enough for the application to be correct. We offer a principled \emph{Just-Right Consistency} approach to designing such applications, reconciling correctness with availability and performance, based on the following insights:(i) The Conflict-Free Replicated Data Type (CRDTs) data model supports asynchronous updates in an intuitive and principled way.(ii) Invariants involving joint or mutually-ordered updates are compatible with AP and can be guaranteed by Transactional Causal Consistency, the strongest consistency model that does not compromise availability. Regarding the remaining, ``CAP-sensitive'' invariants:(iii) For the common pattern of Bounded Counters, we provide encapsulated data type that is proven correct and is efficient; (iv) in the general case, static analysis can identify when synchronisation is not necessary for correctness.Our Antidote cloud database system supports CRDTs, Transactional Causal Consistency and the Bounded Counter data type. Support tools help design applications by static analysis and proof of CAP-sensitive invariants. This system supports industrial-grade applications and has been tested experimentally with hundreds of servers across several geo-distributed data centres.; Le théorème CAP, un système de stockage réparti peut être, en cas de partition, soit cohérent (CP), soit disponible (AP), mais pas les deux. Il y a donc des bases de données CP, où les mises à jour sont synchrones, et les bases AP, où elles sont asynchrones. Cependant, il n'y a pas de raison essentielle de traiter toutes les mises à jour de façon identique. L'objectif est que le système reste aussi disponible que possible, mais suffisamment synchronisé pour que l'application reste correcte. Nous proposons un nouveau principe, la juste cohérence, afin de concevoir de telles applications, réconciliant la sûreté avec la disponibilité et l'efficacité, à partir des constatations suivantes : (i) Le modèle de données des CRDT (Conict-Free Replicated Data Type) permet les mises à jour concurrentes de façon à la fois théoriquement fondée et intuitive. (ii) Les invariants basés sur la simultanéité ou l'ordre partiel des mises à jour sont compatibles avec AP, et peuvent être garanties par la Cohérence Causale Transactionelle (TCC), le modèle de cohérence le plus fort qui ne compromet pas la disponibilité.En ce qui concerne les autres invariants, dits CAP-sensibles : (iii) Le cas courant du compteur borné peut être géré par un type de données encapsulé, correct et cohérent, appelé Bounded Counter ; et (iv) dans le cas général, une analyse statique permet d'indentifier les cas où la sûreté ne nécessite pas de synchronisation. Notre base de données \nuage" Antidote offre les CRDT, le modèle TCC, et le type de données Bounded Counter. Des outils d'analyse statique et de preuve des invariants CAP-sensibles aident à la conception des applications. Notre système est mûrpour des applications d'échelle industrielle, et à été testé expérimentallement sur des centaines de serveurs répartis entre plusieurs centres de données géo-distribués.

Preserving invariants while designing distributed applications under weak consistency models is difficult. The CEC (Correct Eventual Consistency Tool) is meant to aid the application designer in this task. This report presents some specifications tried out using the tool and some recommendations for its improvement based on the usage experience.; Le maintien des invariants, dans les applications réparties s'exécutantdans un modèle de cohérence faible, est un problème difficile.L'outil CEC (Correct Eventual Consistency) est destiné à aider ledéveloppeur d'application dans cette tâche.Notre rapport présente plusieurs exemples de spécifications vérifiées enutilisant cet outil, ainsi que quelques recommandations sur son usage,basées sur notre expérience d'utilisation.

Preserving invariants while designing distributed applications under weak consistency models is difficult. The CEC (Correct Eventual Consistency Tool) is meant to aid the application designer in this task. This report presents some specifications tried out using the tool and some recommendations for its improvement based on the usage experience.; Le maintien des invariants, dans les applications réparties s'exécutantdans un modèle de cohérence faible, est un problème difficile.L'outil CEC (Correct Eventual Consistency) est destiné à aider ledéveloppeur d'application dans cette tâche.Notre rapport présente plusieurs exemples de spécifications vérifiées enutilisant cet outil, ainsi que quelques recommandations sur son usage,basées sur notre expérience d'utilisation.