Search

This paper describes ongoing work on developing a formal specification of a database backend. We present the formalisation of the expected behaviour of a basic transactional system that calls into a simple store API, and instantiate in two semantic models. The first one is a map-based, classical versioned key-value store; the second one, journal-based, appends individual transaction effects to a journal. We formalise a significant part of the specification in the Coq proof assistant. This work will form the basis for a formalisation of a full-fledged backend store with features such as caching or write-ahead logging, as variations on maps and journals., Comment: Workshop on Principles and Practice of Consistency for Distributed Data (PaPoC), EuroSys (ACM), Apr 2024, Ath{\`e}nes, Greece

In this paper, we present the Pipeline for Observational Data Processing, Analysis, and Collaboration (PODPAC) software. PODPAC is an open-source Python library designed to enable widespread exploitation of NASA earth science data by enabling multi-scale and multi-windowed access, exploration, and integration of available earth science datasets to support analysis and analytics; automatic accounting for geospatial data formats, projections, and resolutions; simplified implementation and parallelization of geospatial data processing routines; standardized sharing of data and algorithms; and seamless transition of algorithms and data products from local development to distributed, serverless processing on commercial cloud computing environments. We describe the key elements of PODPAC’s architecture, including Nodes for unified encapsulation of disparate scientific data sources; Algorithms for plug-and-play processing and harmonization of multiple data source Nodes; and Lambda functions for serverless execution and sharing of new data products via the cloud. We provide an overview of our open-source code implementation and testing process for development and deployment of PODPAC. We describe our interactive, JupyterLab-based end-user documentation including quick-start examples and detailed use case studies. We conclude with examples of PODPAC’s application to: encapsulate data sources available on Amazon Web Services (AWS) Open Data repository; harmonize processing of multiple earth science data sets for downscaling of NASA Soil Moisture Active Passive (SMAP) soil moisture data; and deploy a serverless SMAP-based drought monitoring application for use access from mobile devices. We postulate that PODPAC will also be an effective tool for wrangling and standardizing massive earth science data sets for use in model training for machine learning applications.

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.

Database systems use query processing subsystems for enabling efficient query-based data retrieval. An essential aspect of designing any query-intensive application is tuning the query system to fit the application's requirements and workload characteristics. However, the configuration parameters provided by traditional database systems do not cover the design decisions and trade-offs that arise from the geo-distribution of users and data. In this paper, we present a vision towards a new type of query system architecture that addresses this challenge by enabling query systems to be designed and deployed in a per use case basis. We propose a distributed abstraction called Query Processing Unit that encapsulates primitive query processing tasks, and show how it can be used as a building block for assembling query systems. Using this approach, application architects can construct query systems specialized to their use cases, by controlling the query system's architecture and the placement of its state. We demonstrate the expressiveness of this approach by applying it to the design of a query system that can flexibly place its state in the data center or at the edge, and show that state placement decisions affect the trade-off between query response time and query result freshness.

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

One of the most powerful an influential men is covered in this new biography comic book. See how his empire started from the beginning.

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

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.

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 pos- sible behaviours, and conversely of possible anomalies, constitutes the consistency model of the data store.

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.

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., Comment: 5th Workshop on Principles and Practice of Consistency for Distributed Data, Apr 2018, Porto, Portugal. 5th Workshop on Principles and Practice of Consistency for Distributed Data April 23--26, 2018, Porto, Portugal, 2018

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.

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 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.

The advent of non-volatile memory (NVM) technologies like PCM, STT, memristors and Fe-RAM is believed to enhance the system performance by getting rid of the traditional memory hierarchy by reducing the gap between memory and storage. This memory technology is considered to have the performance like that of DRAM and persistence like that of disks. Thus, it would also provide significant performance benefits for big data applications by allowing in-memory processing of large data with the lowest latency to persistence. Leveraging the performance benefits of this memory-centric computing technology through traditional memory programming is not trivial and the challenges aggravate for parallel/concurrent applications. To this end, several programming abstractions have been proposed like NVthreads, Mnemosyne and intel's NVML. However, deciding upon a programming abstraction which is easier to program and at the same time ensures the consistency and balances various software and architectural trade-offs is openly debatable and active area of research for NVM community. We study the NVthreads, Mnemosyne and NVML libraries by building a concurrent and persistent set and open addressed hash-table data structure application. In this process, we explore and report various tradeoffs and hidden costs involved in building concurrent applications for persistence in terms of achieving efficiency, consistency and ease of programming with these NVM programming abstractions. Eventually, we evaluate the performance of the set and hash-table data structure applications. We observe that NVML is easiest to program with but is least efficient and Mnemosyne is most performance friendly but involves significant programming efforts to build concurrent and persistent applications., Comment: Accepted in HiPC SRS 2017

Comparisons of different consistency models often try to place them in a linear strong-to-weak order. However this view is clearly inadequate, since it is well known, for instance, that Snapshot Isolation and Serialisability are incomparable. In the interest of a better understanding, we propose a new classification, along three dimensions, related to: a total order of writes, a causal order of reads, and transactional composition of multiple operations. A model may be stronger than another on one dimension and weaker on another. We believe that this new classification scheme is both scientifically sound and has good explicative value. The current paper presents the three-dimensional design space intuitively.

One of the most powerful an influential men is covered in this new biography comic book. See how his empire started from the beginning.

Kim Kardashian's love life has been part and parcel of her rise to the throne of pop culture icon. She definitely knows how to pick men and it is the many loves of Kim Kardashian that StormFront Comics will explore in "15 Minutes: Kim Kardashian," coming in September. This chronicle of sex tape diva turned world celebrity brand is written by New York Times Bestselling Author Marc Shapiro and illustrated by the mad talent of rising star Noval Hernawan.

In order to converge in the presence of concurrent updates, modern eventually consistent replication systems rely on causality information and operation semantics. It is relatively easy to use semantics of high-level operations on replicated data structures, such as sets, lists, etc. However, it is difficult to exploit semantics of operations on registers, which store opaque data. In existing register designs, concurrent writes are resolved either by the application, or by arbitrating them according to their timestamps. The former is complex and may require user intervention, whereas the latter causes arbitrary updates to be lost. In this work, we identify a register construction that generalizes existing ones by combining runtime causality ordering, to identify concurrent writes, with static data semantics, to resolve them. We propose a simple conflict resolution template based on an application-predefined order on the domain of values. It eliminates or reduces the number of conflicts that need to be resolved by the user or by an explicit application logic. We illustrate some variants of our approach with use cases, and how it generalizes existing designs., Comment: 8 pages

Geo-replicated databases often operate under the principle of eventual consistency to offer high-availability with low latency on a simple key/value store abstraction. Recently, some have adopted commutative data types to provide seamless reconciliation for special purpose data types, such as counters. Despite this, the inability to enforce numeric invariants across all replicas still remains a key shortcoming of relying on the limited guarantees of eventual consistency storage. We present a new replicated data type, called bounded counter, which adds support for numeric invariants to eventually consistent geo-replicated databases. We describe how this can be implemented on top of existing cloud stores without modifying them, using Riak as an example. Our approach adapts ideas from escrow transactions to devise a solution that is decentralized, fault-tolerant and fast. Our evaluation shows much lower latency and better scalability than the traditional approach of using strong consistency to enforce numeric invariants, thus alleviating the tension between consistency and availability.

This report documents the program and the outcomes of Dagstuhl Seminar 13081 "Consistency in Distributed Systems."

Client-side logic and storage are increasingly used in web and mobile applications to improve response time and availability. Current approaches tend to be ad-hoc and poorly integrated with the server-side logic. We present a principled approach to integrate client- and server-side storage. We support mergeable and strongly consistent transactions that target either client or server replicas and provide access to causally-consistent snapshots efficiently. In the presence of infrastructure faults, a client-assisted failover solution allows client execution to resume immediately and seamlessly access consistent snapshots without waiting. We implement this approach in SwiftCloud, the first transactional system to bring geo-replication all the way to the client machine. Example applications show that our programming model is useful across a range of application areas. Our experimental evaluation shows that SwiftCloud provides better fault tolerance and at the same time can improve both latency and throughput by up to an order of magnitude, compared to classical geo-replication techniques.

Many distributed applications require transactions. However, transactional protocols that require strong synchronization are costly in large scale environments. Two properties help with scalability of a transactional system: genuine partial replication (GPR), which leverages the intrinsic parallelism of a workload, and snapshot isolation (SI), which decreases the need for synchronization. We show that, under standard assumptions (data store accesses are not known in advance, and transactions may access arbitrary objects in the data store), it is impossible to have both SI and GPR. To circumvent this impossibility, we propose a weaker consistency criterion, called Non-monotonic Snapshot Isolation (NMSI). NMSI retains the most important properties of SI, i.e., read-only transactions always commit, and two write-conflicting updates do not both commit. We present a GPR protocol that ensures NMSI, and has lower message cost (i.e., it contacts fewer replicas and/or commits faster) than previous approaches.

From July 8-13, 2012, the Dagstuhl Seminar "Security and Dependability for Federated Cloud Platforms" was held in Schloss Dagstuhl -- Leibniz Center for Informatics. During this seminar, participants presented their current research and discussed open problems in the fields of security and dependability of infrastructure clouds and their federation. The executive summary and abstracts of the talks given during the seminar are put together in this paper.

Eventual consistency of replicated data supports concurrent updates, reduces latency and improves fault tolerance, but forgoes strong consistency. Accordingly, several cloud computing platforms implement eventually-consistent data types. The set is a widespread and useful abstraction, and many replicated set designs have been proposed. We present a reasoning abstraction, permutation equivalence, that systematizes the characterization of the expected concurrency semantics of concurrent types. Under this framework we present one of the existing conflict-free replicated data types, Observed-Remove Set. Furthermore, in order to decrease the size of meta-data, we propose a new optimization to avoid tombstones. This approach that can be transposed to other data types, such as maps, graphs or sequences., Comment: No. RR-8083 (2012)

Replikation kann helfen, in einem verteilten System die Fehlertoleranz und Datensicherheit zu verbessern. In Systemen, die über Weitverkehrsnetze kommunizieren oder mobile Endgeräte einschließen, muß das Replikationssystem mit großen Kommunikationslatenzen umgehen können. Deshalb werden in solchen Systemen in der Regel nur asynchrone Replikationsalgorithmen mit schwach-konsistenter Änderungssemantik eingesetzt, da diese die lokale Annahme von Änderungen der Daten und deren Koordinierung mit anderen Replikaten entkoppeln und somit ein schnelles Antwortverhalten bieten können. Diese Dissertation stellt einen Ansatz für die Entwicklung schwach-konsistenter Replikationssysteme mit erweiterten kausalen Konsistenzgarantien vor und weist nach, daß auf seiner Grundlage effiziente Replikationssysteme konstruiert werden können. Dazu werden Mechanismen, Algorithmen und Protokolle vorgestellt, die Änderungen an replizierten Daten aufzeichnen und verteilen und dabei Kausalitätsbeziehungen erhalten. Kern ist ein Änderungsprotokoll, das sowohl als grundlegende Datenstruktur der verteilten Algorithmen agiert, als auch für die Konsistenz der lokalen Daten nach Systemabstürzen sorgt. Die kausalen Garantien werden mit Hilfe von zwei Algorithmen erweitet, die gleichzeitige Änderungen konsistent handhaben. Beide Algorithmen basieren auf der Beobachtung, daß die Divergenz der Replikate durch unkoordinierte, gleichzeitige Änderungen nicht unbedingt als Inkonsistenz gesehen werden muß, sondern auch als das Erzeugen verschiedener Versionen der Daten modelliert werden kann. Distributed Consistent Branching (DCB) erzeugt diese alternativen Versionen der Daten konsistent auf allen Replikaten; Distributed Consistent Cutting (DCC) wählt eine der Versionen konsistent aus. Die vorgestellten Algorithmen und Protokolle wurden in einer Datenbankimplementierung validiert. Mehrere Experimente zeigen ihre Einsetzbarkeit und helfen, ihr Verhalten unter verschiedenen Bedingungen einzuschätzen., Data replication techniques introduce redundancy into a distributed system architecture that can help solve several of its persistent problems. In wide area or mobile systems, a replication system must be able to deal with the presence of unreliable, high-latency links. Only asynchronous replication algorithms with weak-consistency guarantees can be deployed in these environments, as these algorithms decouple the local acceptance of changes to the replicated data from coordination with remote replicas. This dissertation proposes a framework for building weak-consistency replication systems that provides the application developer with causal consistency guarantees and mechanisms for handling concurrency. By presenting an integrated set of mechanisms, algorithms and protocols for capturing and disseminating changes to the replicated data, we show that causal consistency and concurrency handling can be implemented in an efficient and versatile manner. The framework is founded on log of changes, which both acts the core data structure for its distributed algorithms and protocols and serves as the database log that ensures the consistency of the local data replica. The causal consistency guarantees are complemented with two distributed algorithms that handle concurrent operations. Both algorithms are based on the observation that uncoordinated concurrent operations introduce a divergence of state in a replication system that can be modeled as the creation of version branches. Distributed Consistent Branching (DCB) recreates these branches on all participating processes in a consistent manner. Distributed Consistent Cutting (DCC) selects one of the possible branches in a consistent and application-controllable manner and enforces a total causal order for all its operations. The contributed algorithms and protocols were validated in an database system implementation, and several experiments assess the behavior of these algorithms and protocols under varying conditions.

A CRDT is a data type whose operations commute when they are concurrent. Replicas of a CRDT eventually converge without any complex concurrency control. As an existence proof, we exhibit a non-trivial CRDT: a shared edit buffer called Treedoc. We outline the design, implementation and performance of Treedoc. We discuss how the CRDT concept can be generalised, and its limitations.

This post is dedicated to the memory of Rabbi Chaim Flom, late rosh yeshiva of Yeshivat Ohr David in Jerusalem. I first met Rabbi Flom thirty years ago when he became my teacher at the Hebrew Youth Academy of Essex County (now known as the Joseph Kushner Hebrew Academy; unfortunately, another one of my teachers from those years also passed away much too young, Rabbi Yaakov Appel). When he first started teaching he was known as Mr. Flom, because he hadn't yet received semikhah (Actually, he had some sort of semikhah but he told me that he didn't think it was adequate to be called "Rabbi" by the students.) He was only at the school a couple of years and then decided to move to Israel to open his yeshiva. I still remember his first parlor meeting which was held at my house. Rabbi Flom was a very special man. Just to give some idea of this, ten years after leaving the United States he was still in touch with many of the students and even attended our weddings. He would always call me when he came to the U.S. and was genuinely interested to hear about my family and what I was working on. He will be greatly missed.

The Telex system is designed for sharing mutable data in a distributed environment, particularly for collaborative applications. Users operate on their local, persistent replica of shared documents; they can work disconnected and suffer no network latency. The Telex approach to detect and correct conflicts is application independent, based on an action-constraint graph (ACG) that summarises the concurrency semantics of applications. The ACG is stored efficiently in a multilog structure that eliminates contention and is optimised for locality. Telex supports multiple applications and multi-document updates. The Telex system clearly separates system logic (which includes replication, views, undo, security, consistency, conflicts, and commitment) from application logic. An example application is a shared calendar for managing multi-user meetings; the system detects meeting conflicts and resolves them consistently.

We investigate a decentralised approach to committing transactions in a replicated database, under partial replication. Previous protocols either re-execute transactions entirely and/or compute a total order of transactions. In contrast, ours applies update values, and orders only conflicting transactions. It results that transactions execute faster, and distributed databases commit in small committees. Both effects contribute to preserve scalability as the number of databases and transactions increase. Our algorithm ensures serializability, and is live and safe in spite of faults.

Commuting operations greatly simplify consistency in distributed systems. This paper focuses on designing for commutativity, a topic neglected previously. We show that the replicas of \emph{any} data type for which concurrent operations commute converges to a correct value, under some simple and standard assumptions. We also show that such a data type supports transactions with very low cost. We identify a number of approaches and techniques to ensure commutativity. We re-use some existing ideas (non-destructive updates coupled with invariant identification), but propose a much more efficient implementation. Furthermore, we propose a new technique, background consensus. We illustrate these ideas with a shared edit buffer data type.

We study large-scale distributed cooperative systems that use optimistic replication. We represent a system as a graph of actions (operations) connected by edges that reify semantic constraints between actions. Constraint types include conflict, execution order, dependence, and atomicity. The local state is some schedule that conforms to the constraints; because of conflicts, client state is only tentative. For consistency, site schedules should converge; we designed a decentralised, asynchronous commitment protocol. Each client makes a proposal, reflecting its tentative and{\slash}or preferred schedules. Our protocol distributes the proposals, which it decomposes into semantically-meaningful units called candidates, and runs an election between comparable candidates. A candidate wins when it receives a majority or a plurality. The protocol is fully asynchronous: each site executes its tentative schedule independently, and determines locally when a candidate has won an election. The committed schedule is as close as possible to the preferences expressed by clients.

In health care organizations, the division of labor and a need for continuous, 24-hour treatment subjects patients to multiple transitions in care. These transitions, of "handovers" are potential points of failure that have seen very little study. We observed transitions of care in five hospital emergency departments as part of a larger study on safety in emergency care and found that in addition to many other differences in work patterns among the various hospitals, very different sorts of handovers occurred in different contexts, and these differences appeared to reflect a common structure. Using these observations, we have proposed a conceptual framework for characterizing handover events. The ability to characterize certain types of transitions may help to clarify future studies, while assisting in the development of interventions to better fit the context of clinical work.

The prostate cancer incidence and mortality of black Americans is among the highest in the world. The reasons have not been adequately explained. Similar disparities have been noted for men of sub-Saharan origin living in Brazil and the Caribbean. Avenues of investigation have assessed racial and ethnic differences in diet as well as possible differences in the prevalence of genetics (both polymorphisms and mutations). There are studies to suggest that there are no racial differences in outcome when there is equal treatment. Several studies show that there are racial differences in patterns of care in the US and it has been hypothesized that this contributes to some of the racial disparity in survival after diagnosis.