research-article

Commutativity race detection

Authors:

Dimitar Dimitrov,

Veselin Raychev,

Eric KoskinenAuthors Info & Claims

ACM SIGPLAN Notices, Volume 49, Issue 6

Pages 305 - 315

https://doi.org/10.1145/2666356.2594322

Published: 09 June 2014 Publication History

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.

References

[1]

Attiya, H., Guerraoui, R., Hendler, D., Kuznetsov, P., Michael, M., and Vechev, M. Laws of order: Expensive synchronization in concurrent algorithms cannot be eliminated. In ACM POPL'11.

Digital Library

[2]

Clements, A. T., Kaashoek, M. F., Zeldovich, N., Morris, R. T., and Kohler, E. The scalable commutativity rule: Designing scalable software for multicore processors. In ACM SOSP'13.

Digital Library

[3]

Flanagan, C., and Freund, S. N. Fasttrack: Efficient and precise dynamic race detection. In ACM PLDI'09.

Digital Library

[4]

Flanagan, C., and Freund, S. N. The roadrunner dynamic analysis framework for concurrent programs. In ACM PASTE'10.

Digital Library

[5]

Flanagan, C., Freund, S. N., and Yi, J. Velodrome: A sound and complete dynamic atomicity checker for multithreaded programs. In ACM PLDI'08.

Digital Library

[6]

Gao, Q., Zhang, W., Chen, Z., Zheng, M., and Qin, F. 2nd-strike: Toward manifesting hidden concurrency typestate bugs. In ACM ASPLOS'11.

Digital Library

[7]

Herlihy, M., and Koskinen, E. Transactional boosting: A methodology for highly-concurrent transactional objects. In ACM PPoPP '08.

Digital Library

[8]

Kim, D., and Rinard, M. C. Verification of semantic commutativity conditions and inverse operations on linked data structures. In ACM PLDI'11.

Digital Library

[9]

Korth, H. F. Locking primitives in a database system. Journal of the ACM'83.

Digital Library

[10]

Kulkarni, M., Nguyen, D., Prountzos, D., Sui, X., and Pingali, K. Exploiting the commutativity lattice. In ACM PLDI'11.

Digital Library

[11]

Kulkarni, M., Pingali, K., Walter, B., Ramanarayanan, G., Bala, K., and Chew, L. P. Optimistic parallelism requires abstractions. In ACM PLDI'07.

Digital Library

[12]

Lamport, L. Time, clocks, and the ordering of events in a distributed system. Communications of the ACM'78.

Digital Library

[13]

Lin, Y., and Dig, D. Check-then-act misuse of java concurrent collections. In IEEE ICST '13.

Digital Library

[14]

Mattern, F. Virtual time and global states of distributed systems. In Proc. Workshop on Parallel and Distributed Algorithms'88.

[15]

Schwarz, P. M., and Spector, A. Z. Synchronizing shared abstract types. ACM Trans. Comput. Syst.'84.

Digital Library

[16]

Shacham, O., Bronson, N., Aiken, A., Sagiv, M., Vechev, M., and Yahav, E. Testing atomicity of composed concurrent operations. In ACM OOPSLA'11.

Digital Library

[17]

Tripp, O., Yorsh, G., Field, J., and Sagiv, M. Hawkeye: Effective discovery of dataflow impediments to parallelization. In ACM OOPSLA'11.

Digital Library

[18]

Weihl, W. E. Commutativity-based concurrency control for abstract data types. In Twenty-First Annual Hawaii International Conference on Software Track'88.

Digital Library

Cited By

Popovic MPopovic MGhilezan SKordic B(2019)Formal Verification of Python Software Transactional Memory Serializability Based on the Push/Pull Semantic ModelProceedings of the 6th Conference on the Engineering of Computer Based Systems10.1145/3352700.3352706(1-8)Online publication date: 2-Sep-2019
https://dl.acm.org/doi/10.1145/3352700.3352706
Nishi M(2019)Process Barrier for Predictable and Repeatable Concurrent ExecutionProceedings of the 10th International Workshop on Programming Models and Applications for Multicores and Manycores10.1145/3303084.3309494(71-80)Online publication date: 17-Feb-2019
https://dl.acm.org/doi/10.1145/3303084.3309494
Sun YCheung SGuo SCheng M(2019)Disclosing and Locating Concurrency Bugs of Interrupt-Driven IoT ProgramsIEEE Internet of Things Journal10.1109/JIOT.2019.29252916:5(8945-8957)Online publication date: Oct-2019
https://doi.org/10.1109/JIOT.2019.2925291
Show More Cited By

