Inferring Formal Properties of Production Key-Value Stores

TL;DR

This paper develops formal models for key-value store protocols like Riak and Cassandra, verifying their correctness and eventual consistency through novel certified program models in C.

Contribution

It introduces a new approach of modeling distributed protocols as certified C programs, enabling rigorous verification of properties like eventual consistency.

Findings

Models for read-repair and hinted-handoff protocols verified.

Protocols guarantee eventual consistency under specified failure assumptions.

Conformance tested against real production systems.

Abstract

Production distributed systems are challenging to formally verify, in particular when they are based on distributed protocols that are not rigorously described or fully understood. In this paper, we derive models and properties for two core distributed protocols used in eventually consistent production key-value stores such as Riak and Cassandra. We propose a novel modeling called certified program models, where complete distributed systems are captured as programs written in traditional systems languages such as concurrent C. Specifically, we model the read-repair and hinted-handoff recovery protocols as concurrent C programs, test them for conformance with real systems, and then verify that they guarantee eventual consistency, modeling precisely the specification as well as the failure assumptions under which the results hold.