Predicate Abstraction Refinement in Thread-Modular Analysis
https://doi.org/10.15514/ISPRAS-2023-35(3)-14
Abstract
Thread-modular approach over predicate abstraction is an efficient technique for software verification of complicated real-world source code. One of the main problems in the technique is a predicate abstraction refinement in a multithreaded case. A default predicate refiner considers only a path related to one thread, and does not refine the thread-modular environment. For instance, if we have applied an effect from the second thread to the current one, then the path in the second thread to the applied effect is not refined. Our goal was to develop a more precise refinement procedure, reusing a default predicate refiner to refine both: a path in a current thread and a path to an effect in the environment. The idea is to construct a joined boolean formula from these two paths. Since some variables may be common, a key challenge is to correctly rename and equate variables in two parts of the formula to accurately represent the way threads interact. It is essential to get reliable predicates that can potentially prove spuriousness of the path.
The proposed approach is implemented on top of CPAchecker framework. It is evaluated on standard SV-COMP benchmark set, and the results show some benefit. Evaluation on the real-world software does not demonstrate significant accuracy increase, as the described flaw of predicate refinement is not the only reason of false positive results. While the proposed approach can successfully prove some specific paths to be spurious, it is not enough to fully prove correctness of some programs. However, the approach has further potential for improvements
About the Authors
Veronika Pavlovna RUDENCHIK
Ivannikov Institute for System Programming of the Russian Academy of Sciences
Russian Federation
Russian Federation
5th year student of the Specialist’s program of MSU, faculty of mechanics and mathematics; laboratory assistant at ISP RAS.
Pavel Sergeevich ANDRIANOV
Ivannikov Institute for System Programming of the Russian Academy of Sciences
Russian Federation
Russian Federation
Researcher in ISP RAS, Ph.D.
References
1. D. Beyer, T. A. Henzinger, and G. The´oduloz, “Configurable software verification: concretizing the convergence of model checking and program analysis,” in Proceedings of CAV, (Berlin, Heidelberg), pp. 504– 518, Springer-Verlag, 2007.
2. D. Beyer, T. Henzinger, and G. Theoduloz, “Program analysis with dynamic precision adjustment,” in Automated Software Engineering, 2008. ASE 2008. 23rd IEEE/ACM International Conference on, pp. 29– 38, sept. 2008.
3. M. Mandrykin, V. Mutilin, and A. Khoroshilov, “Vvedenie v metod CEGAR – utochnenie abstraktsii po kontrprimeram [Introduction to CEGAR – Counter-Example Guided Abstraction Refinement],” Trudy ISP RAN [Proceedings of ISP RAS], vol. 24, pp. 219–292, 2013.
4. S. Graf and H. Saidi, “Construction of abstract state graphs with PVS,” in Computer Aided Verification (O. Grumberg, ed.), (Berlin, Heidelberg), pp. 72–83, Springer Berlin Heidelberg, 1997.
5. T. A. Henzinger, R. Jhala, R. Majumdar, and S. Qadeer, Thread-Modular Abstraction Refinement, pp. 262–274. Berlin, Heidelberg: Springer Berlin Heidelberg, 2003.
6. A. Gupta, C. Popeea, and A. Rybalchenko, “Threader: A constraint-based verifier for multi-threaded programs,” in Proceedings of the 23rd International Conference on Computer Aided Verification, CAV’11, (Berlin, Heidelberg), pp. 412–417, Springer-Verlag, 2011.
7. P. Andrianov, “Analysis of correct synchronization of operating system components,” vol. 46(8), p. 712–730, Programming and Computer Software, 2020.
8. P. Andrianov and V. Mutilin, “Scalable thread-modular approach for data race detection,” Frontiers in Software Engineering Education, pp. 371– 385, 2020.
9. D. Kroening and M. Tautschnig, “Cbmc – c bounded model checker,” vol. 8413, pp. 389–391, 04 2014.
10. J. Alglave, D. Kroening, V. Nimal, and M. Tautschnig, “Software verification for weak memory via program transformation,” ESOP’13, (Berlin, Heidelberg), p. 512–532, Springer-Verlag, 2013.
11. W. Craig, “Three uses of the herbrand-gentzen theorem in relating model theory and proof theory,” Journal of Symbolic Logic, vol. 22, pp. 269– 285, Sep 1957.
12. R. Bruttomesso, A. Cimatti, A. Franze´n, A. Griggio, and R. Sebastiani, “The mathsat 4smt solver,” in CAV, pp. 299–303, 2008.
13. L. de Moura and N. Bjørner, “Z3: an efficient smt solver,” vol. 4963, pp. 337–340, 04 2008.
14. H. Barbosa, C. Barrett, M. Brain, G. Kremer, H. Lachnitt, M. Mann, Mohamed, M. Mohamed, A. Niemetz, A. No¨tzli, A. Ozdemir, M. Preiner, A. Reynolds, Y. Sheng, C. Tinelli, and Y. Zohar, cvc5: A Versatile and Industrial-Strength SMT Solver, pp. 415–442. 01 2022.
15. T. A. Henzinger, R. Jhala, and R. Majumdar, “Lazy abstraction,” in Symposium on Principles of Programming Languages, pp. 58–70, ACM Press, 2002.
16. D. Beyer, M. E. Keremoglu, and P. Wendler, “Predicate abstraction with adjustable-block encoding,” in Proceedings of the 10th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2010, Lugano, October 20-23), pp. 189–197, FMCAD, 2010.
17. R. Cytron, J. Ferrante, B. Rosen, M. Wegman, and K. Zadeck, “Efficiently computing static single assignment form and the control dependence graph,” ACM Trans. Program. Lang. Syst., vol. 13, pp. 451–490, 10 1991.
18. P. Abdulla, S. Aronis, B. Jonsson, and K. Sagonas, “Optimal dynamic partial order reduction,” SIGPLAN Not., vol. 49, pp. 373–384, jan 2014.
19. S. Qadeer and J. Rehof, “Context-bounded model checking of concurrent software,” in Tools and Algorithms for the Construction and Analysis of Systems (N. Halbwachs and L. D. Zuck, eds.), (Berlin, Heidelberg), pp. 93–107, Springer Berlin Heidelberg, 2005.
20. L. Cordeiro, J. Morse, D. Nicole, and B. Fischer, “Context-bounded model checking with esbmc 1.17,” in Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS’12, (Berlin, Heidelberg), pp. 534–537, Springer-Verlag, 2012.
21. C. Flanagan and S. Qadeer, “Thread-modular model checking,” in Proceedings of the 10th International Conference on Model Checking Software, SPIN’03, (Berlin, Heidelberg), pp. 213–224, Springer-Verlag, 2003.
22. T. A. Henzinger, R. Jhala, and R. Majumdar, “Race checking by context inference,” in Proceedings of the ACM SIGPLAN 2004 Conference on Programming Language Design and Implementation, PLDI ’04, (New York, NY, USA), pp. 1–13, ACM, 2004.
23. A. Malkis, A. Podelski, and A. Rybalchenko, “Thread-modular verification is cartesian abstract interpretation,” in Theoretical Aspects of Computing – ICTAC 2006 (K. Barkaoui, A. Cavalcanti, and A. Cerone, eds.), (Berlin, Heidelberg), pp. 183–197, Springer Berlin Heidelberg, 2006.
24. A. Gupta, C. Popeea, and A. Rybalchenko, “Predicate abstraction and refinement for verifying multi-threaded programs,” SIGPLAN Not., vol. 46, pp. 331–344, Jan 2011.
25. A. Cohen and K. S. Namjoshi, “Local proofs for global safety properties,” Form. Methods Syst. Des., vol. 34, pp. 104–125, Apr. 2009.
Review
For citations:
RUDENCHIK V.P., ANDRIANOV P.S. Predicate Abstraction Refinement in Thread-Modular Analysis. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2023;35(3):187-204. https://doi.org/10.15514/ISPRAS-2023-35(3)-14
Email this article 