research-article

GAMBIT: effective unit testing for concurrency libraries

Authors:

Katherine E. Coons,

Sebastian Burckhardt,

Madanlal MusuvathiAuthors Info & Claims

PPoPP '10: Proceedings of the 15th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming

Pages 15 - 24

https://doi.org/10.1145/1693453.1693458

Published: 09 January 2010 Publication History

Abstract

As concurrent programming becomes prevalent, software providers are investing in concurrency libraries to improve programmer productivity. Concurrency libraries improve productivity by hiding error-prone, low-level synchronization from programmers and providing higher-level concurrent abstractions. Testing such libraries is difficult, however, because concurrency failures often manifest only under particular scheduling circumstances. Current best testing practices are often inadequate: heuristic-guided fuzzing is not systematic, systematic schedule enumeration does not find bugs quickly, and stress testing is neither systematic nor fast.

To address these shortcomings, we propose a prioritized search technique called GAMBIT that combines the speed benefits of heuristic-guided fuzzing with the soundness, progress, and reproducibility guarantees of stateless model checking. GAMBIT combines known techniques such as partial-order reduction and preemption-bounding with a generalized best-first search frame- work that prioritizes schedules likely to expose bugs. We evaluate GAMBIT's effectiveness on newly released concurrency libraries for Microsoft's .NET framework. Our experiments show that GAMBIT finds bugs more quickly than prior stateless model checking techniques without compromising coverage guarantees or reproducibility.

References

[1]

Concurrency and Coordination Runtime - http://msdn.microsoft.com/en-us/library/bb648752.aspx.

[2]

E. M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Logic of Programs, pages 52--71, London, UK, 1981. Springer-Verlag.

Digital Library

[3]

J. Duffy. A query language for data parallel programming: invited talk. In DAMP, page 50, 2007.

Digital Library

[4]