Recommendations

Commutativity race detection
PLDI '14: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation

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 ...
Dynamic race detection for C++11
POPL '17: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages

The intricate rules for memory ordering and synchronisation associated with the C/C++11 memory model mean that data races can be difficult to eliminate from concurrent programs. Dynamic data race analysis can pinpoint races in large and complex ...
Semantics-based Concurrency Contro: Beyond Commutativity

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 49, Issue 6

PLDI '14

June 2014

598 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/2666356

Editor:
Andy Gill
University of Kansas, Lawrence, KS

Issue’s Table of Contents

PLDI '14: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation
June 2014
619 pages
ISBN:9781450327848
DOI:10.1145/2594291
General Chair:
Michael O'Boyle
University of Edinburgh
,
Program Chair:
Keshav Pingali
University of Texas, Austin

Copyright © 2014 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 09 June 2014

Published in SIGPLAN Volume 49, Issue 6

Check for updates

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

57
Total Citations
View Citations
341
Total Downloads

Downloads (Last 12 months)12
Downloads (Last 6 weeks)5

Reflects downloads up to 12 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Popovic MPopovic MGhilezan SKordic B(2019)Formal Verification of Python Software Transactional Memory Serializability Based on the Push/Pull Semantic ModelProceedings of the 6th Conference on the Engineering of Computer Based Systems10.1145/3352700.3352706(1-8)Online publication date: 2-Sep-2019
https://dl.acm.org/doi/10.1145/3352700.3352706
Nishi M(2019)Process Barrier for Predictable and Repeatable Concurrent ExecutionProceedings of the 10th International Workshop on Programming Models and Applications for Multicores and Manycores10.1145/3303084.3309494(71-80)Online publication date: 17-Feb-2019
https://dl.acm.org/doi/10.1145/3303084.3309494
Sun YCheung SGuo SCheng M(2019)Disclosing and Locating Concurrency Bugs of Interrupt-Driven IoT ProgramsIEEE Internet of Things Journal10.1109/JIOT.2019.29252916:5(8945-8957)Online publication date: Oct-2019
https://doi.org/10.1109/JIOT.2019.2925291
Wang PLu KLi GZhou X(2019)DFTrackerFrontiers of Computer Science: Selected Publications from Chinese Universities10.1007/s11704-016-6383-813:2(247-263)Online publication date: 1-Apr-2019
https://dl.acm.org/doi/10.1007/s11704-016-6383-8
Nakade RMercer EAldous PStorey KOgles BHooker JPowell SMcCarthy J(2019)Model-checking task-parallel programs for data-raceInnovations in Systems and Software Engineering10.1007/s11334-019-00343-5Online publication date: 18-May-2019
https://doi.org/10.1007/s11334-019-00343-5
Storey KPowell JOgles BHooker JAldous PMercer E(2019)Optimized Sound and Complete Data Race Detection in Structured Parallel ProgramsLanguages and Compilers for Parallel Computing10.1007/978-3-030-34627-0_8(94-111)Online publication date: 13-Nov-2019
https://doi.org/10.1007/978-3-030-34627-0_8
Dickerson TKoskinen EGazzillo PHerlihy M(2019)Conflict Abstractions and Shadow Speculation for Optimistic Transactional ObjectsProgramming Languages and Systems10.1007/978-3-030-34175-6_16(313-331)Online publication date: 18-Nov-2019
https://doi.org/10.1007/978-3-030-34175-6_16
Luo PZou DJin HDu YZheng LShen J(2018)DigHRThe Journal of Supercomputing10.1007/s11227-018-2307-874:6(2684-2704)Online publication date: 1-Jun-2018
https://dl.acm.org/doi/10.1007/s11227-018-2307-8
Bansal KKoskinen ETripp O(2018)Automatic Generation of Precise and Useful Commutativity ConditionsTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-319-89960-2_7(115-132)Online publication date: 12-Apr-2018
https://doi.org/10.1007/978-3-319-89960-2_7
Nakade RMercer EAldous PMcCarthy J(2018)Model-Checking Task Parallel Programs for Data-RaceNASA Formal Methods10.1007/978-3-319-77935-5_25(367-382)Online publication date: 11-Mar-2018
https://doi.org/10.1007/978-3-319-77935-5_25
Show More Cited By

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents