Sat 22 Jan 2022 13:30 - 14:30 at Salon I - Invited Talk II Chair(s): Amin Timany

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.

Sat 22 Jan

Displayed time zone: Eastern Time (US & Canada) change

13:30 - 14:30
Invited Talk IICoqPL at Salon I
Chair(s): Amin Timany Aarhus University
Verifying Concurrent, Crash-Safe Systems with PerennialRemote
I: Joseph Tassarotti Boston College