×

Symbolic predictive analysis for concurrent programs. (English) Zbl 1242.68187

Summary: 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.

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
PDF BibTeX XML Cite
Full Text: DOI

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 · Zbl 1126.68470
[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 · Zbl 1135.68468
[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 · Zbl 1146.68350
[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 · Zbl 1369.68135
[10] Fidge CJ. (1991) Logical time in distributed computing systems. IEEE Comput 24(8): 28–33 · Zbl 05089955
[11] Farzan A, Madhusudan P (2006) Causal atomicity. In: International Conference on Computer Aided Verification. LNCS, vol 4144. pp 315–328 · Zbl 1188.68186
[12] Farzan A, Madhusudan P (2008) Monitoring atomicity in concurrent programs. In: International Conference on Computer Aided Verification. LNCS, vol 5123. pp 52–65 · Zbl 1155.68365
[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 · Zbl 1234.68076
[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 · Zbl 1242.68065
[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 · Zbl 1271.68086
[17] Havelund K, Pressburger T (2000) Model checking Java programs using Java PathFinder. Softw Tools Technol Transf 2(4) · Zbl 1059.68585
[18] http://www2.epcc.ed.ac.uk/computing/research_activities/java_grande/index_1.html . The java grande forum benchmark suite. · Zbl 1009.68547
[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 · Zbl 1081.68581
[20] Jussila T, Heljanlo K, Niemelä I (2005) BMC via on-the-fly determinization. Int J Softw Tools Technol Transf 7(2):89–101
[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 · Zbl 1081.68623
[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 · Zbl 1242.68166
[24] Lamport L. (1978) Time, clocks, and the ordering of events in a distributed system. Commun ACM 21(7): 558–565 · Zbl 0378.68027
[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 · Zbl 1295.68087
[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 · Zbl 1155.68368
[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 · Zbl 1051.68756
[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 · Zbl 1087.68598
[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 · Zbl 1081.68633
[35] Savage S, Burrows M, Nelson G, Sobalvarro P, Anderson T (1997) Eraser: a dynamic data race detector for multithreaded programs. ACM Trans Comput Syst 15(4):391–411
[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 · Zbl 1234.68066
[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 · Zbl 1143.68583
[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 · Zbl 1242.68187
[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 · Zbl 1284.68418
[46] Wang L, Stoller SD. (2006) Runtime analysis of atomicity for multithreaded programs. IEEE Trans Softw Eng 32(2): 93–110 · Zbl 05113288
[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 · Zbl 1183.68383
[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 · Zbl 1134.68421
[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
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.