Commutativity race detection

Dimitar Dimitrov, Veselin Raychev, Martin Vechev, Eric Koskinen

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

29 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
Title of host publicationPLDI 2014 - Proceedings of the 2014 ACM SIGPLAN Conference on Programming Language Design and Implementation
Pages305-315
Number of pages11
DOIs
StatePublished - 2014
Event35th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2014 - Edinburgh, United Kingdom
Duration: 9 Jun 201411 Jun 2014

Publication series

NameProceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)

Conference

Conference35th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2014
Country/TerritoryUnited Kingdom
CityEdinburgh
Period9/06/1411/06/14

Fingerprint

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

Cite this