research-article

Underspecified harnesses and interleaved bugs

Authors:

Shuvendu K. Lahiri,

Akash LalAuthors Info & Claims

ACM SIGPLAN Notices, Volume 47, Issue 1

Pages 19 - 30

https://doi.org/10.1145/2103621.2103662

Published: 25 January 2012 Publication History

Abstract

Static assertion checking of open programs requires setting up a precise harness to capture the environment assumptions. For instance, a library may require a file handle to be properly initialized before it is passed into it. A harness is used to set up or specify the appropriate preconditions before invoking methods from the program. In the absence of a precise harness, even the most precise automated static checkers are bound to report numerous false alarms. This often limits the adoption of static assertion checking in the hands of a user.

In this work, we explore the possibility of automatically filtering away (or prioritizing) warnings that result from imprecision in the harness. We limit our attention to the scenario when one is interested in finding bugs due to concurrency. We define a warning to be an interleaved bug when it manifests on an input for which no sequential interleaving produces a warning. As we argue in the paper, limiting a static analysis to only consider interleaved bugs greatly reduces false positives during static concurrency analysis in the presence of an imprecise harness.

We formalize interleaved bugs as a differential analysis between the original program and its sequential version and provide various techniques for finding them. Our implementation CBugs demonstrates that the scheme of finding interleaved bugs can alleviate the need to construct precise harnesses while checking real-life concurrent programs.

Supplementary Material

JPG File (popl_1a_2.jpg)

Download
15.21 KB

MP4 File (popl_1a_2.mp4)

Download
208.19 MB

References

[1]

