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

research-article

Assertion guided abstraction: a cooperative optimization for dynamic partial order reduction

Authors:

Chao WangAuthors Info & Claims

ASE '14: Proceedings of the 29th ACM/IEEE International Conference on Automated Software Engineering

Pages 175 - 186

https://doi.org/10.1145/2642937.2642998

Published: 15 September 2014 Publication History

Abstract

We propose a new method for reducing the interleaving space during stateless model checking of multithreaded C/C++ programs. The problem is challenging because of the exponential growth of possible interleavings between threads. We have developed a new method, called assertion guided abstraction, which leverages both static and dynamic program analyses in a cooperative framework to reduce the interleaving space. Unlike existing methods that consider all interleavings of all conflicting memory accesses in a program, our new method relies on a new notion of predicate dependence based on which we can soundly abstract the interleaving space to only those conflicting memory accesses that may cause assertion violations and/or deadlocks. Our experimental evaluation of assertion guided abstraction on open source benchmarks shows that it is capable of achieving a significant reduction, thereby allowing for the verification of programs that were previously too complex for existing algorithms to handle.

References

[1]

P. A. Abdulla, S. Aronis, B. Jonsson, and K. F. Sagonas. Optimal dynamic partial order reduction. In ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pages 373--384, 2014.

Digital Library

[2]

H. Agrawal and J. R. Horgan. Dynamic program slicing. In ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 246--256, 1990.

Digital Library

[3]

J. Alglave, D. Kroening, and M. Tautschnig. Partial orders for efficient bounded model checking of concurrent software. In International Conference on Computer Aided Verification, pages 141--157, 2013.

[4]

T. Ball and J. R. Larus. Optimally profiling and tracing programs. ACM Trans. Program. Lang. Syst., 16(4):1319--1360, July 1994.

Digital Library

[5]

S. Bindal, S. Bansal, and A. Lal. Variable and thread bounding for systematic testing of multithreaded programs. In International Symposium on Software Testing and Analysis, pages 145--155, 2013.

Digital Library

[6]

J.-D. Choi, B. P. Miller, and R. H. B. Netzer. Techniques for debugging parallel programs with flowback analysis. ACM Trans. Program. Lang. Syst., 13(4):491--530, Oct. 1991.

Digital Library

[7]

E. M. Clarke, Jr., O. Grumberg, and D. A. Peled. Model Checking. MIT Press, Cambridge, MA, USA, 1999.

Digital Library

[8]

K. E. Coons, M. Musuvathi, and K. S. McKinley. Bounded partial-order reduction. In ACM SIGPLAN Conference on Object Oriented Programming, Systems, Languages, and Applications, pages 833--848, 2013.

Digital Library

[9]

E. Duesterwald, R. Gupta, and M. Soffa. Distributed slicing and partial re-execution for distributed programs. In Languages and Compilers for Parallel Computing, pages 497--511. ACM, 1993.

Digital Library

[10]

O. Edelstein, E. Farchi, Y. Nir, G. Ratsaby, and S. Ur. Multithreaded java program test generation. IBM Syst. J., 41(1):111--125, Jan. 2002.

Digital Library

[11]

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

Digital Library

[12]

J. Ferrante, K. J. Ottenstein, and J. D. Warren. The program dependence graph and its use in optimization. ACM Trans. Program. Lang. Syst., 9(3):319--349, July 1987.

Digital Library

[13]

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

Digital Library

[14]

P. Godefroid. Using partial orders to improve automatic verification methods. In International Conference on Computer Aided Verification, pages 176--185, 1991.

Digital Library

[15]

P. Godefroid. Model checking for programming languages using verisoft. In ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pages 174--186, 1997.

Digital Library

[16]

P. Godefroid and D. Pirottin. Refining dependencies improves partial-order verification methods (extended abstract). In International Conference on Computer Aided Verification, pages 438--449, 1993.

Digital Library

[17]

