TY - GEN
T1 - Verifying concurrent, crash-safe systems with perennial
AU - Chajed, Tej
AU - Tassarotti, Joseph
AU - Kaashoek, M. F.
AU - Zeldovich, Nickolai
N1 - Funding Information:
We’d like to thank Butler Lampson, Jay Lorch, the anonymous reviewers, and our shepherd, Gernot Heiser, who provided comments that helped improve this paper. This research was supported by NSF awards CNS-1563763 and CCF-1836712, Google, and Oracle Labs. Tej Chajed is supported by an SOSP 2019 student scholarship from the National Science Foundation.
Funding Information:
We?d like to thank Butler Lampson, Jay Lorch, the anonymous reviewers, and our shepherd, Gernot Heiser, who provided comments that helped improve this paper. This research was supported by NSF awards CNS-1563763 and CCF-1836712, Google, and Oracle Labs. Tej Chajed is supported by an SOSP 2019 student scholarship from the National Science Foundation.
Publisher Copyright:
© 2019 Copyright held by the owner/author(s).
PY - 2019/10/27
Y1 - 2019/10/27
N2 - This paper introduces Perennial, a framework for verifying concurrent, crash-safe systems. Perennial extends the Iris concurrency framework with three techniques to enable crash-safety reasoning: recovery leases, recovery helping, and versioned memory. To ease development and deployment of applications, Perennial provides Goose, a subset of Go and a translator from that subset to a model in Perennial with support for reasoning about Go threads, data structures, and file-system primitives. We implemented and verified a crash-safe, concurrent mail server using Perennial and Goose that achieves speedup on multiple cores. Both Perennial and Iris use the Coq proof assistant, and the mail server and the framework’s proofs are machine checked.
AB - This paper introduces Perennial, a framework for verifying concurrent, crash-safe systems. Perennial extends the Iris concurrency framework with three techniques to enable crash-safety reasoning: recovery leases, recovery helping, and versioned memory. To ease development and deployment of applications, Perennial provides Goose, a subset of Go and a translator from that subset to a model in Perennial with support for reasoning about Go threads, data structures, and file-system primitives. We implemented and verified a crash-safe, concurrent mail server using Perennial and Goose that achieves speedup on multiple cores. Both Perennial and Iris use the Coq proof assistant, and the mail server and the framework’s proofs are machine checked.
KW - Concurrency
KW - Crash safety
KW - Separation logic
UR - http://www.scopus.com/inward/record.url?scp=85076769749&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85076769749&partnerID=8YFLogxK
U2 - 10.1145/3341301.3359632
DO - 10.1145/3341301.3359632
M3 - Conference contribution
AN - SCOPUS:85076769749
T3 - SOSP 2019 - Proceedings of the 27th ACM Symposium on Operating Systems Principles
SP - 243
EP - 258
BT - SOSP 2019 - Proceedings of the 27th ACM Symposium on Operating Systems Principles
PB - Association for Computing Machinery, Inc
T2 - 27th ACM Symposium on Operating Systems Principles, SOSP 2019
Y2 - 27 October 2019 through 30 October 2019
ER -