Commutativity Race Detection: Concepts, Algorithms and Open Problems

Martin Vechev

In this talk I will introduce the notion of a commutativity race. A commutativity race occurs when two method invocations happen concurrently yet they do not commute (according to a logical specification). Commutativity races are an elegant concept which generalize classic data races and enable reasoning about concurrent interaction at the library interface. I will then present an approach which takes as input a logical specification that captures commutativity and automatically synthesizes an ecient concurrency analyzer for that specification. The resulting analyzers have been used to find concurrency errors in large scale production applications. Finally, generalization of classic data race detection leads to many fundamental research questions, which I will discuss, including: black box specification learning, impossibility of simulating race detectors, connections between logical fragments and asymptotic complexity of the analysis, as well as various practical applications.