10-21

Avenger: Catching Bugs in Distributed Systems Via Almost-Invariant Inference

It is notoriously hard to develop dependable distributed systems. This is partly due to the difficulties in foreseeing various corner cases and failure scenarios while the system is running over an asynchronous network. Reasoning about the distributed system invariants is easier than reasoning about the code itself. The invariants can be used for debugging, theorem proving, and runtime enforcement. In this talk, I'll introduce an approach to observe the behavior of a system and automatically infer invariants which reveal the bugs in the current implementation of the system. Using our tool, Avenger, we automatically generate a large number of potentially relevant properties, check them against the traces of system executions, and filter out all but a few properties before reporting them to the developer. Our key insight in filtering is that a good candidate for an invariant is the one that holds in all but a few cases, i.e., an "almost-invariant". Our experimental results with the BGP, RandTree, and Chord implementations demonstrate Avenger's ability to identify the almost-invariants that lead the developer to programming errors.

Bio:
Marco Canini received the "laurea" degree in Computer Science and Engineering from the University of Genoa, Italy. He holds a Ph.D. degree from the Department of Communications, Computer and Systems Science (DIST) of the University of Genoa. During his Ph.D., he was invited as a visitor to the University of Cambridge, Computer Laboratory. He now is with the Networked Systems Laboratory at EPFL, Switzerland. His research focuses on computer networking with emphasis on rethinking Internet fundamentals to include power awareness and improve Internet's energy efficiency, methods for Internet traffic classification based on application identification, design of network monitoring applications, and graphical visualization of networking data.