skip to main content
10.1145/2790449.2790530acmotherconferencesArticle/Chapter ViewAbstractPublication PagesppdpConference Proceedingsconference-collections
research-article

Detecting concurrency bugs in higher-order programs through abstract interpretation

Published: 14 July 2015 Publication History

Abstract

Manually detecting bugs in concurrent programs is hard due to the myriad of thread interleavings that needs to be accounted for. Higher-order programming features only exacerbate this difficulty. The need for tool support therefore increases as these features become more widespread. We investigate the P(CEK*)S abstract machine as the foundation for tool support for detecting concurrency bugs. This abstract interpreter analyzes multi-threaded, higher-order programs with shared-store concurrency and a compare-and-swap synchronization primitive. In this paper, we evaluate two different approaches to reduce the size of the state space explored by the abstract interpreter. First, we integrate abstract garbage collection into the abstract interpreter, and we observe that it does not reduce the state space as expected. We then evaluate the impact of adding first-class support for locks on the machine's client analyses. To this end, we compare a cas-based and a lock-based formulation of race condition and deadlock detection analyses. We show that adding first-class support for locks not only significantly reduces the number of abstract program states that need to be explored, but also simplifies formulating the client analyses.

References

[1]
M. Abadi, C. Flanagan, and S. N. Freund. Types for safe locking: Static race detection for Java. ACM Transactions on Programming Languages and Systems (TOPLAS), 28(2):207--255, 2006.
[2]
C. Artho and A. Biere. Applying static analysis to large-scale, multi-threaded Java programs. In Software Engineering Conference, 2001. Proceedings. 2001 Australian, pages 68--75. IEEE, 2001.
[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. Communications of the ACM, 53(2):66--75, 2010.
[4]
A. Biere, A. Cimatti, E. M. Clarke, O. Strichman, and Y. Zhu. Bounded model checking. Advances in computers, 58:117--148, 2003.
[5]
C. Boyapati. Safejava: a unified type system for safe programming. PhD thesis, Massachusetts Institute of Technology, 2004.
[6]
C. Boyapati and M. Rinard. A parameterized type system for race-free Java programs. In ACM SIGPLAN Notices, volume 36, pages 56--69. ACM, 2001.
[7]
C. Boyapati, R. Lee, and M. Rinard. Ownership types for safe programming: Preventing data races and deadlocks. In ACM SIGPLAN Notices, volume 37, pages 211--230. ACM, 2002.
[8]
J. Burch, E. M. Clarke, and D. Long. Symbolic model checking with partitioned transition relations. Computer Science Department, page 435, 1991.
[9]
J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L.-J. Hwang. Symbolic model checking: 1020 states and beyond. In Logic in Computer Science, 1990. LICS'90, Proceedings., Fifth Annual IEEE Symposium on e, pages 428--439. IEEE, 1990.
[10]
E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Progress on the state explosion problem in model checking. In Informatics, pages 176--194. Springer, 2001.
[11]
J. C. Corbett, M. B. Dwyer, J. Hatcliff, S. Laubach, C. S. Pasareanu, H. Zheng, et al. Bandera: Extracting finite-state models from Java source code. In Software Engineering, 2000. Proceedings of the 2000 International Conference on, pages 439--448. IEEE, 2000.
[12]
C. Earl, I. Sergey, M. Might, and D. Van Horn. Introspective pushdown analysis of higher-order programs. In Proceedings of the 17th ACM SIGPLAN international conference on Functional programming, pages 177--188. ACM, 2012.
[13]
D. Engler and K. Ashcraft. Racerx: effective, static detection of race conditions and deadlocks. In ACM SIGOPS Operating Systems Review, volume 37, pages 237--252. ACM, 2003.
[14]
C. Flanagan and M. Abadi. Types for safe locking. In Programming Languages and Systems, pages 91--108. Springer, 1999.
[15]
C. Flanagan and S. N. Freund. Type-based race detection for Java. In ACM SIGPLAN Notices, volume 35, pages 219--232. ACM, 2000.
[16]
C. Flanagan, A. Sabry, B. F. Duba, and M. Felleisen. The essence of compiling with continuations. In ACM Sigplan Notices, volume 28, pages 237--247. ACM, 1993.
[17]
L.-Å. Fredlund and H. Svensson. Mcerlang: a model checker for a distributed functional programming language. In ACM SIGPLAN Notices, volume 42, pages 125--136. ACM, 2007.
[18]
P. Godefroid. Model checking for programming languages using verisoft. In Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 174--186. ACM, 1997.
[19]
G. Gueta, C. Flanagan, E. Yahav, and M. Sagiv. Cartesian partial-order reduction. Model Checking Software, page 95, 2007.
[20]
K. Havelund and T. Pressburger. Model checking Java programs using Java PathFinder. International Journal on Software Tools for Technology Transfer, 2(4):366--381, 2000.
[21]
G. J. Holzmann. The SPIN model checker: Primer and reference manual, volume 1003. Addison-Wesley Reading, 2004.
[22]
S. Jagannathan. Locality abstractions for parallel and distributed computing. In Theory and Practice of Parallel Programming, pages 320--345. Springer, 1995.
[23]
S. Jagannathan and S. Weeks. Analyzing stores and references in a parallel symbolic language. In ACM SIGPLAN Lisp Pointers, volume 7, pages 294--305. ACM, 1994.
[24]
J. I. Johnson and D. Van Horn. Abstracting abstract control. In Proceedings of the 10th ACM Symposium on Dynamic languages, pages 11--22. ACM, 2014.
[25]
S. Lu, S. Park, E. Seo, and Y. Zhou. Learning from mistakes: a comprehensive study on real world concurrency bug characteristics. In ACM Sigplan Notices, volume 43, pages 329--339. ACM, 2008.
[26]
M. Might and O. Shivers. Improving flow analyses via γcfa: abstract garbage collection and counting. ACM SIGPLAN Notices, 41(9):13--25, 2006.
[27]
M. Might and D. Van Horn. A family of abstract interpretations for static analysis of concurrent higher-order programs. In Static Analysis, pages 180--197. Springer, 2011.
[28]
M. Naik, A. Aiken, and J. Whaley. Effective static race detection for Java, volume 41. ACM, 2006.
[29]
M. Naik, C.-S. Park, K. Sen, and D. Gay. Effective static deadlock detection. In Proceedings of the 31st International Conference on Software Engineering, pages 386--396. IEEE Computer Society, 2009.
[30]
D. Peled. Ten years of partial order reduction. In Computer Aided Verification, pages 17--28. Springer, 1998.
[31]
A. Sasturkar, R. Agarwal, L. Wang, and S. D. Stoller. Automated type-based analysis of data races and atomicity. In Proceedings of the tenth ACM SIGPLAN symposium on Principles and practice of parallel programming, pages 83--94. ACM, 2005.
[32]
D. Schmidt and B. Steffen. Program analysis as model checking of abstract interpretations. In Static Analysis, pages 351--380. Springer, 1998.
[33]
D. Van Horn and M. Might. Abstracting abstract machines. In ACM Sigplan Notices, volume 45, pages 51--62. ACM, 2010.
[34]
C. von Praun. Detecting synchronization defects in multi-threaded object-oriented programs. PhD thesis, Swiss Federal Institute of Technology, Zurich, 2004.
[35]
S. Weeks, S. Jagannathan, and J. Philbin. A concurrent abstract interpreter. Lisp and Symbolic Computation, 7(2-3):173--193, 1994.
[36]
A. Williams, W. Thies, and M. D. Ernst. Static deadlock detection for Java libraries. In ECOOP 2005-Object-Oriented Programming, pages 602--629. Springer, 2005.

Cited By

View all
  • (2023)Result Invalidation for Incremental Modular AnalysesVerification, Model Checking, and Abstract Interpretation10.1007/978-3-031-24950-1_14(296-319)Online publication date: 17-Jan-2023
  • (2022)Combining BMC and Fuzzing Techniques for Finding Software Vulnerabilities in Concurrent ProgramsIEEE Access10.1109/ACCESS.2022.322335910(121365-121384)Online publication date: 2022
  • (2019)Effect-Driven Flow AnalysisVerification, Model Checking, and Abstract Interpretation10.1007/978-3-030-11245-5_12(247-274)Online publication date: 11-Jan-2019
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Other conferences
PPDP '15: Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming
July 2015
263 pages
ISBN:9781450335164
DOI:10.1145/2790449
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]

