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

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.