Analysis of Message-Passing Concurrency: The Challenges of Asynchrony, Mobility, and Faults


April 15, 2014


Damien Zufferey




Asynchronous message-passing concurrency is a natural model for many services and event-driven systems ranging from device drivers to smartphones and the cloud. Interactions between the systems’ components or with the environment occurs through the exchange of messages. Developing such systems is challenging as the number of possible executions, e.g. message interleaving, makes it hard to catch and reproduce bugs. In this talk, I will present methods to help the programmer in this task, and verify those systems. First, I will shortly describe P, a domain-specific language to write asynchronous event driven code. P isolates the control-structure, or protocol, from the data-processing. This allows us not only to generate efficient code, but also to test it using model checking techniques. P was used to implement and validate the core of the USB device driver stack that ships with Microsoft Windows 8. Next, we will look at systems that are dynamic and mobile, i.e., where the number of processes and communication links change over time. Unfortunately, many analysis techniques, such as the validation in P, only deals with finite-state systems and cannot analyze mobile processes. I will present an analysis method for mobile processes that overcomes this limitation. The analysis exploits the monotonic behavior of the system and a graph-based abstract domain to compactly represent infinite sets of processes and their interactions. Finally, I will discuss the limitations of asynchrony, in particular when faults are considered, and lay out a research direction about programming and verifying fault-tolerant distributed systems.


Damien Zufferey

Damien Zufferey is a Postdoctoral researcher in Martin Rinard’s group at MIT CSAIL since Octorber 2013. Before moving to MIT, He obtained a PhD at the Institute of Science and Technology Austria (IST Austria) under supervision of Thomas A. Henzinger in September 2013 and a Master in computer science from EPFL in 2009. He is interested in improving software reliability by developing theoretical models, building analysis tools, and giving the programmer the appropriate language constructs. He is particularly interested in the study of complex concurrent systems. His research lies at the intersection of formal methods and programming languages. During the winter 2011-2012 he has done an internship at MSR in the RiSE group working with Shaz Qadeer and Ethan Jackson.