P. Godefroid and P. Wolper. Using partial orders for the efficient verification of deadlock freedom and safety properties. In International Conference on Computer Aided Verification, pages 332--342, 1992.

Digital Library

[18]

R. Gupta, M. L. Soffa, and J. Howard. Hybrid slicing: Integrating dynamic information with static analysis. ACM Trans. Softw. Eng. Methodol., 6(4):370--397, Oct. 1997.

Digital Library

[19]

S. Hong, J. Ahn, S. Park, M. Kim, and M. J. Harrold. Testing concurrent programs to achieve high synchronization coverage. In International Symposium on Software Testing and Analysis, pages 210--220, 2012.

Digital Library

[20]

S. Hong, M. Staats, J. Ahn, M. Kim, and G. Rothermel. The impact of concurrent coverage metrics on testing effectiveness. In IEEE International Conference on Software Testing, Verification and Validation, pages 232--241, 2013.

Digital Library

[21]

S. Horwitz, T. Reps, and D. Binkley. Interprocedural slicing using dependence graphs. In ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 35--46, 1988.

Digital Library

[22]

P. Joshi, M. Naik, C.-S. Park, and K. Sen. CalFuzzer: An extensible active testing framework for concurrent programs. In International Conference on Computer Aided Verification, pages 675--681, 2009.

Digital Library

[23]

V. Kahlon, C. Wang, and A. Gupta. Monotonic partial order reduction: An optimal symbolic partial order reduction technique. In International Conference on Computer Aided Verification, pages 398--413, 2009.

Digital Library

[24]

M. Kamkar, P. Fritzson, and N. Shahmehri. Three approaches to interprocedural dynamic slicing. Microprocessing and Microprogramming, 38(1):625--636, 1993.

Digital Library

[25]

K. Kennedy and J. R. Allen. Optimizing Compilers for Modern Architectures: A Dependence-based Approach. Morgan Kaufmann Publishers Inc., San Francisco, CA, USA, 2002.

Digital Library

[26]

A. Mazurkiewicz. Trace theory. In Advances in Petri Nets 1986, Part II on Petri Nets: Applications and Relationships to Other Models of Concurrency, pages 279--324, New York, NY, USA, 1987. Springer-Verlag New York, Inc.

Digital Library

[27]

M. Musuvathi and S. Qadeer. Iterative context bounding for systematic testing of multithreaded programs. In ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 446--455, 2007.

Digital Library

[28]

Non-blocking data structures. URL: https://code.google.com/p/nbds/.

[29]

Thread-caching malloc implementation. URL: http://www.nedprod.com/programs/portable/nedmalloc/.

[30]

R. H. B. Netzer and M. H. Weaver. Optimal tracing and incremental reexecution for debugging long-running programs. In ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 313--325, 1994.

Digital Library

[31]

S. Park, S. Lu, and Y. Zhou. CTrigger: Exposing atomicity violation bugs from their hiding places. In International Conference on Architectural Support for Programming Languages and Operating Systems, pages 25--36, 2009.

Digital Library

[32]

D. Peled. Combining partial order reductions with on-the-fly model-checking. In International Conference on Computer Aided Verification, pages 377--390, 1994.

Digital Library

[33]

F. Sorrentino, A. Farzan, and P. Madhusudan. PENELOPE: weaving threads to expose atomicity violations. In ACM SIGSOFT Symposium on Foundations of Software Engineering, pages 37--46, 2010.

Digital Library

[34]

2013 software verification competition. URL: http://sv-comp.sosy-lab.org/2013/.

[35]

P. Thomson, A. F. Donaldson, and A. Betts. Concurrency testing using schedule bounding: An empirical study. In ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, pages 15--28, 2014.

Digital Library

[36]

A. Valmari. Stubborn sets for reduced state space generation. In International Conference on Applications and Theory of Petri Nets, pages 491--515, 1991.

Digital Library

[37]

