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 GroveKV, a realistic distributed multi-threaded key-value store. GroveKV supports reconfiguration, primary/backup replication, and crash recovery, and uses leases to execute read-only requests on any replica. GroveKV achieves high performance (67-73% of Redis on a single core), scales with more cores and more backup replicas (achieving about 2x the throughput when going from 1 to 3 servers), and can safely execute reads while reconfiguring.

翻译：Grove是一个用于验证分布式系统的并发分离逻辑库。Grove是首个能够处理基于时间的租约问题的解决方案，涵盖了租约与重配置、崩溃恢复、线程级并发以及不可靠网络之间的交互。本文利用Grove验证了用Go编写的多个分布式系统组件，包括GroveKV——一个实际的多线程分布式键值存储系统。GroveKV支持重配置、主备复制和崩溃恢复，并使用租约在任何副本上执行只读请求。GroveKV实现了高性能（单核性能达到Redis的67-73%），随着核心数和备份副本数量的增加，其吞吐量呈线性扩展（从1台服务器扩展到3台时，吞吐量提升约2倍），并且能够在重配置过程中安全地执行读取操作。