Much ADO about failures: a fault-aware model for compositional verification of strongly consistent distributed systems

Despite recent advances, guaranteeing the correctness of large-scale distributed applications without compromising performance remains a challenging problem. Network and node failures are inevitable and, for some applications, careful control over how they are handled is essential. Unfortunately, existing approaches either completely hide these failures behind an atomic state machine replication (SMR) interface, or expose all of the network-level details, sacrificing atomicity. We propose a novel, compositional, atomic distributed object (ADO) model for strongly consistent distributed systems that combines the best of both options. The object-oriented API abstracts over protocol-specific details and decouples high-level correctness reasoning from implementation choices. At the same time, it intentionally exposes an abstract view of certain key distributed failure cases, thus allowing for more fine-grained control over them than SMR-like models. We demonstrate that proving properties even of composite distributed systems can be straightforward with our Coq verification framework, Advert, thanks to the ADO model. We also show that a variety of common protocols including multi-Paxos and Chain Replication refine the ADO semantics, which allows one to freely choose among them for an application's implementation without modifying ADO-level correctness proofs.

Consensus in anonymous asynchronous systems with crash-recovery and omission failures

In anonymous distributed systems, processes are indistinguishable because they have no identity and execute the same algorithm. Currently, anonymous systems are receiving a lot of attention mainly because they preserve privacy, which is an important property when we want to avoid impersonation attacks. On the other hand, Consensus is a fundamental problem in distributed computing. It is well-known that Consensus cannot be deterministically solved in pure asynchronous anonymous systems if processes can crash (the so-called crash-stop failure model). This impossibility holds even if message losses never occur in transmission. Failure detectors are an elegant and powerful abstraction for achieving deterministic Consensus in asynchronous distributed systems. A failure detector is a distributed object that gives the processes information about crashed processes. Failure detectors have attracted so much attention in the crash-stop failure model because they provide a totally independent abstraction. $$\varOmega $$ Ω is the weakest failure detector to solve Consensus in classic asynchronous systems when a majority of processes never crash, and $$A\varOmega '$$ A Ω ′ is its implementable version for anonymous systems. As far as we know, there is a lack of works in the literature which tackle Consensus in anonymous asynchronous systems where crashed process can recover (the so-called crash-recovery failure model) and also assuming errors in transmission operations (the so-called omission failure model). Extending failure models in the system allows us to design more realistic systems and solve more practical security problems (i.e., fair exchange and the secure multiparty computation). We present, in this paper, an algorithm to solve Consensus using $$A\varOmega '$$ A Ω ′ in anonymous asynchronous systems under the crash-recovery and omission failure models. Another important contribution of this paper is a communication-efficient and latency-efficient implementation of $$A\varOmega '$$ A Ω ′ for these new failure models.

Comparing of Soap and Distributed Object Technologies: A Case Study

Web service technology has emerged as a popular way for building distributed applications involving distributed databases. It is the next generation technology in the long journey from functions to objects to components to services. Today’s comparing SOAP as a wire protocol to the commonly used distributed object technologies and their wire protocols in use. SOAP makes use of openly available technologies that, when combined, specify a wire protocol. This protocol can be used to facilitate highly and ultra-distributed architecture. SOAP commonly uses the HTTP protocol to transport XML-encoded serialized method argument data from system to system. This serialized argument data is used on the remote end to execute the client’s method call on that system, rather than the client’s local system. This case study provides a more details comparison of the SOAP and Distributed objects.