C. Wang, S. Chaudhuri, A. Gupta, and Y. Yang. Symbolic pruning of concurrent program executions. In ACM SIGSOFT Symposium on Foundations of Software Engineering, pages 23--32, 2009.

Digital Library

[38]

C. Wang, M. Said, and A. Gupta. Coverage guided systematic concurrency testing. In International Conference on Software Engineering, pages 221--230, 2011.

Digital Library

[39]

C. Wang, Y. Yang, A. Gupta, and G. Gopalakrishnan. Dynamic model checking with property driven pruning to detect race conditions. In International Symposium on Automated Technology for Verification and Analysis, pages 126--140, 2008.

Digital Library

[40]

C. Wang, Z. Yang, V. Kahlon, and A. Gupta. Peephole partial order reduction. In International Conference on Tools and Algorithms for Construction and Analysis of Systems, pages 382--396, 2008.

Digital Library

[41]

M. Weiser. Program slicing. In International Conference on Software Engineering, pages 439--449, 1981.

Digital Library

[42]

Y. Yang, X. Chen, G. Gopalakrishnan, and R. M. Kirby. Efficient stateful dynamic partial order reduction. In International SPIN workshop on Model Checking Software, pages 288--305, 2008.

Digital Library

[43]

Y. Yang, X. Chen, G. Gopalakrishnan, and C. Wang. Automatic discovery of transition symmetry in multithreaded programs using dynamic analysis. In International SPIN workshop on Model Checking Software, pages 279--295, 2009. LNCS 5578.

Digital Library

[44]

J. Yu, S. Narayanasamy, C. Pereira, and G. Pokam. Maple: A coverage-driven testing tool for multithreaded programs. In ACM SIGPLAN Conference on Object Oriented Programming, Systems, Languages, and Applications, pages 485--502, 2012.

Digital Library

[45]

X. Zhang, R. Gupta, and Y. Zhang. Precise dynamic slicing algorithms. In International Conference on Software Engineering, pages 319--329, May 2003.

Digital Library

Cited By

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
Guo SWu MWang CLeavens GGarcia APăsăreanu C(2018)Adversarial symbolic execution for detecting concurrency-related cache timing leaksProceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering10.1145/3236024.3236028(377-388)Online publication date: 26-Oct-2018
https://dl.acm.org/doi/10.1145/3236024.3236028
Jiang QLiu JHu H(2018)A Thread Modularity Approach for Verification Concurrent Software Based on Abstract Interpretation2018 25th Asia-Pacific Software Engineering Conference (APSEC)10.1109/APSEC.2018.00026(119-128)Online publication date: Dec-2018
https://doi.org/10.1109/APSEC.2018.00026
Show More Cited By

Index Terms

Assertion guided abstraction: a cooperative optimization for dynamic partial order reduction
1. Software and its engineering
  1. Software organization and properties
    1. Software functional properties
      1. Formal methods
        Model checking
2. Theory of computation
  1. Logic
    1. Verification by model checking
  2. Semantics and reasoning
    1. Program reasoning

Recommendations

Assertion guided symbolic execution of multithreaded programs
ESEC/FSE 2015: Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering

Symbolic execution is a powerful technique for systematic testing of sequential and multithreaded programs. However, its application is limited by the high cost of covering all feasible intra-thread paths and inter-thread interleavings. We propose a ...
Dynamic partial order reduction for relaxed memory models
PLDI '15: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation

Under a relaxed memory model such as TSO or PSO, a concurrent program running on a shared-memory multiprocessor may observe two types of nondeterminism: the nondeterminism in thread scheduling and the nondeterminism in store buffering. Although there ...
Dynamic partial order reduction for relaxed memory models
PLDI '15

Under a relaxed memory model such as TSO or PSO, a concurrent program running on a shared-memory multiprocessor may observe two types of nondeterminism: the nondeterminism in thread scheduling and the nondeterminism in store buffering. Although there ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ASE '14: Proceedings of the 29th ACM/IEEE International Conference on Automated Software Engineering

