Inferring Formal Properties of Production Key-Value Stores

Autor:	Pek, Edgar, Garg, Pranav, Rahman, Muntasir Raihan, Palmskog, Karl, Gupta, Indranil, Madhusudan, P.
Rok vydání:	2017
Předmět:	Computer Science - Distributed Parallel and Cluster Computing Computer Science - Logic in Computer Science
Druh dokumentu:	Working Paper
Popis:	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. Comment: 15 pages, 2 figures
Databáze:	arXiv
Externí odkaz:	http://arxiv.org/abs/1712.10056 Zobrazit plný text záznamu View this record from Arxiv