TY - GEN
T1 - Commutativity race detection
AU - Dimitrov, Dimitar
AU - Raychev, Veselin
AU - Vechev, Martin
AU - Koskinen, Eric
PY - 2014
Y1 - 2014
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84901623111&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84901623111&partnerID=8YFLogxK
U2 - 10.1145/2594291.2594322
DO - 10.1145/2594291.2594322
M3 - Conference contribution
AN - SCOPUS:84901623111
SN - 9781450327848
T3 - Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)
SP - 305
EP - 315
BT - PLDI 2014 - Proceedings of the 2014 ACM SIGPLAN Conference on Programming Language Design and Implementation
T2 - 35th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2014
Y2 - 9 June 2014 through 11 June 2014
ER -