September 2014

934 pages

ISBN:9781450330138

DOI:10.1145/2642937

General Chair:
Ivica Crnkovic
Mälardalen University, Sweden
,
Program Chairs:
Marsha Chechik
University of Toronto, Canada
,
Paul Grünbacher
Johannes Kepler Universität Linz, Austria

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 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

SIGAI: ACM Special Interest Group on Artificial Intelligence
SIGSOFT: ACM Special Interest Group on Software Engineering
Mälardalen University: Mälardalen University
IEEE CS

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 15 September 2014

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

ASE '14

Sponsor:

SIGAI
SIGSOFT
Mälardalen University

ASE '14: ACM/IEEE International Conference on Automated Software Engineering

September 15 - 19, 2014

Vasteras, Sweden

Acceptance Rates

ASE '14 Paper Acceptance Rate 82 of 337 submissions, 24%;

Overall Acceptance Rate 82 of 337 submissions, 24%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

20
Total Citations
View Citations
173
Total Downloads

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

Reflects downloads up to 10 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

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
Guo SWu MWang CLeavens GGarcia APăsăreanu C(2018)Adversarial symbolic execution for detecting concurrency-related cache timing leaksProceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering10.1145/3236024.3236028(377-388)Online publication date: 26-Oct-2018
https://dl.acm.org/doi/10.1145/3236024.3236028
Jiang QLiu JHu H(2018)A Thread Modularity Approach for Verification Concurrent Software Based on Abstract Interpretation2018 25th Asia-Pacific Software Engineering Conference (APSEC)10.1109/APSEC.2018.00026(119-128)Online publication date: Dec-2018
https://doi.org/10.1109/APSEC.2018.00026
Cheng LYang ZWang CRosu GDi Penta MNguyen T(2017)Systematic reduction of GUI test sequencesProceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering10.5555/3155562.3155668(849-860)Online publication date: 30-Oct-2017
https://dl.acm.org/doi/10.5555/3155562.3155668
Guo SWu MWang CBodden ESchäfer WDeursen AZisman A(2017)Symbolic execution of programmable logic controller codeProceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering10.1145/3106237.3106245(326-336)Online publication date: 21-Aug-2017
https://dl.acm.org/doi/10.1145/3106237.3106245
Cheng LYang ZWang C(2017)Systematic reduction of GUI test sequences2017 32nd IEEE/ACM International Conference on Automated Software Engineering (ASE)10.1109/ASE.2017.8115696(849-860)Online publication date: Oct-2017
https://doi.org/10.1109/ASE.2017.8115696
Parízek PPiskac RTalupur M(2016)Hybrid partial order reduction with under-approximate dynamic points-to and determinacy informationProceedings of the 16th Conference on Formal Methods in Computer-Aided Design10.5555/3077629.3077655(141-148)Online publication date: 3-Oct-2016
https://dl.acm.org/doi/10.5555/3077629.3077655
Guo SKusano MWang CLo DApel SKhurshid S(2016)Conc-iSE: incremental symbolic execution of concurrent softwareProceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering10.1145/2970276.2970332(531-542)Online publication date: 25-Aug-2016
https://dl.acm.org/doi/10.1145/2970276.2970332
Sung CKusano MSinha NWang CZimmermann TCleland-Huang JSu Z(2016)Static DOM event dependency analysis for testing web applicationsProceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering10.1145/2950290.2950292(447-459)Online publication date: 1-Nov-2016
https://dl.acm.org/doi/10.1145/2950290.2950292
Kusano MWang CZimmermann TCleland-Huang JSu Z(2016)Flow-sensitive composition of thread-modular abstract interpretationProceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering10.1145/2950290.2950291(799-809)Online publication date: 1-Nov-2016
https://dl.acm.org/doi/10.1145/2950290.2950291
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