From high level specification to executable code: Specification, refinement, and implementation of a survivable and consistent data service for dynamic networks

Providing middleware services that implement atomic shared memory for applications deployed in dynamic distributed systems where processing nodes may fail or become disconnected is challenging. The key difficulty in this setting is to guarantee linearizability while maintaining overall system efficiency. A general framework called RAMBO (Reconfigurable Atomic Memory for Basic Objects), developed by Lynch and Shvartsman, can be used to implement such a service in systems where nodes may join, fail, become delayed, and become periodically or permanently disconnected from the network. In this thesis we introduce four new algorithms that build on RAMBO and that are designed to provide efficient and versatile implementations of an atomic memory service suited for many deployment settings, for example, ad hoc and mobile, and peer-to-peer networks. ^ RAMBO utilizes replication to ensure survivability, where the object is replicated at a number of networked nodes. Atomicity is ensured via the use of quorum systems, where quorum members are the replica owners. Since failures may result in a quorum system becoming disabled, RAMBO provides reconfiguration by which new quorum systems are installed and old quorum systems removed. Novelty of RAMBO is its graceful reconfiguration mechanism that allows replacement of old quorum systems with new ones without aborting or blocking ongoing read and write operations. The original RAMBO algorithms target simplicity of design, generality of solution, and fault tolerance, however make no attempt to optimize communication efficiency. Implementations derived directly from the original algorithms, while correct, may lead to high or even unbounded operation latency, and very high communication overhead. ^ In this thesis we introduce algorithms that implement the RAMBO service, which are communication-efficient and ensure operation progress in sparsely-connected or limited-bandwidth networks under reasonable timing assumptions on message delivery. Specifically, we successively refine with additional levels of detail, the RAMBO framework where each resulting algorithm is formally proved correct to preserve safety guarantees of the source specification, provide analytical performance study of each refinement in order to quantify the potential performance improvements, provide physical implementation of each algorithm in an experimental distributed setting, and collect experimental results to support the theoretical performance expectations. ^ Implementation of RAMBO algorithm into executable code can be viewed as the final refinement. It is important to be convinced that the implemented system has the same characteristics as its source specification, hence ensuring that the executable code is correct. Therefore, the implementation process must be guided by a formal translation methodology that can be verified to preserve safety guarantees of the source specification. We prototyped and used a framework for a manual translation of RAMBO into to executable Java code. We formally prove correct one part of our framework and leave the remaining parts as future research.