More Web Proxy on the site http://driver.im/

research-article

Variable and thread bounding for systematic testing of multithreaded programs

Authors:

Sandeep Bindal,

Akash LalAuthors Info & Claims

ISSTA 2013: Proceedings of the 2013 International Symposium on Software Testing and Analysis

Pages 145 - 155

https://doi.org/10.1145/2483760.2483764

Published: 15 July 2013 Publication History

Abstract

Previous approaches to systematic state-space exploration for testing multi-threaded programs have proposed context-bounding and depth-bounding to be effective ranking algorithms for testing multithreaded programs. This paper proposes two new metrics to rank thread schedules for systematic state-space exploration. Our metrics are based on characterization of a concurrency bug using v (the minimum number of distinct variables that need to be involved for the bug to manifest) and t (the minimum number of distinct threads among which scheduling constraints are required to manifest the bug). Our algorithm is based on the hypothesis that in practice, most concurrency bugs have low v (typically 1-2) and low t (typically 2-4) characteristics. We iteratively explore the search space of schedules in increasing orders of v and t. We show qualitatively and empirically that our algorithm finds common bugs in fewer number of execution runs, compared with previous approaches. We also show that using v and t improves the lower bounds on the probability of finding bugs through randomized algorithms. Systematic exploration of schedules requires instrumenting each variable access made by a program, which can be very expensive and severely limits the applicability of this approach. Previous work has avoided this problem by interposing only on synchronization operations (and ignoring other variable accesses). We demonstrate that by using variable bounding (v) and a static imprecise alias analysis, we can interpose on all variable accesses (and not just synchronization operations) at 10-100x less overhead than previous approaches.

References

[1]

L. O. Andersen. Program analysis and specialization for the C programming language. Technical report, 1994.

[2]

K. R. Apt, N. Francez, and S. Katz. Appraising fairness in distributed languages. In POPL ’87.

Digital Library

[3]

A. Bessey, K. Block, B. Chelf, A. Chou, B. Fulton, S. Hallem, C. Henri-Gros, A. Kamsky, S. McPeak, and D. Engler. A few billion lines of code later: using static analysis to find bugs in the real world. Commun. ACM, 53:66–75, February 2010.

Digital Library

[4]

S. Bindal, S. Bansal, and A. Lal. Variable and thread bounding for systematic testing of multithreaded programs. Technical report, IIT Delhi, 2012. http://arxiv.org/abs/1207.2544.

[5]

D. Bruening and J. Chapin. Systematic testing of multithreaded programs. Technical report, LCS-TM-607, MIT/LCS, 2000.

[6]

S. Burckhardt, P. Kothari, M. Musuvathi, and S. Nagarakatte. A randomized scheduler with probabilistic guarantees of finding bugs. In ASPLOS ’10.

Digital Library

[7]

S. Chiba. Javassist — a reflection-based programming wizard for java. In OOPSLA ’98.

[8]

T. Elmas, S. Qadeer, and S. Tasiran. Goldilocks: a race and transactionaware java runtime. In PLDI ’07.

Digital Library

[9]

M. Emmi, S. Qadeer, and Z. Rakamaric. Delay-bounded scheduling. In POPL, pages 411–422, 2011.

Digital Library

[10]

Y. Eytani, K. Havelund, S. D. Stoller, and S. Ur. Toward a framework and benchmark for testing tools for multi-threaded programs. Concurrency and Computation: Practice & Experience, 19(3):267––279, 2007.

Digital Library

[11]

P. Godefroid. Model checking for programming languages using VeriSoft. In POPL ’97.

Digital Library

[12]

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.

Digital Library

[13]

P. Godefroid, R. S. Hanmer, and L. J. Jagadeesan. Model checking without a model: an analysis of the heart-beat monitor of a telephone switch using VeriSoft. In ISSTA ’98.

Digital Library

[14]

P. Joshi, C.-S. Park, K. Sen, and M. Naik. A randomized dynamic program analysis technique for detecting real deadlocks. In PLDI ’09.

