Finding Flaws in Unmodified Distributed Systems
Principal Investigator: Charles Killian
Debugging distributed systems is notoriously difficult. This is in large part due to both the software complexity and accordingly large state space, and because of the inherent asynchrony in networked systems. We have built a model-checker to test unmodified distributed systems built with the Mace programming toolkit. The modelchecker (MaceMC) uses automated state space exploration combined with long random execution to find and isolate bugs forcing distributed systems to violate liveness properties, which are essentially the properties which developers to specify that a system not only avoids bad states, but eventually accomplishes its goal.
We continue to extend the features and capabilities of the Mace model checker. We are now working on how to use the model checking infrastructure to find performance bugs in unmodified distributed systems, and how to incorporate malicious agents into the testing infrastructure to automatically detect errors and system degradation caused by these malicious agents, and to verify fixes once designed.
Students: Hyojeong Lee Karthik Nagaraj Salman Pervez Anurag Singh Sunghwan Yoo
Darren Dao, Jeannie Albrecht, Charles Killian, and Amin Vahdat, “Live Debugging of Distributed Systems", International Conference on Compiler Construction, York, UK, March, 2009.
Dejan Kostic, Alex C. Snoeren, Amin Vahdat, Ryan Braud, Charles Killian, Jeannie Albrecht, James W. Anderson, Adolfo Rodriguez, and Erik Vandekieft ,"High Bandwidth Data Dissemination for Large-scale Distributed Systems",ACM Transactions on Computer Systems, 2008
Keywords: debug, errors, infrastructure, security