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: | Chajed, Tej, Tassarotti, Joseph, Kaashoek, M. Frans, Zeldovich, Nickolai |
---|---|
Other Authors: | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory |
Format: | Article |
Language: | English |
Published: |
Association for Computing Machinery (ACM)
2021
|
Online Access: | https://hdl.handle.net/1721.1/129984 |
Similar Items
-
Argosy: verifying layered storage systems with recovery refinement
by: Chajed, Tej, et al.
Published: (2021) -
Verifying a concurrent, crash-safe file system with sequential reasoning
by: Chajed, Tej
Published: (2022) -
Verifying a high-performance crash-safe file system using a tree specification
by: Chen, Haogang, et al.
Published: (2021) -
Grove: a Separation-Logic Library for Verifying Distributed Systems
by: Sharma, Upamanyu, et al.
Published: (2023) -
Using Crash Hoare logic for certifying the FSCQ file system
by: Chen, Haogang, et al.
Published: (2021)