Verifying concurrent, crash-safe systems with Perennial
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 applicati...
| Main Authors: | , , , |
|---|---|
| Other Authors: | |
| Format: | Article |
| Language: | English |
| Published: |
Association for Computing Machinery (ACM)
2021
|
| Online Access: | https://hdl.handle.net/1721.1/129984 |
| _version_ | 1826211967054905344 |
|---|---|
| author | Chajed, Tej Tassarotti, Joseph Kaashoek, M. Frans Zeldovich, Nickolai |
| author2 | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory |
| author_facet | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory Chajed, Tej Tassarotti, Joseph Kaashoek, M. Frans Zeldovich, Nickolai |
| author_sort | Chajed, Tej |
| collection | MIT |
| description | 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. |
| first_indexed | 2024-09-23T15:14:14Z |
| format | Article |
| id | mit-1721.1/129984 |
| institution | Massachusetts Institute of Technology |
| language | English |
| last_indexed | 2024-09-23T15:14:14Z |
| publishDate | 2021 |
| publisher | Association for Computing Machinery (ACM) |
| record_format | dspace |
| spelling | mit-1721.1/1299842022-09-29T13:34:21Z Verifying concurrent, crash-safe systems with Perennial Chajed, Tej Tassarotti, Joseph Kaashoek, M. Frans Zeldovich, Nickolai Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory 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. NSF (Awards CNS-1563763 and CCF- 1836712) 2021-02-23T22:14:55Z 2021-02-23T22:14:55Z 2019-10 2020-12-22T14:37:47Z Article http://purl.org/eprint/type/ConferencePaper 9781450368735 https://hdl.handle.net/1721.1/129984 Chajed, Tej et al. "Verifying concurrent, crash-safe systems with Perennial." Proceedings of the 27th ACM Symposium on Operating Systems Principles, October 2019, Huntsville, Ontario, Canada, Association for Computing Machinery, October 2019. © 2019 owner/author(s) en http://dx.doi.org/10.1145/3341301.3359632 Proceedings of the 27th ACM Symposium on Operating Systems Principles Creative Commons Attribution-Noncommercial-Share Alike http://creativecommons.org/licenses/by-nc-sa/4.0/ application/pdf Association for Computing Machinery (ACM) MIT web domain |
| spellingShingle | Chajed, Tej Tassarotti, Joseph Kaashoek, M. Frans Zeldovich, Nickolai Verifying concurrent, crash-safe systems with Perennial |
| title | Verifying concurrent, crash-safe systems with Perennial |
| title_full | Verifying concurrent, crash-safe systems with Perennial |
| title_fullStr | Verifying concurrent, crash-safe systems with Perennial |
| title_full_unstemmed | Verifying concurrent, crash-safe systems with Perennial |
| title_short | Verifying concurrent, crash-safe systems with Perennial |
| title_sort | verifying concurrent crash safe systems with perennial |
| url | https://hdl.handle.net/1721.1/129984 |
| work_keys_str_mv | AT chajedtej verifyingconcurrentcrashsafesystemswithperennial AT tassarottijoseph verifyingconcurrentcrashsafesystemswithperennial AT kaashoekmfrans verifyingconcurrentcrashsafesystemswithperennial AT zeldovichnickolai verifyingconcurrentcrashsafesystemswithperennial |