M. B. Dwyer, S. Elbaum, S. Person, and R. Purandare. Parallel randomized state-space search. In Proceedings of the 29th international conference on Software Engineering (ICSE '07), pages 3--12, Washington, DC, USA, 2007. IEEE Computer Society.

Digital Library

[5]

S. Edelkamp and S. Jabbar. Large-scale directed model checking ltl. In SPIN Workshop on Model Checking of Software, pages 1--18. Springer, 2006.

Digital Library

[6]

S. Edelkamp, A. L. Lafuente, and S. Leue. Directed explicit model checking with HSF-SPIN. In SPIN Workshop on Model Checking of Software, pages 57--79. Springer-Verlag, 2001.

Digital Library

[7]

O. Edelstein, E. Farchi, E. Goldin, Y. Nir, G. Ratsaby, and S. Ur. Framework for testing multi-threaded java programs. Concurrency and Computation: Practice and Experience, 15(3-5):485--499, 2003.

[8]

C. Flanagan and P. Godefroid. Dynamic partial-order reduction for model checking software. In 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '05), pages 110--121, 2005.

Digital Library

[9]

P. Godefroid. Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem. Springer-Verlag New York, Inc., Secaucus, NJ, USA, 1996. Foreword By-Pierre Wolper.

Digital Library

[10]

P. Godefroid.Model checking for programming languages using Verisoft. In POPL 97: Principles of Programming Languages, pages 174--186. ACM Press, 1997.

Digital Library

[11]

P. Godefroid and S. Khurshid. Exploring very large state spaces using genetic algorithms. In In Tools and Algorithms for the Construction and Analysis of Systems, pages 266--280. Springer, 2002.

Digital Library

[12]

P. Godefroid and P. Wolper. Using partial orders for the efficient verification of deadlock freedom and safety properties. In Computer Aided Verification (CAV '91), pages 332--342, 1992.

Digital Library

[13]

A. Groce and W. Visser. Heuristic model checking for java programs. In Proceedings of the 9th International SPIN Workshop on Model Checking of Software, pages 242--245, London, UK, 2002. Springer-Verlag.

Digital Library

[14]

G. Holzmann. The model checker SPIN. IEEE Transactions on Software Engineering, 23(5):279--295, May 1997.

Digital Library

[15]

P. Joshi, M. Naik, C.-S. Park, and K. Sen. Calfuzzer: An extensible active testing framework for concurrent programs. In Proceedings of the 21st International Conference on Computer Aided Verification (CAV '09), pages 675--681, Berlin, Heidelberg, 2009. Springer-Verlag.

Digital Library

[16]

A first look at jsr 166: Concurrency utilities http://today.java.net/pub/a/today/2004/03/01/jsr166.html.

[17]

R. E. Korf, W. Zhang, I. Thayer, and H. Hohwald. Frontier search. Journal of the ACM, 52(5):715--748, 2005.

Digital Library

[18]

D. Leijen, W. Schulte, and S. Burckhardt. The design of a task parallel library. In OOPSLA, page to appear, 2009.

Digital Library

[19]

M. Musuvathi and S. Qadeer. Iterative context bounding for systematic testing of multithreaded programs. In Programming Language Design and Implementation (PLDI '07), pages 446--455, 2007.

Digital Library

[20]

M. Musuvathi, S. Qadeer, T. Ball, G. Basler, A. Nainar, and I. Neamtiu. Finding and reproducing heisenbugs in concurrent programs. In 8th USENIX Symposium on Operating Systems Design and Implementation, 2009.

Digital Library

[21]

W. T. Overman. Verification of concurrent systems: function and timing. PhD thesis, 1981.

Digital Library

[22]

S. Park, S. Lu, and Y. Zhou. Ctrigger: exposing atomicity violation bugs from their hiding places. In ASPLOS, pages 25--36, 2009.

Digital Library

[23]

J. Pearl. Heuristics: Intelligent Search Strategies for Computer Problem Solving. Addison-Wesley, 1984.

Digital Library

[24]

J.-P. Queille and J. Sifakis. Specification and verification of concurrent systems in cesar. In The Fifth International Symposium on Programming, pages 337--351, London, UK, 1982. Springer-Verlag.

Digital Library

[25]

J. Reinders. Intel Threading Building Blocks : Outfitting C++ for Multi-core Processor Parallelism. O'Reilly, 2007.

Digital Library

[26]

N. Rungta and E. G. Mercer. Guided model checking for programs with polymorphism.In Proceedings of the 2009 ACM SIGPLAN workshop on Partial evaluation and program manipulation (PEPM '09), pages 21--30, New York, NY, USA, 2009. ACM.

Digital Library

[27]

S. J. Russell and P. Norvig. Artificial intelligence: a modern approach. Prentice Hall, 2nd edition, 2003.

Digital Library

[28]

K. Sen. Effective random testing of concurrent programs. In ASE, pages 323--332, 2007.

Digital Library

[29]

K. Sen. Race directed random testing of concurrent programs. In PLDI, pages 11--21, 2008.

Digital Library

[30]

Optimize managed code for multi-core machines - http://msdn.microsoft.com/en-us/library/bb648752.aspx.

[31]

A. Valmari. Stubborn sets for reduced state space generation. In The 10th International Conference on Applications and Theory of Petri Nets, pages 491--515, London, UK, 1991. Springer-Verlag.

Digital Library

[32]

W. Visser, K. Havelund, G. Brat, and S. Park. Java PathFinder - second generation of a Java model checker. In Proceedings of Post- CAV Workshop on Advances in Verification, July 2000.

[33]

C. H. Yang and D. L. Dill. Validation with guided search of the state space. In DAC '98, pages 599--604, 1998.

Digital Library

Cited By

Wang YGao FWang LYu TZhao JLi X(2022)Automatic Detection, Validation, and Repair of Race Conditions in Interrupt-Driven Embedded SoftwareIEEE Transactions on Software Engineering10.1109/TSE.2020.298917148:1(346-363)Online publication date: 1-Jan-2022
https://doi.org/10.1109/TSE.2020.2989171
Mu YWang ZLiu SSun JChen JChen X(2021)HARS: Heuristic-Enhanced Adaptive Randomized Scheduling for Concurrency Testing2021 IEEE 21st International Conference on Software Quality, Reliability and Security (QRS)10.1109/QRS54544.2021.00033(219-230)Online publication date: Dec-2021
https://doi.org/10.1109/QRS54544.2021.00033
Joost Slob FJongmans S(2021)Prut4j: Protocol Unit Testing fo(u)r Java2021 14th IEEE Conference on Software Testing, Verification and Validation (ICST)10.1109/ICST49551.2021.00058(448-453)Online publication date: Apr-2021
https://doi.org/10.1109/ICST49551.2021.00058
Show More Cited By

Recommendations

GAMBIT: effective unit testing for concurrency libraries
PPoPP '10

As concurrent programming becomes prevalent, software providers are investing in concurrency libraries to improve programmer productivity. Concurrency libraries improve productivity by hiding error-prone, low-level synchronization from programmers and ...
Iterative context bounding for systematic testing of multithreaded programs
PLDI '07: Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation

Multithreaded programs are difficult to get right because of unexpected interaction between concurrently executing threads. Traditional testing methods are inadequate for catching subtle concurrency errors which manifest themselves late in the ...
Iterative context bounding for systematic testing of multithreaded programs
Proceedings of the 2007 PLDI conference

Multithreaded programs are difficult to get right because of unexpected interaction between concurrently executing threads. Traditional testing methods are inadequate for catching subtle concurrency errors which manifest themselves late in the ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

PPoPP '10: Proceedings of the 15th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming

January 2010

372 pages

ISBN:9781605588773

DOI:10.1145/1693453

General Chairs:
R. Govindarajan
Indian Institute of Science
,
David Padua
UIUC
,
Program Chair:
Mary Hall
University of Utah

ACM SIGPLAN Notices Volume 45, Issue 5
PPoPP '10
May 2010
346 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/1837853
Issue’s Table of Contents

Copyright © 2010 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]

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 09 January 2010

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

PPoPP '10

Sponsor:

SIGPLAN

PPoPP '10: ACM SIGPLAN Principles and Practice of Parallel Computing

January 9 - 14, 2010

Bangalore, India

Acceptance Rates

Overall Acceptance Rate 230 of 1,014 submissions, 23%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

46
Total Citations
View Citations
488
Total Downloads

Downloads (Last 12 months)11
Downloads (Last 6 weeks)1

Reflects downloads up to 13 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Wang YGao FWang LYu TZhao JLi X(2022)Automatic Detection, Validation, and Repair of Race Conditions in Interrupt-Driven Embedded SoftwareIEEE Transactions on Software Engineering10.1109/TSE.2020.298917148:1(346-363)Online publication date: 1-Jan-2022
https://doi.org/10.1109/TSE.2020.2989171
Mu YWang ZLiu SSun JChen JChen X(2021)HARS: Heuristic-Enhanced Adaptive Randomized Scheduling for Concurrency Testing2021 IEEE 21st International Conference on Software Quality, Reliability and Security (QRS)10.1109/QRS54544.2021.00033(219-230)Online publication date: Dec-2021
https://doi.org/10.1109/QRS54544.2021.00033
Joost Slob FJongmans S(2021)Prut4j: Protocol Unit Testing fo(u)r Java2021 14th IEEE Conference on Software Testing, Verification and Validation (ICST)10.1109/ICST49551.2021.00058(448-453)Online publication date: Apr-2021
https://doi.org/10.1109/ICST49551.2021.00058
Yu THuang ZWang C(2020) ConTesa : Directed Test Suite Augmentation for Concurrent Software IEEE Transactions on Software Engineering10.1109/TSE.2018.286139246:4(405-419)Online publication date: 1-Apr-2020
https://doi.org/10.1109/TSE.2018.2861392
Lukman JKe HStuardo CSuminto RKurniawan DSimon DPriambada STian CYe FLeesatapornwongsa TGupta ALu SGunawi H(2019)FlyMCProceedings of the Fourteenth EuroSys Conference 201910.1145/3302424.3303986(1-16)Online publication date: 25-Mar-2019
https://dl.acm.org/doi/10.1145/3302424.3303986
Jongmans S(2019)Toward New Unit-Testing Techniques for Shared-Memory Concurrent Programs2019 24th International Conference on Engineering of Complex Computer Systems (ICECCS)10.1109/ICECCS.2019.00025(164-169)Online publication date: Nov-2019
https://doi.org/10.1109/ICECCS.2019.00025
Parízek PLhoták O(2019)Fast detection of concurrency errors by state space traversal with randomization and early backtrackingInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-018-0484-721:4(365-400)Online publication date: 1-Aug-2019
https://dl.acm.org/doi/10.1007/s10009-018-0484-7
Bianchi FMargara APezze M(2018)A Survey of Recent Trends in Testing Concurrent Software SystemsIEEE Transactions on Software Engineering10.1109/TSE.2017.270708944:8(747-783)Online publication date: 1-Aug-2018
https://dl.acm.org/doi/10.1109/TSE.2017.2707089
Yu TPradel M(2018)Pinpointing and repairing performance bottlenecks in concurrent programsEmpirical Software Engineering10.1007/s10664-017-9578-123:5(3034-3071)Online publication date: 1-Oct-2018
https://dl.acm.org/doi/10.1007/s10664-017-9578-1
Ou PDemsky B(2017)Checking Concurrent Data Structures Under the C/C++11 Memory ModelACM SIGPLAN Notices10.1145/3155284.301874952:8(45-59)Online publication date: 26-Jan-2017
https://dl.acm.org/doi/10.1145/3155284.3018749
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 Table of Contents