Grove: a Separation-Logic Library for Verifying Distributed Systems

Upamanyu Sharma; Ralf Jung; Joseph Tassarotti; Frans Kaashoek; Nickolai Zeldovich

doi:10.1145/3600006.3613172

Grove: a Separation-Logic Library for Verifying Distributed Systems

Upamanyu Sharma, Ralf Jung, Joseph Tassarotti, Frans Kaashoek, Nickolai Zeldovich

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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 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.

Original language	English (US)
Title of host publication	SOSP 2023 - Proceedings of the 29th ACM Symposium on Operating Systems Principles
Publisher	Association for Computing Machinery, Inc
Pages	113-129
Number of pages	17
ISBN (Electronic)	9798400702297
DOIs	https://doi.org/10.1145/3600006.3613172
State	Published - Oct 23 2023
Event	29th ACM Symposium on Operating Systems Principles, SOSP 2023 - Koblenz, Germany Duration: Oct 23 2023 → Oct 26 2023

Publication series

Name	SOSP 2023 - Proceedings of the 29th ACM Symposium on Operating Systems Principles

Conference

Conference	29th ACM Symposium on Operating Systems Principles, SOSP 2023
Country/Territory	Germany
City	Koblenz
Period	10/23/23 → 10/26/23

ASJC Scopus subject areas

Computational Theory and Mathematics
Computer Science Applications
Software

Access to Document

10.1145/3600006.3613172

Cite this

Sharma, U., Jung, R., Tassarotti, J., Kaashoek, F., & Zeldovich, N. (2023). Grove: a Separation-Logic Library for Verifying Distributed Systems. In SOSP 2023 - Proceedings of the 29th ACM Symposium on Operating Systems Principles (pp. 113-129). (SOSP 2023 - Proceedings of the 29th ACM Symposium on Operating Systems Principles). Association for Computing Machinery, Inc. https://doi.org/10.1145/3600006.3613172

Grove: a Separation-Logic Library for Verifying Distributed Systems. / Sharma, Upamanyu; Jung, Ralf; Tassarotti, Joseph et al.
SOSP 2023 - Proceedings of the 29th ACM Symposium on Operating Systems Principles. Association for Computing Machinery, Inc, 2023. p. 113-129 (SOSP 2023 - Proceedings of the 29th ACM Symposium on Operating Systems Principles).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Sharma, U, Jung, R, Tassarotti, J, Kaashoek, F & Zeldovich, N 2023, Grove: a Separation-Logic Library for Verifying Distributed Systems. in SOSP 2023 - Proceedings of the 29th ACM Symposium on Operating Systems Principles. SOSP 2023 - Proceedings of the 29th ACM Symposium on Operating Systems Principles, Association for Computing Machinery, Inc, pp. 113-129, 29th ACM Symposium on Operating Systems Principles, SOSP 2023, Koblenz, Germany, 10/23/23. https://doi.org/10.1145/3600006.3613172

Sharma U, Jung R, Tassarotti J, Kaashoek F, Zeldovich N. Grove: a Separation-Logic Library for Verifying Distributed Systems. In SOSP 2023 - Proceedings of the 29th ACM Symposium on Operating Systems Principles. Association for Computing Machinery, Inc. 2023. p. 113-129. (SOSP 2023 - Proceedings of the 29th ACM Symposium on Operating Systems Principles). doi: 10.1145/3600006.3613172

@inproceedings{70f185030d5e41c6bc91566ba2fc43f2,

title = "Grove: a Separation-Logic Library for Verifying Distributed Systems",

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 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.",

author = "Upamanyu Sharma and Ralf Jung and Joseph Tassarotti and Frans Kaashoek and Nickolai Zeldovich",

note = "Publisher Copyright: {\textcopyright} 2023 Owner/Author(s).; 29th ACM Symposium on Operating Systems Principles, SOSP 2023 ; Conference date: 23-10-2023 Through 26-10-2023",

year = "2023",

month = oct,

day = "23",

doi = "10.1145/3600006.3613172",

language = "English (US)",

series = "SOSP 2023 - Proceedings of the 29th ACM Symposium on Operating Systems Principles",

publisher = "Association for Computing Machinery, Inc",

pages = "113--129",

booktitle = "SOSP 2023 - Proceedings of the 29th ACM Symposium on Operating Systems Principles",

}

TY - GEN

T1 - Grove

T2 - 29th ACM Symposium on Operating Systems Principles, SOSP 2023

AU - Sharma, Upamanyu

AU - Jung, Ralf

AU - Tassarotti, Joseph

AU - Kaashoek, Frans

AU - Zeldovich, Nickolai

PY - 2023/10/23

Y1 - 2023/10/23

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85172354600&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85172354600&partnerID=8YFLogxK

U2 - 10.1145/3600006.3613172

DO - 10.1145/3600006.3613172

M3 - Conference contribution

AN - SCOPUS:85172354600

T3 - SOSP 2023 - Proceedings of the 29th ACM Symposium on Operating Systems Principles

SP - 113

EP - 129

BT - SOSP 2023 - Proceedings of the 29th ACM Symposium on Operating Systems Principles

PB - Association for Computing Machinery, Inc

Y2 - 23 October 2023 through 26 October 2023

ER -

Grove: a Separation-Logic Library for Verifying Distributed Systems

Abstract

Publication series

Conference

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this