Digital Library

[15]

S. Khurshid, C. S. Păsăreanu, and W. Visser. Generalized symbolic execution for model checking and testing. In TACAS’03.

Digital Library

[16]

O. Lhoták and L. Hendren. Evaluating the benefits of contextsensitive points-to analysis using a bdd-based implementation. ACM Trans. Softw. Eng. Methodol., 18:3:1–3:53, October 2008.

Digital Library

[17]

S. Lu, S. Park, E. Seo, and Y. Zhou. Learning from mistakes: a comprehensive study on real world concurrency bug characteristics. In ASPLOS ’08.

Digital Library

[18]

S. Lu, J. Tucek, F. Qin, and Y. Zhou. Avio: detecting atomicity violations via access interleaving invariants. In ASPLOS ’06.

Digital Library

[19]

D. Marino, M. Musuvathi, and S. Narayanasamy. Literace: effective sampling for lightweight data-race detection. In PLDI ’09.

Digital Library

[20]

M. Musuvathi and S. Qadeer. Iterative context bounding for systematic testing of multithreaded programs. In PLDI ’07.

Digital Library

[21]

M. Musuvathi, S. Qadeer, T. Ball, G. Basler, P. A. Nainar, and I. Neamtiu. In OSDI ’08.

[22]

M. Naik, A. Aiken, and J. Whaley. Effective static race detection for java. In PLDI ’06.

Digital Library

[23]

S. Park, S. Lu, and Y. Zhou. CTrigger: Exposing atomicity violation bugs from their hiding places. In ASPLOS ’09.

Digital Library

[24]

S. Savage, M. Burrows, G. Nelson, P. Sobalvarro, and T. Anderson. Eraser: a dynamic data race detector for multithreaded programs. ACM Trans. Comput. Syst., 15:391–411, November 1997.

Digital Library

[25]

K. Sen. Race directed random testing of concurrent programs. In PLDI ’08.

Digital Library

[26]

S. D. Stoller. Model-checking multi-threaded distributed java programs. In SPIN Workshop on Model Checking and Software Verification, 2000.

Digital Library

[27]

J. Whaley and M. S. Lam. Cloning-based context-sensitive pointer alias analysis using binary decision diagrams. In PLDI ’04.

Digital Library

[28]

W. Xiong, S. Park, J. Zhang, Y. Zhou, and Z. Ma. Ad hoc synchronization considered harmful. In OSDI ’10.

Digital Library

[29]

Y. Yu, T. Rodeheffer, and W. Chen. Racetrack: efficient detection of data race conditions via adaptive tracking. In SOSP ’05.

Digital Library

Cited By

Guo JLi ZShi CZhao R(2020)Thread Scheduling Sequence Generation Based on All Synchronization Pair Coverage CriteriaInternational Journal of Software Engineering and Knowledge Engineering10.1142/S021819402050005930:01(97-118)Online publication date: 27-Feb-2020
https://doi.org/10.1142/S0218194020500059
Wang TYu XQiu ZJin GMueller F(2020)BarrierFinder: recognizing ad hoc barriersEmpirical Software Engineering10.1007/s10664-020-09862-3Online publication date: 1-Sep-2020
https://doi.org/10.1007/s10664-020-09862-3
Sung CLahiri SEnea CWang CHuchard MKästner CFraser G(2018)Datalog-based scalable semantic diffing of concurrent programsProceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering10.1145/3238147.3238211(656-666)Online publication date: 3-Sep-2018
https://dl.acm.org/doi/10.1145/3238147.3238211
Show More Cited By

Index Terms

Variable and thread bounding for systematic testing of multithreaded programs

Recommendations

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 ...
Testing multithreaded programs via thread speed control
ESEC/FSE 2018: Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering

