×

Lost in abstraction: monotonicity in multi-threaded programs. (English) Zbl 1355.68055

Summary: Monotonicity in concurrent systems stipulates that, in any global state, system actions remain executable when new processes are added to the state. This concept is both natural and useful: if every thread’s memory is finite, monotonicity often guarantees the decidability of safety properties even when the number of running threads is unknown. In this paper, we show that finite-data thread abstractions for model checking can be at odds with monotonicity: predicate-abstracting monotone software can result in non-monotone Boolean programs – the monotonicity is lost in the abstraction. As a result, pertinent well-established safety checking algorithms for infinite-state systems become inapplicable. We demonstrate how monotonicity in the abstraction can be restored, without affecting safety properties. This improves earlier approaches of enforcing monotonicity via overapproximations. We implemented our solution in the unbounded-thread model checker \(\mathsf{monabs}\) and applied it to numerous concurrent programs and algorithms, whose predicate abstractions are often fundamentally beyond existing tools.

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Andrews, G. R., Concurrent Programming: Principles and Practice (1991), Benjamin-Cummings Publishing Co., Inc.: Benjamin-Cummings Publishing Co., Inc. Redwood City, CA, USA
[2] Abdulla, P. A.; Cerans, K.; Jonsson, B.; Tsay, Y.-K., General decidability theorems for infinite-state systems, (LICS (1996)), 313-321
[3] Abdulla, P. A.; Delzanno, G.; Rezine, A., Monotonic abstraction in parameterized verification, Electron. Notes Theor. Comput. Sci., 223, 3-14 (2008) · Zbl 1337.68164
[4] Henzinger, T. A.; Jhala, R.; Majumdar, R., Race checking by context inference, (PLDI (2004)), 1-13
[5] Chaki, S.; Clarke, E. M.; Kidd, N.; Reps, T. W.; Touili, T., Verifying concurrent message-passing C programs with recursive calls, (TACAS (2006)), 334-349 · Zbl 1180.68109
[6] Cook, B.; Kroening, D.; Sharygina, N., Verification of Boolean programs with unbounded thread creation, Theor. Comput. Sci., 388, 1-3, 227-242 (2007) · Zbl 1143.68043
[7] Witkowski, T.; Blanc, N.; Kroening, D.; Weissenbacher, G., Model checking concurrent Linux device drivers, (ASE (2007)), 501-504
[8] Gupta, A.; Popeea, C.; Rybalchenko, A., Predicate abstraction and refinement for verifying multi-threaded programs, (POPL (2011)), 331-344 · Zbl 1284.68427
[9] Donaldson, A. F.; Kaiser, A.; Kroening, D.; Tautschnig, M.; Wahl, T., Counterexample-guided abstraction refinement for symmetric concurrent programs, Form. Methods Syst. Des., 41, 1, 25-44 (2012) · Zbl 1284.68179
[10] Farzan, A.; Kincaid, Z., Verification of parameterized concurrent programs by modular reasoning about data and control, (POPL (2012)), 297-308 · Zbl 1321.68192
[11] Farzan, A.; Kincaid, Z.; Podelski, A., Inductive data flow graphs, (POPL (2013)), 129-142 · Zbl 1301.68178
[12] Farzan, A.; Kincaid Duet, Z., Static analysis for unbounded parallelism, (CAV (2013)), 191-196
[13] Malkis, A., Cartesian abstraction and verification of multithreaded programs (2010), University of Freiburg, Ph.D. thesis
[14] Clarke, E. M.; Grumberg, O.; Long, D. E., Model checking and abstraction, ACM Trans. Program. Lang. Syst., 16, 5, 1512-1542 (1994)
[15] Graf, S.; Saïdi, H., Construction of abstract state graphs with PVS, (CAV (1997)), 72-83
[16] Torre, S. L.; Madhusudan, P.; Parlato, G., Model-checking parameterized concurrent programs using linear interfaces, (CAV (2010)), 629-644
[17] Dräger, K.; Kupriyanov, A.; Finkbeiner, B.; Wehrheim, H., SLAB: a certifying model checker for infinite-state concurrent systems, (TACAS (2010)), 271-274
[18] German, S. M.; Sistla, A. P., Reasoning about systems with many processes, J. ACM, 39, 3, 675-735 (1992) · Zbl 0799.68078
[19] Finkel, A.; Schnoebelen, P., Well-structured transition systems everywhere!, Theor. Comput. Sci., 256, 1-2, 63-92 (2001) · Zbl 0973.68170
[20] Abdulla, P. A., Well (and better) quasi-ordered transition systems, Bull. Symb. Log., 16, 4, 457-515 (2010) · Zbl 1207.68219
[21] Minsky, M. L., Computation: Finite and Infinite Machines (1967), Prentice-Hall, Inc.: Prentice-Hall, Inc. Upper Saddle River, NJ, USA · Zbl 0195.02402
[22] Schnoebelen, P., Lossy counter machines decidability cheat sheet, (RP (2010)), 51-75 · Zbl 1287.68101
[23] Ball, T.; Podelski, A.; Rajamani, S. K., Boolean and Cartesian abstraction for model checking C programs, (TACAS (2001)), 268-283 · Zbl 0978.68540
[24] Kaiser, A.; Kroening, D.; Wahl, T., Efficient coverability analysis by proof minimization, (CONCUR (2012)), 500-515 (2012) · Zbl 1364.68138
[25] Gupta, A.; Popeea, C.; Rybalchenko, A., Threader: a constraint-based verifier for multi-threaded programs, (CAV (2011)), 412-417
[26] Gupta, A.; Popeea, C.; Rybalchenko, A., The cream tool
[27] Bozzano, M.; Delzanno, G., Beyond parameterized verification, (Tools and Algorithms for the Construction and Analysis of Systems, Proceedings of the 8th International Conference, TACAS 2002, Held as Part of the Joint European Conference on Theory and Practice of Software. Tools and Algorithms for the Construction and Analysis of Systems, Proceedings of the 8th International Conference, TACAS 2002, Held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2002, Grenoble, France, April 8-12, 2002 (2002)), 221-235 · Zbl 1043.68565
[28] Arons, T.; Pnueli, A.; Ruah, S.; Xu, J.; Zuck, L. D., Parameterized verification with automatically computed inductive assertions, (CAV (2001)), 221-234 · Zbl 0991.68541
[29] Flanagan, C.; Qadeer, S., Predicate abstraction for software verification, (POPL (2002)), 191-202 · Zbl 1323.68371
[30] Lahiri, S. K.; Bryant, R. E., Constructing quantified invariants via predicate abstraction, (VMCAI (2004)), 267-281 · Zbl 1202.68251
[31] Sánchez, A.; Sankaranarayanan, S.; Sánchez, C.; Chang, B.-Y. E., Invariant generation for parametrized systems using self-reflection, (SAS (2012)), 146-163, (extended version)
[32] Abdulla, P. A.; Haziza, F.; Holík, L., All for the price of few, (Verification, Model Checking, and Abstract Interpretation, Proceedings of the 14th International Conference. Verification, Model Checking, and Abstract Interpretation, Proceedings of the 14th International Conference, VMCAI 2013, Rome, Italy, January 20-22, 2013 (2013)), 476-495 · Zbl 1426.68160
[33] Bingham, J. D.; Hu, A. J., Empirically efficient verification for a class of infinite-state systems, (TACAS (2005)), 77-92 · Zbl 1087.68584
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.