Note that you are all welcome to attend all colloquium talks. You can subscribe to the talks list here: https://mailman.cs.washington.edu/mailman/listinfo/talks
NOTE: Corrections – this talk will *not* be taped or broadcast live! Location has also been changed!
UNIVERSITY OF WASHINGTON
Computer Science and Engineering
Research Seminar
SPEAKER: Ranjit Jhala, UCSD
TITLE: Finding Liveness Bugs in Systems Code
DATE: Tuesday, February 9, 2010
TIME: 3:30pm
PLACE: 403 Paul G. Allen Center for CSE
HOST: Michael Ernst
ABSTRACT:
In this talk, we describe a technique for finding bugs in complex concurrent and distributed systems implementations. To do so, the developer formally specifies high-level liveness properties which define desirable end-to-end system conditions, which need not always hold, perhaps as a result of failure or during system initialization, but which must eventually be satisfied.
Unfortunately, previous techniques cannot find liveness bugs because doing so requires finding an infinite execution that does not satisfy a liveness property.
We present probabilistic heuristics to find a large class of liveness violations and the critical transition of the violating execution. The critical transition is the step in an execution that moves the system from a state that can satisfy the liveness property in the future, to a dead state that can never achieve the liveness property, regardless of any subsequent sequence of actions.
Our approach is implemented in a software model checker, MaceMC. MaceMC isolated, without any false warnings, complex liveness errors in implementations of Pastry, Chord, a reliable transport protocol, an aggregation service, Overcast, and an overlay tree implementing a failure-resilient random tree, allowing us to understand and fix problems that had eluded detection for several years.
(Joint work with Chip Killian, James Anderson and Amin Vahdat)
BIO:
Ranjit Jhala is an Assistant Professor in the Department of Computer Science and Engineering at UC San Diego. Before joining UCSD, he was a graduate student at UC Berkeley. Ranjit is is interested in applying techniques from Programming Languages and Software Engineering to solve computing problems, in particular, to build reliable computer systems. His work draws from, combines and contributes to methods the areas of Model Checking, Program Analysis, Type Systems and Automated Deduction.
Email: talk-info@cs.washington.edu
Info: http://www.cs.washington.edu/
(206) 543-1695
The University of Washington is committed to providing access, equal opportunity and reasonable accomodation in its services, programs, activities, education and employment for individuals with disabilities. To request disability accommodation, contact the Disability Services Office at least ten days in advance of the event at: (206) 543-6450/V, (206) 543-6452/TTY, (206) 685-3885/FAX, or access@u.washington.edu.
_______________________________________________