Mohsen Lesani: Certified Causally Consistent Distributed Key-Value Stores
Today’s Internet services are often expected to stay available and
render high responsiveness even in the face of site crashes and
network partitions. Theoretical results state that causal consistency
is one of the strongest consistency guarantees that is possible under
these requirements, and many practical systems provide causally
consistent key-value stores. In this paper, we present modular
verification of causal consistency for replicated key-value store
algorithms and their client programs. Specifically, we formulate
separate correctness conditions for key-value store algorithms and
for their clients. The interface between the two is a novel operational
semantics for causal consistency. We have verified the causal
consistency of two key-value store algorithms from the literature
using a novel proof technique. We have also implemented a simple
automatic model checker for the correctness of client programs. The
two independently verified results for the algorithms and clients
can be composed to conclude correctness of any of the programs
when executed with any of the algorithms. We have developed and
checked our framework in Coq, extracted it to OCaml, and built
executable stores.
Abstract:
access objects should execute atomically. Due to the intricacy of
synchronization, encapsulating atomicity in modules can improve both
the programmability and verifiabilty of user programs. Therefore,
mainstream programming languages offer libraries of concurrent data types.
An important question is how composable these concurrent data types are.
They usually guarantee linearizability that supports horizontal composition.
An execution may involve method calls on multiple concurrent objects and
each method call appears to take effect atomically. However, they usually
don't support vertical composition. The execution of multiple method calls
on a concurrent object is not necessarily atomic. I present "ideally"
composable concurrent objects and how synthesis from high-level relational
specifications can directly target them. I present our current effort to
build a verification framework for composable concurrent objects in Coq.