research-article

Open access

Symbolic predictive analysis for concurrent programs

Authors:

Rhishikesh Limaye,

Aarti GuptaAuthors Info & Claims

Formal Aspects of Computing, Volume 23, Issue 6

Pages 781 - 805

https://doi.org/10.1007/s00165-011-0179-2

Published: 01 November 2011 Publication History

Abstract

Predictive analysis aims at detecting concurrency errors during runtime by monitoring a concrete execution trace of a concurrent program. In recent years, various models based on the happens-before causality relations have been proposed for predictive analysis. However, these models often rely on only the observed runtime events and typically do not utilize the program source code. Furthermore, the enumerative algorithms they use for verifying safety properties in the predicted traces often suffer from the interleaving explosion problem. In this paper, we introduce a precise predictive model based on both the program source code and the observed execution events, and propose a symbolic algorithm to check whether a safety property holds in all feasible permutations of events of the given trace. Rather than explicitly enumerating and checking the interleavings, our method conducts the search using a novel encoding and symbolic reasoning with a satisfiability modulo theory solver. We also propose a technique to bound the number of context switches allowed in the interleavings during the symbolic search, to further improve the scalability of the algorithm.

References

References

[1]

Burckhardt S, Alur R, and Martin M (2007) CheckFence: checking consistency of concurrent data types on relaxed memory models. In: ACM SIGPLAN Conference on Programming Language Design and Implementation, pp 12–21

[2]

Biere A, Cimatti A, Clarke E, and Zhu Y (1999) Symbolic model checking without BDDs. In: Tools and Algorithms for Construction and Analysis of Systems. LNCS, vol 1579. Springer, Berlin, pp 193–207

[3]

Beckman N, Nori AV, Rajamani SK, Simmons RJ (2008) Proofs from tests. In: International Symposium on Software Testing and Analysis, pp 3–14

[4]

Clarke E, Kroening D, Lerda F (2004) A tool for checking ANSI-C programs. In: International Conference on Tools and Algorithms for Construction and Analysis of Systems. LNCS, vol 2988. pp 168–176

[5]

Chen F, Rosu G (2007) Parametric and sliced causality. In: International Conference on Computer Aided Verification. LNCS, vol 4590, Springer, Berlin, pp 240–253

[6]

Dutertre B and de Moura L (2006) A fast linear-arithmetic solver for DPLL(T). In International Conference on Computer Aided Verification. LNCS, vol 4144. Springer, Berlin, pp 81–94

[7]

Flanagan C, Freund SN (2004) Atomizer: a dynamic atomicity checker for multithreaded programs. In: Parallel and Distributed Processing Symposium

[8]

Flanagan C, Freund SN, Yi J (2008) Velodrome: a sound and complete dynamic atomicity checker for multithreaded programs. In: ACM SIGPLAN Conference on Programming Language Design and Implementation, pp 293–303

[9]

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

[10]

Fidge CJ. Logical time in distributed computing systems IEEE Comput 1991 24 8 28-33

Digital Library

[11]

Farzan A, Madhusudan P (2006) Causal atomicity. In: International Conference on Computer Aided Verification. LNCS, vol 4144. pp 315–328

[12]

Farzan A, Madhusudan P (2008) Monitoring atomicity in concurrent programs. In: International Conference on Computer Aided Verification. LNCS, vol 5123. pp 52–65

[13]

Farzan A, Madhusudan P (2009) The complexity of predicting atomicity violations. In: International Conference on Tools and Algorithms for Construction and Analysis of Systems, pp 155–169

[14]

Farzan A, Madhusudan P (2009) Meta-analysis for atomicity violations under nested locking. In: International Conference on Computer Aided Verification, LNCS, pp 248–262

[15]

Farchi E, Nir Y, Ur S (2003) Concurrent bug patterns and how to test them. In: Parallel and Distributed Processing Symposium

[16]

Flanagan C, Qadeer S (2003) A type and effect system for atomicity. In: ACM SIGPLAN Conference on Programming Language Design and Implementation, pp 338–349

[17]

Havelund K, Pressburger T (2000) Model checking Java programs using Java PathFinder. Softw Tools Technol Transf 2(4)

[18]

http://www2.epcc.ed.ac.uk/computing/research_activities/java_grande/index_1.html. The java grande forum benchmark suite.

[19]

