Уточнение предикатной абстракции при раздельном анализе потоков
https://doi.org/10.15514/ISPRAS-2023-35(3)-14
Аннотация
Комбинация анализа с раздельным рассмотрением потоков (Thread-Modular analysis) и предикатной абстракции является эффективной техникой верификации реального программного обеспечения. Одним из недостатков этой техники является уточнение предикатной абстракции при анализе многопоточных программ. В классической процедуре уточнения абстракции рассматривается только путь в одном потоке, и окружение Thread-Modular анализа не уточняется. Например, при применении эффекта из второго потока к первому путь к эффекту во втором потоке не уточняется. Целью нашей работы была разработка более точной процедуры уточнения абстракции, которая бы переиспользовала имеющуюся процедуру уточнения абстракции и позволяла бы уточнять и путь в анализируемом потоке, и путь в окружении. Основная идея заключается в построении совместной логической формулы для двух путей. Так как имена переменных разных потоков могут совпасть, необходимо корректно переименовать и приравнять некоторые переменные для того, чтобы формула правильно отражала связи между потоками. Это позволяет получить предикаты, необходимые для доказательства недостижимости пути.
Предложенный подход был реализован на базе инструмента статической верификации CPAchecker. Подход был оценен на стандартном наборе задач SV-COMP и показал небольшое улучшение. Для больших программ улучшений в результатах не наблюдалась, так как описанный недостаток анализа не является единственной причиной ложноположительных результатов. Предложенный подход может успешно доказать недостижимость некоторых путей, то этого может быть недостаточно для доказательства корректности программы. Однако подход обладает дальнейшим потенциалом для совершенствования.
Об авторах
Вероника Павловна РУДЕНЧИК
Институт системного программирования им. В.П. Иванникова РАН
Россия
Россия
Cтудентка 5 курса специалитета механико-математического факультета МГУ, лаборант ИСП РАН
Павел Сергеевич АНДРИАНОВ
Институт системного программирования им. В.П. Иванникова РАН
Россия
Россия
Научный сотрудник ИСП РАН, кандидат физико-математических наук.
Список литературы
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.
Рецензия
Для цитирования:
РУДЕНЧИК В.П., АНДРИАНОВ П.С. Уточнение предикатной абстракции при раздельном анализе потоков. Труды Института системного программирования РАН. 2023;35(3):187-204. https://doi.org/10.15514/ISPRAS-2023-35(3)-14
For citation:
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
Послать статью по эл. почте 