arXiv subjects

Annette Bieniusa

Publications and source records attributed to Annette Bieniusa.

23 records · Page 2Linked to original sources

arXiv2017

EPTL - A temporal logic for weakly consistent systems

The high availability and scalability of weakly-consistent systems attracts system designers. Yet, writing correct application code for this type of systems is difficult; even how to specify the intended behavior of such systems is still an open question. There has not been established any standard method to specify the intended dynamic behavior of a weakly consistent system. There exist specifications of various consistency models for distributed and concurrent systems; and the semantics of replicated datatypes like CRDTs have been specified in axiomatic and operational models based on visibility relations. In this paper, we present a temporal logic, EPTL, that is tailored to specify properties of weakly consistent systems. In contrast to LTL and CTL, EPTL takes into account that operations of weakly consistent systems are in many cases not serializable and have to be treated respectively to capture the behavior. We embed our temporal logic in Isabelle/HOL and can thereby leverage strong semi-automatic proving capabilities.

cs.LO↗

arXiv2016

Decoupling conflicts for configurable resolution in an open replication system

Replikativ is a replication middleware supporting a new kind of confluent replicated datatype resembling a distributed version control system. It retains the order of write operations at the trade-off of reduced availability with after-the- fact conflict resolution. The system allows to develop applications with distributed state in a similar fashion as native applications with exclusive local state, while transparently exposing the necessary compromises in terms of the CAP theorem. In this paper, we give a specification of the replicated datatype and discuss its usage in the replikativ middleware. Experiments with the implementation show the feasibility of the concept as a foundation for replication as a service (RaaS).

cs.DC↗

arXiv2015

Eventually Consistent Register Revisited

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.

cs.DC↗

arXiv2013

SwiftCloud: Fault-Tolerant Geo-Replication Integrated all the Way to the Client Machine

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.

cs.DC↗

arXiv2012

An optimized conflict-free replicated set

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.

cs.DC↗