Grove: a Separation-Logic Library for Verifying Distributed Systems
Grove: a Separation-Logic Library for Verifying Distributed Systems
复制标题
DOI：
10.1145/3600006.3613172
复制
发表时间：
2023-09
期刊：
影响因子：
--
通讯作者：
Upamanyu Sharma;Ralf Jung;Joseph Tassarotti;Frans Kaashoek;Nickolai Zeldovich
中科院分区：
文献类型：
--
作者：
Upamanyu Sharma;Ralf Jung;Joseph Tassarotti;Frans Kaashoek;Nickolai Zeldovich
Grove 是一个用于验证分布式系统的并发分离逻辑库。 Grove 是第一个处理基于时间的租约的系统，包括它们与重新配置、崩溃恢复、线程级并发和不可靠网络的交互。本文使用 Grove 验证了几个用 Go 编写的分布式系统组件，包括 vKV，一个现实的分布式多线程键值存储。 vKV 支持重新配置、主/备份复制和崩溃恢复，并使用租约在任何副本上执行只读请求。 vKV 实现了高性能（单个核心上的 Redis 的 67--73%），可通过更多核心和更多备份副本进行扩展（从 1 台服务器增加到 3 台服务器时，吞吐量可达到约 2 倍），并且可以在重新配置时安全地执行读取。
Grove is a concurrent separation logic library for verifying distributed systems. Grove is the first to handle time-based leases, including their interaction with reconfiguration, crash recovery, thread-level concurrency, and unreliable networks. This paper uses Grove to verify several distributed system components written in Go, including vKV, a realistic distributed multi-threaded key-value store. vKV supports reconfiguration, primary/backup replication, and crash recovery, and uses leases to execute read-only requests on any replica. vKV achieves high performance (67--73% of Redis on a single core), scales with more cores and more backup replicas (achieving about 2× the throughput when going from 1 to 3 servers), and can safely execute reads while reconfiguring.