Storage systems, such as databases and file systems, often have concurrent implementations. These systems are expected to be crash-safe, meaning that they should be able to recover from failures caused by power loss. However, achieving crash-safety is difficult because programmers must consider many potential interleavings of threads as well as the possibility of interruption from crashes at any point. Perennial is a framework for formally verifying crash safety of concurrent systems. This talk will describe the core reasoning principles of Perennial and our experience using Perennial to verify GoTxn, a concurrent transaction system.

Joint work with Tej Chajed, Mark Theng, Ralf Jung, Frans Kaashoek, and Nickolai Zeldovich.