A Lightweight, General Approach to Finding Serious Storage System Errors

April 2, 2007
Time: 11:00am-12:00pm
InterSchool Lab, 7th floor CEPSR
Hosted by: CS Department
Speaker: Junfeng Yang, Stanford University

Abstract

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 an approach we invented that makes it easy to systematically check real storage systems for errors. We used a novel adaption from model checking, a comprehensive, heavyweight formal verification technique, that makes our approach systematic while being lightweight. We applied this approach to a broad range of real storage systems, and found serious data-loss bugs in every system checked, typically with little effort.

Speaker 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, the Stanford School of Engineering fellowship. He received the Best Paper Award of OSDI 2004.


500 W. 120th St., Mudd 1310, New York, NY 10027    212-854-3105               
©2014 Columbia University