Equivalences for Causal Concurrency with Umang Mathur

Abstract:Testing and verifying concurrent software is challenging due to the vast number of possible thread interleavings. But many of these interleavings are effectively equivalent, i.e., they represent the same underlying behavior. Indeed, identifying such equivalences can significantly improve efficiency: in verification, it allows us to prune redundant executions, and in testing, it lets us generalize from a single execution to an entire class, increasing coverage.

In this talk, I will delve deeper into some notions of equivalence between concurrent executions and the computational questions that arise when reasoning about them. I'll begin with trace theory, an elegant framework for defining equivalence based on commutativity of events that has remained popular for the algorithmic benefits it offers. I'll discuss classic and recent computational results regarding trace equivalence in the setting of predictive runtime testing of concurrent software.

I will then turn to reads-from equivalence, a more modern notion of equivalence that captures data and control dependencies between events in an execution. This notion yields a coarser equivalence, allowing for the potential of greater reduction in verification tasks and greater generalizations in testing tasks. However, this coarsening comes with an efficiency tradeoff manifesting as hardness results that I will discuss next.

Finally, I'll describe our recent work on generalizing trace theory to bridge these two notions of equivalences, aiming to retain the algorithmic strengths of trace theory while capturing the practical advantages of coarser equivalence notions like reads-from.

Bio: Umang Mathur is a Presidential Young Professor at the National University of Singapore, where he leads the FOCS lab. He received his PhD from the University of Illinois at Urbana Champaign and was an NTT Research Fellow at the Simons Institute for the Theory of Computing at Berkeley. His research broadly centers on developing techniques inspired from formal methods and logic for answering design, analysis and implementation questions in programming languages, software engineering and computer systems, has been recognized by Distinguished and Best Paper awards at POPL, ASPLOS, FSE and CPP, a SIGPLAN research highlights award, and has been supported by a PhD fellowship and research grant by Google. More details: https://www.comp.nus.edu.sg/~umathur/