Grove: a Separation-Logic Library for Verifying Distributed Systems (Extended Version)

TL;DR

Grove introduces a novel separation-logic library for verifying distributed systems, effectively handling time-based leases and reconfiguration, demonstrated through verifying a high-performance, scalable distributed key-value store in Go.

Contribution

First to incorporate time-based leases in a separation-logic framework for distributed system verification, enabling correctness proofs for reconfiguration and crash recovery.

Findings

GroveKV supports reconfiguration, crash recovery, and lease-based read execution.

GroveKV achieves 67-73% of Redis performance on a single core.

Scales nearly linearly with additional cores and replicas.

Abstract

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.