Ivančić F, Yang Z, Shlyakhter I, Ganai MK, Gupta A, Ashar P (2005) F-Soft : Software verification platform. In: Computer-Aided Verification. LNCS, vol 3576. Springer, Berlin, pp. 301–306

[20]

Jussila T, Heljanlo K, and Niemelä I BMC via on-the-fly determinization Int J Softw Tools Technol Transf 2005 7 2 89-101

Digital Library

[21]

Kahlon V, Ivancic F,Gupta A (2005) Reasoning about threads communicating via locks. In: International Conference on Computer Aided Verification. LNCS, vol 3576. pp 505–518

[22]

Kahlon V, Wang C (2010) Universal Causality Graphs: a precise happens-before model for detecting bugs in concurrent programs. In: International Conference on Computer Aided Verification. LNCS, vol 6174. Springer, Berlin, pp 434–449

[23]

Kahlon V, Wang C, Gupta A (2009) Monotonic partial order reduction: An optimal symbolic partial order reduction technique. In: International Conference on Computer Aided Verification. pp 398–413

[24]

Lamport L. Time, clocks, and the ordering of events in a distributed system Commun ACM 1978 21 7 558-565

Digital Library

[25]

Lee J, Padua D, Midkiff S (1999) Basic compiler algorithms for parallel programs. In: Principles and Practice of Parallel Programming, pp 1–12

[26]

Lahiri S, Qadeer S (2008) Back to the future: revisiting precise program verification using SMT solvers. In ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp 171–182

[27]

Lahiri S, Qadeer S, Rakamaric Z (2009) Static and precise detection of concurrency errors in systems code using SMT solvers. In: International Conference on Computer Aided Verification, pp 509–524

[28]

Lal A, Reps TW (2008) Reducing concurrent analysis under a context bound to sequential analysis. In: International Conference on Computer Aided Verification. LNCS, vol 5123. pp 37–53

[29]

Lu S, Tucek J, Qin F, Zhou Y (2006) AVIO: detecting atomicity violations via access interleaving invariants. In: Architectural Support for Programming Languages and Operating Systems, pp 37–48

[30]

Musuvathi M, Qadeer S (2006) CHESS: systematic stress testing of concurrent software. In: Logic-Based Program Synthesis and Transformation. LNCS, vol 4407. Springer, Berlin, pp 15–16

[31]

Necula G, McPeak S, Rahul S, and Weimer W (2002) CIL: Intermediate language and tools for analysis and transformation of c programs. In International Conference on Compiler Construction. LNCS 2304, pp. 213–228

[32]

Qadeer S (2004) Joint CAV/ISSTA special event on specification, verification, and testing of concurrent software

[33]

Qadeer S, Rehof J (2005) Context-bounded model checking of concurrent software. In: International Conference on Tools and Algorithms for Construction and Analysis of Systems. Springer, Berlin, pp 93–107

[34]

Rabinovitz I, Grumberg O (2005) Bounded model checking of concurrent programs. In: International Conference on Computer Aided Verification, LNCS, vol 2988. pp 82–97

[35]

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

Digital Library

[36]

Serbănută TF, Chen F, Rosu G (2008) Maximal causal models for multithreaded systems. Technical Report UIUCDCS-R-2008-3017, University of Illinois at Urbana-Champaign

[37]

Sadowski C, Freund SN, Flanagan C (2009) Singletrack: a dynamic determinism checker for multithreaded programs. In: European Symposium on Programming, pp 394–409

[38]

Sen K, Rosu G, Agha G (2005) Detecting errors in multithreaded programs by generalized predictive analysis of executions. In: Formal Methods for Open Object-Based Distributed Systems, pp 211–226

[39]

Said M, Wang C, Yang Z, Sakallah K (2011) Generating data race witnesses by an SMT-based analysis. In: NASA Formal Methods Symposiumvon

[40]

Praun C, Gross TR (2004) Static detection of atomicity violations in object-oriented programs. Object Technol 3(6)

[41]

Wang C, Chaudhuri S, Gupta A, Yang Y (2009) Symbolic pruning of concurrent program executions. In: ACM SIGSOFT Symposium on Foundations of Software Engineering, pp 23–32

[42]

Wang C, Gupta A, Ganai M (2006) Predicate learning and selective theory deduction for a difference logic solver. In: Design Automation Conference, ACM, New York, pp 235–240.

[43]

