Practical Formal Verification of Concurrent Code in the 21st Century

09/09/2022

Speaker

Hernan Ponce de Leon

Abstract

Sequential Consistency (SC) is a simple (yet powerful) model of computation for concurrent systems. This model is the basis of most automatic tools to reason about concurrent code. Unfortunately, systems guaranteeing SC incur performance penalties that might be impractical in a realistic setting. Weaker (and more performant) notions of consistency have existed for years, but only recently their guarantees has been formalized. In this talk I'll discussed some of the advances in formal verification technology in the presence of weak consistency. Particularly, I will describe some of the lessons learned during the development of the Dartagnan model checker during the last 7 years. Those lessons allowed us to improve Dartagnan from analyzing only small code snippets in 2016, to analyze (and find bugs in!) complex algorithms from the Linux Kernel in 2022.

Bio

Hernan Ponce de Leon is a Principal Software Systems Research Engineer at Huawei. While he has always been interested in concurrency, over the years his research interests has moved from the theory of high level modeling languages (Petri nets), to how to practically apply verification technology to low level models, particularly the architecture and microarchitecture of modern processors.