A multithreaded program's interleaving space is discrete and astronomically large, making effectively sampling thread schedules for manifesting concurrency bugs a challenging task. Observing that concurrency bugs can be manifested by adjusting thread ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ISSTA 2013: Proceedings of the 2013 International Symposium on Software Testing and Analysis

July 2013

381 pages

ISBN:9781450321594

DOI:10.1145/2483760

General Chair:
Mauro Pezzè,
Program Chair:
Mark Harman

Copyright © 2013 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 the author(s) 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

SIGSOFT: ACM Special Interest Group on Software Engineering

In-Cooperation

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 15 July 2013

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

ISSTA '13

Sponsor:

SIGSOFT

ISSTA '13: Iitsnternational Symposium on Software Testing and Analysis

July 15 - 20, 2013

Lugano, Switzerland

Acceptance Rates

Overall Acceptance Rate 58 of 213 submissions, 27%

Upcoming Conference

ISSTA '25

Sponsor:
sigsoft

34th ACM SIGSOFT International Symposium on Software Testing and Analysis

June 25 - 28, 2025

Trondheim , Norway

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

14
Total Citations
View Citations
218
Total Downloads

Downloads (Last 12 months)4
Downloads (Last 6 weeks)0

Reflects downloads up to 10 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Guo JLi ZShi CZhao R(2020)Thread Scheduling Sequence Generation Based on All Synchronization Pair Coverage CriteriaInternational Journal of Software Engineering and Knowledge Engineering10.1142/S021819402050005930:01(97-118)Online publication date: 27-Feb-2020
https://doi.org/10.1142/S0218194020500059
Wang TYu XQiu ZJin GMueller F(2020)BarrierFinder: recognizing ad hoc barriersEmpirical Software Engineering10.1007/s10664-020-09862-3Online publication date: 1-Sep-2020
https://doi.org/10.1007/s10664-020-09862-3
Sung CLahiri SEnea CWang CHuchard MKästner CFraser G(2018)Datalog-based scalable semantic diffing of concurrent programsProceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering10.1145/3238147.3238211(656-666)Online publication date: 3-Sep-2018
https://dl.acm.org/doi/10.1145/3238147.3238211
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 TSrisa-an WRothermel G(2017)An automated framework to support testing for process‐level race conditionsSoftware Testing, Verification and Reliability10.1002/stvr.163427:4-5Online publication date: 10-May-2017
https://doi.org/10.1002/stvr.1634
Banga PPai ARoy SChaudhuri MTalpin J(2016)Accelerating schedule space exploration of multi-threaded programs with GPUsProceedings of the 14th ACM-IEEE International Conference on Formal Methods and Models for System Design10.5555/3343414.3343430(115-124)Online publication date: 18-Nov-2016
https://dl.acm.org/doi/10.5555/3343414.3343430
Banga PPai ARoy SChaudhuri M(2016)Accelerating schedule space exploration of multi-threaded programs with GPUs2016 ACM/IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE)10.1109/MEMCOD.2016.7797754(115-124)Online publication date: Nov-2016
https://doi.org/10.1109/MEMCOD.2016.7797754
Abdulla PAtig MDiep B(2016)Counter-Example Guided Program VerificationFM 2016: Formal Methods10.1007/978-3-319-48989-6_2(25-42)Online publication date: 8-Nov-2016
https://doi.org/10.1007/978-3-319-48989-6_2
Kusano MChattopadhyay AWang CBertolino ACanfora GElbaum S(2015)Dynamic generation of likely invariants for multithreaded programsProceedings of the 37th International Conference on Software Engineering - Volume 110.5555/2818754.2818855(835-846)Online publication date: 16-May-2015
https://dl.acm.org/doi/10.5555/2818754.2818855
Cai YCao LDi Nitto EHarman MHeymans P(2015)Effective and precise dynamic detection of hidden races for Java programsProceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering10.1145/2786805.2786839(450-461)Online publication date: 30-Aug-2015
https://dl.acm.org/doi/10.1145/2786805.2786839
Show More Cited By

View Options

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