Commutativity race detection

Dimitar Dimitrov, Veselin Raychev, Martin Vechev, Eric Koskinen

Research output: Contribution to journalArticlepeer-review

20 Scopus citations

Abstract

This paper introduces the concept of a commutativity race. A commutativity race occurs in a given execution when two library method invocations can happen concurrently yet they do not commute. Commutativity races are an elegant concept enabling reasoning about concurrent interaction at the library interface.

We present a dynamic commutativity race detector. Our technique is based on a novel combination of vector clocks and a structural representation automatically obtained from a commutativity specification. Conceptually, our work can be seen as generalizing classical read-write race detection.

We also present a new logical fragment for specifying commutativity conditions. This fragment is expressive, yet guarantees a constant number of comparisons per method invocation rather than linear with unrestricted specifications.

We implemented our analyzer and evaluated it on real-world applications. Experimental results indicate that our analysis is practical: it discovered harmful commutativity races with overhead comparable to state-of-the-art, low-level race detectors.

Original languageEnglish
Pages (from-to)305-315
Number of pages11
JournalACM SIGPLAN Notices
Volume49
Issue number6
DOIs
StatePublished - 5 Jun 2014

Fingerprint

Dive into the research topics of 'Commutativity race detection'. Together they form a unique fingerprint.

Cite this