Article

Symbolic Predictive Analysis for Concurrent Programs

Authors:

Aarti GuptaAuthors Info & Claims

FM '09: Proceedings of the 2nd World Congress on Formal Methods

Pages 256 - 272

https://doi.org/10.1007/978-3-642-05089-3_17

Published: 04 November 2009 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 happens-before causality relations have been proposed for predictive analysis to improve the interleaving coverage while ensuring the absence of false alarms. However, these models are based on only the observed events, and typically do not utilize source code. Furthermore, the enumerative algorithms they use for verifying safety properties in the predicted execution traces often suffer from the interleaving explosion problem. In this paper, we introduce a new symbolic causal model based on source code and the observed events, and propose a symbolic algorithm to check whether a safety property holds in all feasible permutations of events in the given execution trace. Rather than explicitly enumerating the interleavings, our algorithm conducts the verification using a novel encoding of the causal model and symbolic reasoning with a satisfiability modulo theory (SMT) solver. Our algorithm has a larger interleaving coverage than known causal models in the literature. We also propose a method to <em>symbolically bound</em> the number of context switches allowed in an interleaving, to further improve the scalability of the algorithm.

References

[1]

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

[2]

Flanagan, C., Freund, S.N.: Atomizer: A dynamic atomicity checker for multithreaded programs. In: Parallel and Distributed Processing Symposium (IPDPS). IEEE, Los Alamitos (2004).

[3]

Wang, L., Stoller, S.D.: Runtime analysis of atomicity for multithreaded programs. IEEE Trans. Software Eng. 32(2), 93-110 (2006).

[4]

Sen, K., Rosu, G., Agha, G.: Detecting errors in multithreaded programs by generalized predictive analysis of executions. In: Steffen, M., Zavattaro, G. (eds.) FMOODS 2005. LNCS, vol. 3535, pp. 211-226. Springer, Heidelberg (2005).

[5]

Chen, F., Rosu, G.: Parametric and sliced causality. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 240-253. Springer, Heidelberg (2007).

[6]

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

[7]

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

[8]

Wang, C., Chaudhuri, S., Gupta, A., Yang, Y.: Symbolic pruning of concurrent program executions. In: Foundations of Software Engineering. ACM, New York (2009).

[9]

Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168-176. Springer, Heidelberg (2004).

[10]

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

[11]

Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 81-94. Springer, Heidelberg (2006).

[12]

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

[13]

Wang, C., Yang, Z., Kahlon, V., Gupta, A.: Peephole partial order reduction. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 382-396. Springer, Heidelberg (2008).

[14]

Kahlon, V., Wang, C., Gupta, A.: Monotonic partial order reduction: An optimal symbolic partial order reduction technique. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 398-413. Springer, Heidelberg (2009).

[15]

Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 93-107. Springer, Heidelberg (2005).

[16]

Musuvathi, M., Qadeer, S.: CHESS: Systematic stress testing of concurrent software. In: Puebla, G. (ed.) LOPSTR 2006. LNCS, vol. 4407, pp. 15-16. Springer, Heidelberg (2007).

[17]

Lal, A., Reps, T.W.: Reducing concurrent analysis under a context bound to sequential analysis. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 37-51. Springer, Heidelberg (2008).

[18]

Farchi, E., Nir, Y., Ur, S.: Concurrent bug patterns and how to test them. In: Guo, M. (ed.) ISPA 2003. LNCS, vol. 2745, p. 286. Springer, Heidelberg (2003).

[19]

Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: Principles of programming languages, pp. 110-121 (2005).

[20]

Fidge, C.J.: Logical time in distributed computing systems. IEEE Computer 24(8), 28-33 (1991).

[21]

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

[22]

Rabinovitz, I., Grumberg, O.: Bounded model checking of concurrent programs. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 82-97. Springer, Heidelberg (2005).

[23]

Godefroid, P.: Software model checking: The VeriSoft approach. Formal Methods in System Design 26(2), 77-101 (2005).

[24]

Yang, Y., Chen, X., Gopalakrishnan, G.: Inspect: A Runtime Model Checker for Multithreaded C Programs. Technical Report UUCS-08-004, University of Utah (2008).

Cited By

