EXPLODE: a lightweight, General System for Finding Serious Storage System Errors

Storage systems such as file systems, databases, and RAID systems have a simple, basic contract: you give them data, they do not lose or corrupt it. Unfortunately, their code is exceptionally hard to get right: it must anticipate all failures and crashes, and always correctly recover from them, regardless of the current system state. In this talk, I will describe EXPLODE, a storage system checking tool we developed that makes it easy to systematically check real storage systems for errors. EXPLODE practically adapts ideas from model checking, a comprehensive, heavyweight formal verification technique, which makes it systematic while being lightweight. We applied EXPLODE to a broad range of real storage systems, and found serious data-loss errors in every system checked, typically with little effort.

Biography:

Junfeng Yang is a Ph.D. candidate in the Computer Science Department at Stanford. His research interests span the areas of systems, security, software engineering and programming languages, focusing on practically checking large, real-world software systems. Junfeng Yang received his MS in Computer Science from Stanford in 2002, and his BS in Computer Science from Tsinghua University, Beijing, China in 2000. He is a receipt of the Siebel Scholarship and the Stanford School of Engineering fellowship. He received the Best Paper Award of OSDI 2004.