Wang C, Ivančić F, Ganai M, Gupta A (2005) Deciding separation logic formulae by SAT and incremental negative cycle elimination. In: Logic for Programming Artificial Intelligence and Reasoning. LNCS, vol 3835. Springer, Berlin pp 322–336

[44]

Wang C, Kundu S, Ganai M, Gupta A (2009) Symbolic predictive analysis for concurrent programs. In: International Symposium on Formal Methods, pp 256–272

[45]

Wang C, Limaye R, Ganai M, Gupta A (2010) Trace-based symbolic analysis for atomicity violations. In: International Conference on Tools and Algorithms for Construction and Analysis of Systems

[46]

Wang L and Stoller SD. Runtime analysis of atomicity for multithreaded programs IEEE Trans Softw Eng 2006 32 2 93-110

Digital Library

[47]

Wang C, Said M, Gupta A (2011) Coverage driven systematic concurrency testing. In: International Conference on Software Engineering

[48]

Wang C, Yang Y, Gupta A, Gopalakrishnan G (2008) Dynamic model checking with property driven pruning to detect race conditions. In: Automated Technology for Verification and Analysis

[49]

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

[50]

Xu M, Bodík R, Hill MD (2005) A serializability violation detector for shared-memory server programs. In: ACM SIGPLAN Conference on Programming Language Design and Implementation, pp 1–14

[51]

Yang Y, Chen X, Gopalakrishnan G (2008) Inspect: a runtime model checker for multithreaded C programs. Technical Report UUCS-08-004, University of Utah

[52]

Yang Y, Chen X, Gopalakrishnan G, Wang C (2009) Automatic discovery of transition symmetry in multithreaded programs using dynamic analysis. In: SPIN workshop on Software Model Checking

Cited By

Cai YYe CShi QZhang CRoychoudhury ACadar CKim M(2022)Peahen: fast and precise static deadlock detection via context reductionProceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering10.1145/3540250.3549110(784-796)Online publication date: 7-Nov-2022
https://dl.acm.org/doi/10.1145/3540250.3549110
Fu HWang ZChen XFan X(2018)A systematic survey on automated concurrency bug detection, exposing, avoidance, and fixing techniquesSoftware Quality Journal10.1007/s11219-017-9385-326:3(855-889)Online publication date: 1-Sep-2018
https://dl.acm.org/doi/10.1007/s11219-017-9385-3

Recommendations

Symbolic Predictive Analysis for Concurrent Programs
FM '09: Proceedings of the 2nd World Congress on Formal Methods

Predictive analysis aims at detecting concurrency errors during runtime by monitoring a concrete execution trace of a concurrent program. In recent years, various models based on happens-before causality relations have been proposed for predictive ...
Symbolic pruning of concurrent program executions
ESEC/FSE '09: Proceedings of the 7th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering

We propose a new algorithm for verifying concurrent programs, which uses concrete executions to partition the program into a set of lean partitions called concurrent trace programs (CTPs), and symbolically verifies each CTP using a satisfiability ...
Symbolic finite state transducers: algorithms and applications
POPL '12

Finite automata and finite transducers are used in a wide range of applications in software engineering, from regular expressions to specification languages. We extend these classic objects with symbolic alphabets represented as parametric theories. ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Formal Aspects of Computing

Formal Aspects of Computing Volume 23, Issue 6

Nov 2011

121 pages

ISSN:0934-5043

EISSN:1433-299X

Issue’s Table of Contents

© British Computer Society 2011.

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 November 2011

Accepted: 09 November 2010

Revision received: 02 July 2010

Received: 18 March 2010

Published in FAC Volume 23, Issue 6

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
58
Total Downloads

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

Reflects downloads up to 13 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Cai YYe CShi QZhang CRoychoudhury ACadar CKim M(2022)Peahen: fast and precise static deadlock detection via context reductionProceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering10.1145/3540250.3549110(784-796)Online publication date: 7-Nov-2022
https://dl.acm.org/doi/10.1145/3540250.3549110
Fu HWang ZChen XFan X(2018)A systematic survey on automated concurrency bug detection, exposing, avoidance, and fixing techniquesSoftware Quality Journal10.1007/s11219-017-9385-326:3(855-889)Online publication date: 1-Sep-2018
https://dl.acm.org/doi/10.1007/s11219-017-9385-3

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

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 Article

Media

Figures

Other

Tables

View Issue’s Table of Contents