INDIMO: Invariant Discovery and Monitoring for Message-Passing Programs

Software systems that rely on message-passing concurrency are increasingly popular thanks to programming languages such as Go, Rust, Erlang, and Kotlin which support it natively. These languages notably power WhatsApp's servers, Uber's software infrastructure, and the NHS information backbone. They are popular, because message-passing concurrency allows parts of a software system to run in parallel while coordinating by exchanging messages. This is in contrast to shared memory concurrency, where memory accesses by concurrent components are protected by mutexes. Two key advantages of message-passing concurrency are that it is higher-level and avoids data-race bugs by construction. However, just like mutex-based concurrency, message-passing concurrency is liable to bugs such as deadlocks—which can cause huge performance problems and correctness issues. For instance, Uber, one of our project partners, regularly has concurrency bugs that make it into production and impact up to 1,000,000 users. This project aims at designing new techniques and tools to detect such bugs automatically, with a particular focus on programs that include statically unknown parameters that affect their concurrent structure, e.g., communication channel bounds, number of concurrent processes. We will adopt a hybrid approach to software verification that will give us the best of both worlds: the high coverage of static approaches and the high precision of dynamic approaches. Our key technical insight hinges on inferring logical properties—we call them Optimistic Invariants—that affect the presence or absence of a concurrency bug. Our project will make contributions to four areas of computer science: Verification of concurrent systems. We will produce novel techniques to reason about systems that communicate via message-passing. Our algorithms will infer optimistic invariants from an intermediate representation (IR). These invariants will be used to detect bugs and output the logical conditions that affect their presence. Static analysis. We will design an IR that will serve as a convenient abstraction for high-level message-passing programs. Our IR will model the concurrency-related instructions and the data aspects that affect the concurrent structure of programs. We will produce tools to compile Go and Erlang programs to this IR, this will enable the verification of real-world codebases. Runtime monitoring. We will design low-overhead techniques to monitor optimistic invariants at runtime. This will allow us to understand better the difference between their dynamic and static properties, produce techniques to enforce invariants, and to mitigate bugs at runtime. Software engineering. Our tool chain will be evaluated on the industrial codebases of Uber and WhatsApp, as well as open-source projects. We will perform user surveys to assess the effectiveness of our optimistic invariant-based approach. Our techniques will be validated in collaboration with Uber and WhatsApp, two heavy users of message-passing concurrency in Go and Erlang. Our tools will be open source so that any developers may benefit from our software improvement techniques. This will impact the quality of software systems as fundamental as Docker and Kubernetes, two platforms built with Go powering most modern software infrastructure. In the longer term, our project will help decrease the cost of producing high-quality software and produce more secure software for the end users.