DATE: Wednesday, December 5, 2012
TIME: Noon - 1:00 pm
PLACE: GHC 8102
SPEAKER: Junfeng Yang, Columbia University
TITLE: Effectively Model Check Real-World Distributed Systems
ABSTRACT:
Distributed systems are the bedrock of cloud computing, yet these systems are notoriously difficult to get right. Although several implementation-level model checkers such as MoDist (our previous work) and dBug can find errors in these systems, they all face a well-known problem of model checking: a system typically has too many states for a model checker to completely explore---the so-called state-explosion problem.
In this talk, I'll describe our recent work that soundly reduces the number of states to check by up to five orders of magnitude. The insight is that system builders already decompose a system into components with narrow interfaces, so a model checker can leverage these interfaces to check each component separately, avoiding expensive global exploration of all components. I'll also describe our on-going work to further reduce states using a technique we call stable multithreading.
BIO:
Junfeng Yang's research centers on making reliable and secure systems. He earned his PhD at Stanford, where he created eXplode, a general, lightweight system for effectively finding storage system errors. This work has led to an OSDI '04 best paper, numerous bug fixes to real systems such as the Linux kernel, and a featured article in Linux Weekly news. He worked at Microsoft Research, Silicon Valley from 2007-2008, extending eXplode to check production distributed systems. MoDist, the resultant system, is being transferred to Microsoft product groups. He's now co-directing the Software Systems Lab (ssl.cs.columbia.edu) at Columbia University, where his recent work on making reliable parallel programs, the Tern/Peregrine stable multithreading system, was featured in ACM Tech News, The Register, and many other sites. He won Sloan and AFOSR YIP both in 2012; and NSF CAREER in 2011.
HOST:
Garth Gibson
VISITOR COORDINATOR:
Jenn Landefeld (jennsbl@cs.cmu.edu)
SDI / ISTC SEMINAR QUESTIONS?
Karen Lindenfelser, 86716, or visit www.pdl.cmu.edu/SDI/