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.