Huang ZRavi SWang CFilkov VRay BZhou M(2024)Discovering Likely Program Invariants for Persistent MemoryProceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering10.1145/3691620.3695544(1795-1807)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1145/3691620.3695544
Farzan AMathur U(2024)Coarser Equivalences for Causal ConcurrencyProceedings of the ACM on Programming Languages10.1145/36328738:POPL(911-941)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632873
Wang MSrikant SSamak MO’Reilly UFerrara PHadarean L(2023)RaceInjector: Injecting Races to Evaluate and Learn Dynamic Race Detection AlgorithmsProceedings of the 12th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis10.1145/3589250.3596142(63-70)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3589250.3596142
Show More Cited By

Symbolic Predictive Analysis for Concurrent Programs

Recommendations

Symbolic predictive analysis for concurrent programs
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 ...
Execution privatization for scheduler-oblivious concurrent programs
OOPSLA '12

Making multithreaded execution less non-deterministic is a promising solution to address the difficulty of concurrent programming plagued by the non-deterministic thread scheduling. In fact, a vast category of concurrent programs are scheduler-oblivious:...
Verifying concurrent programs: tutorial talk
FMCAD '11: Proceedings of the International Conference on Formal Methods in Computer-Aided Design

The proliferation of multi-core hardware has led to widespread use of concurrent programs. However, these programs are notoriously difficult to get right and to debug for developers. Even for automated verification, it is a big challenge to reason about ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

FM '09: Proceedings of the 2nd World Congress on Formal Methods

November 2009

818 pages

ISBN:9783642050886

Editors:
Ana Cavalcanti
Department of Computer Science, Heslington, University of York, York, UK Y010 5DD
,
Dennis R. Dams
Bell Laboratories, Murray Hill, USA 07974

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 04 November 2009

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

61
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 12 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Huang ZRavi SWang CFilkov VRay BZhou M(2024)Discovering Likely Program Invariants for Persistent MemoryProceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering10.1145/3691620.3695544(1795-1807)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1145/3691620.3695544
Farzan AMathur U(2024)Coarser Equivalences for Causal ConcurrencyProceedings of the ACM on Programming Languages10.1145/36328738:POPL(911-941)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632873
Wang MSrikant SSamak MO’Reilly UFerrara PHadarean L(2023)RaceInjector: Injecting Races to Evaluate and Learn Dynamic Race Detection AlgorithmsProceedings of the 12th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis10.1145/3589250.3596142(63-70)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3589250.3596142
Fan HSun ZHe F(2023)Satisfiability Modulo Ordering Consistency Theory for SC, TSO, and PSO Memory ModelsACM Transactions on Programming Languages and Systems10.1145/357983545:1(1-37)Online publication date: 3-Mar-2023
https://dl.acm.org/doi/10.1145/3579835
Sun ZFan HHe F(2022)Consistency-preserving propagation for SMT solving of concurrent program verificationProceedings of the ACM on Programming Languages10.1145/35633216:OOPSLA2(929-956)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563321
Wen CHe MWu BXu ZQin SDwyer MDamian DZeller A(2022)Controlled concurrency testing via periodical schedulingProceedings of the 44th International Conference on Software Engineering10.1145/3510003.3510178(474-486)Online publication date: 21-May-2022
https://dl.acm.org/doi/10.1145/3510003.3510178
He FSun ZFan HFreund SYahav E(2021)Satisfiability modulo ordering consistency theory for multi-threaded program verificationProceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3453483.3454108(1264-1279)Online publication date: 19-Jun-2021
https://dl.acm.org/doi/10.1145/3453483.3454108
Mathur UPavlogiannis AViswanathan M(2021)Optimal prediction of synchronization-preserving racesProceedings of the ACM on Programming Languages10.1145/34343175:POPL(1-29)Online publication date: 4-Jan-2021
https://dl.acm.org/doi/10.1145/3434317
Mathur UPavlogiannis AViswanathan MHermanns HZhang LKobayashi NMiller D(2020)The Complexity of Dynamic Data Race PredictionProceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3373718.3394783(713-727)Online publication date: 8-Jul-2020
https://dl.acm.org/doi/10.1145/3373718.3394783
Pavlogiannis A(2019)Fast, sound, and effectively complete dynamic race predictionProceedings of the ACM on Programming Languages10.1145/33710854:POPL(1-29)Online publication date: 20-Dec-2019
https://dl.acm.org/doi/10.1145/3371085
Show More Cited By

View Options

View options

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 Publication

Media

Figures

Other

Tables

View Table of Contents