推断生产级键值存储的形式化性质
分布式、并行与集群计算
2018-01-01 v1 计算机科学中的逻辑
摘要
生产级分布式系统难以形式化验证，尤其当它们基于未被严格描述或未被完全理解的分布式协议时。本文中，我们为最终一致的生产级键值存储（如 Riak 与 Cassandra）所使用的两个核心分布式协议推导模型与性质。我们提出一种称为认证程序模型的新颖建模方式，其中完整分布式系统被捕获为用传统系统语言（如并发 C）编写的程序。具体而言，我们将读修复与暗示切换（hinted-handoff）恢复协议建模为并发 C 程序，对其实与真实系统的符合性进行测试，随后验证它们保证最终一致性，精确建模了规范以及结果成立所依赖的失效假设。
引用
@article{arxiv.1712.10056,
title = {Inferring Formal Properties of Production Key-Value Stores},
author = {Edgar Pek and Pranav Garg and Muntasir Raihan Rahman and Karl Palmskog and Indranil Gupta and P. Madhusudan},
journal= {arXiv preprint arXiv:1712.10056},
year = {2018}
}
备注
15 pages, 2 figures