R. Alur, P. Cerný, P. Madhusudan, and W. Nam. Synthesis of interface specifications for java classes. In Principles of Programming Languages (POPL '05), pages 98--109, 2005.

Digital Library

[2]

M. Barnett and K. R. M. Leino. Weakest-precondition of unstructured programs. In Program Analysis For Software Tools and Engineering (PASTE '05), pages 82--87, 2005.

Digital Library

[3]

E. Börger, E. Gradel, and Y. Gurevich. The Classical Decision Problem. Springer-Verlag, 1997.

[4]

S. Burckhardt, C. Dern, M. Musuvathi, and R. Tan. Line-up: a complete and automatic linearizability checker. In Programming Language Design and Implementation (PLDI '10), pages 330--340, 2010.

Digital Library

[5]

J. Burnim, T. Elmas, G. C. Necula, and K. Sen. Ndseq: runtime checking for nondeterministic sequential specifications of parallel correctness. In Programming Language Design and Implementation (PLDI '11), pages 401--414, 2011.

Digital Library

[6]

L. Cordeiro and B. Fischer. Verifying multi-threaded software using smt-based context-bounded model checking. In International Conference on Software Engineering (ICSE '11), pages 331--340, 2011.

Digital Library

[7]

D. Detlefs, G. Nelson, and J. B. Saxe. Simplify: a theorem prover for program checking. J. ACM, 52(3):365--473, 2005.

Digital Library

[8]

E. W. Dijkstra. Guarded commands, nondeterminacy and formal derivation of programs. Communications of the ACM, 18:453--457, 1975.

Digital Library

[9]

I. Dillig, T. Dillig, and A. Aiken. Static error detection using semantic inconsistency inference. In Programming Language Design and Implementation (PLDI '07), pages 435--445, 2007.

Digital Library

[10]

M. Emmi, S. Qadeer, and Z. Rakamaric. Delay-bounded scheduling. In Principles of Programming Languages, pages 411--422, 2011.

Digital Library

[11]

D. R. Engler, D. Y. Chen, and A. Chou. Bugs as inconsistent behavior: A general approach to inferring errors in systems code. In Symposium on Operating Systems Principles (SOSP '01), pages 57--72, 2001.

Digital Library

[12]

M. Herlihy and J. M. Wing. Linearizability: A correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst., 12(3):463--492, 1990.

Digital Library

[13]

R. Jhala and R. Majumdar. Interprocedural analysis of asynchronous programs. In Principles of Programming Languages, pages 339--350, 2007.

Digital Library

[14]

T. Kremenek and D. R. Engler. Z-ranking: Using statistical analysis to counter the impact of static analysis approximations. In Static Analysis Symposium (SAS '03), LNCS 2694, pages 295--315, 2003.

Digital Library

[15]

S. Lahiri, S. Qadeer, and Z. Rakamaric. Static and precise detection of concurrency errors in systems code using SMT solvers. In Computer Aided Verification, 2009.

Digital Library

[16]

K. R. M. Leino, T. D. Millstein, and J. B. Saxe. Generating error traces from verification-condition counterexamples. Sci. Comput. Program., 55(1--3):209--226, 2005.

Digital Library

[17]

Poirot: The Concurrency Sleuth. http://research.microsoft.com/en-us/projects/poirot/.

[18]

K. Sen and M. Viswanathan. Model checking multithreaded programs with asynchronous atomic methods. In Computer Aided Verification, pages 300--314, 2006.

Digital Library

[19]

S. F. Siegel, A. Mironova, G. S. Avrunin, and L. A. Clarke. Using model checking with symbolic execution to verify parallel numerical programs. In International Symposium on Software Testing and Analysis (ISSTA '06), pages 157--168, 2006.

Digital Library

[20]

O. Tkachuk, M. B. Dwyer, and C. S. Pasareanu. Automated environment generation for software model checking. In Automated Software Engineering (ASE '03), pages 116--129, 2003.

Digital Library

[21]

J. W. Voung, R. Jhala, and S. Lerner. Relay: static race detection on millions of lines of code. In Symposium on Foundations of Software Engineering (ESEC/SIGSOFT FSE '07), pages 205--214, 2007.

Digital Library

[22]

Microsoft windows driver kit (WDK). http://www.microsoft.com/whdc/devtools/ddk/default.mspx.

Cited By

Muske TSerebrenik A(2023)Survey of Approaches for Postprocessing of Static Analysis AlarmsACM Computing Surveys10.1145/349452155:3(1-39)Online publication date: 30-Apr-2023
https://dl.acm.org/doi/10.1145/3494521
Das ALahiri SLal ALi Y(2015)Angelic Verification: Precise Verification Modulo UnknownsComputer Aided Verification10.1007/978-3-319-21690-4_19(324-342)Online publication date: 16-Jul-2015
https://doi.org/10.1007/978-3-319-21690-4_19
Sliwa JJoffe E(2014)Ethics between the lines (of code)Proceedings of the IEEE 2014 International Symposium on Ethics in Engineering, Science, and Technology10.5555/2960587.2960692(1-7)Online publication date: 23-May-2014
https://dl.acm.org/doi/10.5555/2960587.2960692
Show More Cited By

Index Terms

Underspecified harnesses and interleaved bugs

Recommendations

Underspecified harnesses and interleaved bugs
POPL '12: Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Static assertion checking of open programs requires setting up a precise harness to capture the environment assumptions. For instance, a library may require a file handle to be properly initialized before it is passed into it. A harness is used to set ...
Modular verification of concurrent assembly code with dynamic thread creation and termination
ICFP '05: Proceedings of the tenth ACM SIGPLAN international conference on Functional programming

Proof-carrying code (PCC) is a general framework that can, in principle, verify safety properties of arbitrary machine-language programs. Existing PCC systems and typed assembly languages, however, can only handle sequential programs. This severely ...
Modular verification of concurrent assembly code with dynamic thread creation and termination
Proceedings of the tenth ACM SIGPLAN international conference on Functional programming

Proof-carrying code (PCC) is a general framework that can, in principle, verify safety properties of arbitrary machine-language programs. Existing PCC systems and typed assembly languages, however, can only handle sequential programs. This severely ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 47, Issue 1

POPL '12

January 2012

569 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/2103621

Issue’s Table of Contents

POPL '12: Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages
January 2012
602 pages
ISBN:9781450310833
DOI:10.1145/2103656
General Chair:
John Field
Google, USA
,
Program Chair:
Michael Hicks
University of Maryland, College Park, USA

Copyright © 2012 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: 25 January 2012

Published in SIGPLAN Volume 47, Issue 1

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

36
Total Citations
View Citations
517
Total Downloads

Downloads (Last 12 months)22
Downloads (Last 6 weeks)2

Reflects downloads up to 20 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Muske TSerebrenik A(2023)Survey of Approaches for Postprocessing of Static Analysis AlarmsACM Computing Surveys10.1145/349452155:3(1-39)Online publication date: 30-Apr-2023
https://dl.acm.org/doi/10.1145/3494521
Das ALahiri SLal ALi Y(2015)Angelic Verification: Precise Verification Modulo UnknownsComputer Aided Verification10.1007/978-3-319-21690-4_19(324-342)Online publication date: 16-Jul-2015
https://doi.org/10.1007/978-3-319-21690-4_19
Sliwa JJoffe E(2014)Ethics between the lines (of code)Proceedings of the IEEE 2014 International Symposium on Ethics in Engineering, Science, and Technology10.5555/2960587.2960692(1-7)Online publication date: 23-May-2014
https://dl.acm.org/doi/10.5555/2960587.2960692
Chen CLu KWang XZhou XFang L(2013)Pruning False Positives of Static Data-Race Detection via Thread SpecializationRevised Selected Papers of the 10th International Symposium on Advanced Parallel Processing Technologies - Volume 829910.1007/978-3-642-45293-2_6(77-90)Online publication date: 27-Aug-2013
https://dl.acm.org/doi/10.1007/978-3-642-45293-2_6
He YWu WChen Y(2012)An efficient method for detecting concurrency errors in object-oriented programsScience China Information Sciences10.1007/s11432-012-4751-z55:12(2774-2784)Online publication date: 29-Dec-2012
https://doi.org/10.1007/s11432-012-4751-z
Razavi NIvančić FKahlon VGupta A(2012)Concurrent Test Generation Using Concolic Multi-trace AnalysisProgramming Languages and Systems10.1007/978-3-642-35182-2_17(239-255)Online publication date: 2012
https://doi.org/10.1007/978-3-642-35182-2_17
Giannakopoulou DRakamarić ZRaman V(2012)Symbolic learning of component interfacesProceedings of the 19th international conference on Static Analysis10.1007/978-3-642-33125-1_18(248-264)Online publication date: 11-Sep-2012
https://dl.acm.org/doi/10.1007/978-3-642-33125-1_18
Muduli SPadulkar RRoy S(2024)Interactive Theorem Proving Modulo FuzzingComputer Aided Verification10.1007/978-3-031-65627-9_24(480-493)Online publication date: 24-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-65627-9_24
Guo ZTan TLiu SLiu XLai WYang YLi YChen LDong WZhou Y(2023)Mitigating False Positive Static Analysis Warnings: Progress, Challenges, and OpportunitiesIEEE Transactions on Software Engineering10.1109/TSE.2023.332966749:12(5154-5188)Online publication date: 1-Dec-2023
https://dl.acm.org/doi/10.1109/TSE.2023.3329667
Muduli SRoy S(2022)Satisfiability modulo fuzzing: a synergistic combination of SMT solving and fuzzingProceedings of the ACM on Programming Languages10.1145/35633326:OOPSLA2(1236-1263)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563332
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 Issue’s Table of Contents