In-Cooperation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 14 July 2015

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. abstract interpretation
  2. deadlock detection
  3. race condition detection

Qualifiers

  • Research-article

Funding Sources

Conference

PPDP '15

Acceptance Rates

Overall Acceptance Rate 230 of 486 submissions, 47%

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)5
  • Downloads (Last 6 weeks)0
Reflects downloads up to 19 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2023)Result Invalidation for Incremental Modular AnalysesVerification, Model Checking, and Abstract Interpretation10.1007/978-3-031-24950-1_14(296-319)Online publication date: 17-Jan-2023
  • (2022)Combining BMC and Fuzzing Techniques for Finding Software Vulnerabilities in Concurrent ProgramsIEEE Access10.1109/ACCESS.2022.322335910(121365-121384)Online publication date: 2022
  • (2019)Effect-Driven Flow AnalysisVerification, Model Checking, and Abstract Interpretation10.1007/978-3-030-11245-5_12(247-274)Online publication date: 11-Jan-2019
  • (2016)Improving trace-based JIT optimisation using whole-program informationProceedings of the 8th International Workshop on Virtual Machines and Intermediate Languages10.1145/2998415.2998418(16-23)Online publication date: 31-Oct-2016
  • (2016)Scala-AM: A Modular Static Analysis Framework2016 IEEE 16th International Working Conference on Source Code Analysis and Manipulation (SCAM)10.1109/SCAM.2016.14(85-90)Online publication date: Oct-2016

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media