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

Full description

Bibliographic Details
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