Анализ корректности синхронизации компонентов ядра операционных систем
https://doi.org/10.15514/ISPRAS-2019-31(5)-16
Аннотация
Большинство современных инструментов статической верификации плохо масштабируются на сложное программное обеспечение. Целью работы была разработка инструмента, который станет золотой серединой между точными и медленными инструментами статической верификации и быстрыми, но менее точными инструментами статического анализа. Основной идеей подхода является абстракция от точного взаимодействия потоков и анализ каждого потока отдельно от всех остальных, но в некотором окружении, которое моделирует влияние потоков друг на друга. Окружение содержит описание возможных действий над разделяемыми данными и примитивами синхронизации, а также условий их применения. Варьируя точность построения окружения, можно добиваться необходимого баланса между скоростью и точностью анализа в целом. Формальное описание предлагаемого подхода было сделано с использованием теории адаптивного статического анализа. Это позволило сформулировать условия и доказать корректность предлагаемого подхода в этих условиях. Для эффективного поиска состояний гонки используется специальная модель памяти, которая позволяет разделять области памяти на непересекающиеся регионы, соответствующие типам данных. Реализация предложенного подхода во фреймворке CPAchecker позволяет переиспользовать существующие техники анализа с минимальными изменениями. А реализация дополнительных техник анализа в рамках предложенной теории позволяет повысить точность анализа. Результаты проведенных экспериментов на двух наборах тестовых задач позволяют заключить о масштабируемости и практической применимости метода.
Об авторе
Павел Сергеевич АндриановРоссия
Младший научный сотрудник
Список литературы
1. Parosh Abdulla, Stavros Aronis, Bengt Jonsson, and Konstantinos Sagonas. Optimal dynamic partial order reduction. SIGPLAN Notices, vol. 49, issue 1, 2014, pp. 373–384.
2. Patrice Godefroid. Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem. Springer-Verlag, Berlin, Heidelberg, 1996, 143 p.
3. Gérard Basler, Michele Mazzucchi, Thomas Wahl, and Daniel Kroening. Symbolic counter abstraction for concurrent software. Lecture Notes in Computer Science, vol. 5643, 2009, pp. 64–78.
4. Dirk Beyer. Automatic verification of C and Java Programs: SV-COMP. Lecture Notes in Computer Science, vol. 11429, 2019, pp. 133–155.
5. Dirk Beyer, Thomas A. Henzinger, and Grégory Théoduloz. Configurable software verification: concretizing the convergence of model checking and program analysis. Lecture Notes in Computer Science, vol. 4590, 2007, pp. 504–518
6. D. Beyer, T.A. Henzinger, and G. Theoduloz. Program analysis with dynamic precision adjustment. In Proc. of the 23rd IEEE/ACM International Conference on Automated Software Engineering, 2008, pp. 29–38.
7. Cormac Flanagan and Shaz Qadeer. Thread-modular model checking. Lecture Notes in Computer Science, vol. 2648, 2003, pp. 213–224.
8. Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Shaz Qadeer. Thread-Modular Abstraction Lecture Notes in Computer Science, vol. 2725, 2003, pp, 262–274.
9. Byron Cook, Daniel Kroening, and Natasha Sharygina. Verification of Boolean programs with unbounded thread creation. Theoretical Computer Science, vol. 388, issue 1-3, 2007, pp. 227–242.
10. Ashutosh Gupta, Corneliu Popeea, and Andrey Rybalchenko. Threader: A constraint-based verifier for multi-threaded programs. Lecture Notes in Computer Science, vol. 6806, 2011, pp. 412–417.
11. E.M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. Lecture Notes in Computer Science, vol. 1855, 2000, pp. 154–169.
12. Susanne Graf and Hassen Saidi. Construction of abstract state graphs with PVS. Lecture Notes in Computer Science, vol. 1254, 1997, pp. 72–83.
13. Stefan Savage, Michael Burrows, Greg Nelson, Patrick Sobalvarro, and Thomas Anderson. Eraser: A dynamic data race detector for multi-threaded programs. ACM SIGOPS Operating Systems Review, vol. 31, issue 5, 1997, pp. 27–37.
14. Richard Bornat. Proving pointer programs in Hoare logic. Lecture Notes in Computer Science, vol. 1837, 2000, pp. 102–126.
15. R M Burstall. Some techniques for proving correctness of programs which alter data structures. Machine Intelligence, vol. 7, 1972, pp. 23–50.
16. Pavel Andrianov, Karlheinz Friedberger, Mikhail Mandrykin, Vadim Mutilin, and Anton Volkov. CPA-BAM-BnB: Block-abstraction memoization and region-based memory models for predicate abstractions. Lecture Notes in Computer Science, vol. 10206, 2017, pp. 355–359.
17. Evgeny Novikov and Ilja Zakharov. Towards automated static verification of GNU C programs. Lecture Notes in Computer Science, vol. 10742, 2018, pp. 402–416.
18. Evgeny Novikov and Ilja Zakharov. Verification of operating system monolithic kernels without extensions. Lecture Notes in Computer Science, vol. 11247, 2018, pp. 230–248.
19. Dirk Beyer and Karlheinz Friedberger. In Proc. of the 11th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science, 2016, pp. 61–71.
20. Dirk Beyer and Stefan Löwe. Explicit-state software model checking based on CEGAR and interpolation. Lecture Notes in Computer Science, vol. 7793, 2013, pp. 146–162.
21. D. Beyer, M.E. Keremoglu, and P. Wendler. Predicate abstraction with adjustable-block encoding. In Proc. of 10th International Conference on Formal Methods in Computer-Aided Design, 2010, pp. 189–197.
22. Armin Biere, Alessandro Cimatti, Edmund M. Clarke, and Yunshan Zhu. Symbolic model checking without bdds. Lecture Notes in Computer Science, vol. 1579, 1999, pp. 193–207
23. Dirk Beyer, Stefan Löwe, and Philipp Wendler. Reliable benchmarking: requirements and solutions. International Journal on Software Tools for Technology Transfer, vol. 21, issue 1, 2019, pp. 1–29.
24. Shaz Qadeer and Jakob Rehof. Context-bounded model checking of concurrent software. Lecture Notes in Computer Science, vol. 3440, 2005, pp. 93–107.
25. Lucas Cordeiro, Jeremy Morse, Denis Nicole, and Bernd Fischer. Context-bounded model checking with esbmc 1.17. Lecture Notes in Computer Science, vol. 7214, 2012, pp. 534–537.
26. Ariel Cohen and Kedar S. Namjoshi. Local proofs for global safety properties. Formal Methods in System Design, vol. 34, issue 2, 2009, pp. 104–125.
27. Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar. Race checking by context inference. In Proc. of the ACM SIGPLAN 2004 Conference on Programming Language Design and Implementation, 2004, pp. 1–13.
28. Alexander Malkis, Andreas Podelski, and Andrey Rybalchenko. Thread-modular verification is cartesian abstract interpretation. Lecture Notes in Computer Science, vol. 4281, 2006, pp. 183–197.
29. Ashutosh Gupta, Corneliu Popeea, and Andrey Rybalchenko. Predicate abstraction and refinement for verifying multi-threaded programs. ACM SIGPLAN Notices, vol. 46, issue 1m 2011, pp. 331–344.
30. Akash Lal and Thomas Reps. Reducing concurrent analysis under a context bound tosequential analysis. Formal Methods in System Design, vol. 35, issue 1, 2009, pp. 73–97.
31. Salvatore La Torre, P. Madhusudan, and Gennaro Parlato. Reducing context-bounded concurrent reachability to sequential reachability. Lecture Notes in Computer Science, vol. 5643, 2009, pp. 477–492.
32. Ermenegildo Tomasco, Omar Inverso, Bernd Fischer, Salvatore La Torre, and Gennaro Parlato. MU-CSeq: Sequentialization of C programs by shared memory unwindings. Lecture Notes in Computer Science, vol. 8413, 2014, pp. 402–404.
33. Pantazis Deligiannis, Alastair F. Donaldson, and Zvonimir Rakamaric. Fast and precise symbolic analysis of concurrency bugs in device drivers (t). In Proc. of the 2015 30th IEEE/ACM International Conference on Automated Software Engineering (ASE), 2015, pp. 166–177.
34. Akash Lal, Shaz Qadeer, and Shuvendu K. Lahiri. A solver for reachability modulo theories. Lecture Notes in Computer Science, vol. 7358, 2012, pp. 427–443.
35. Jan Wen Voung, Ranjit Jhala, and Sorin Lerner. RELAY: Static race detection on millions of lines of code. In Proceedings of the 6th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on The Foundations of Software Engineering, 2007, pp. 205–214.
36. Polyvios Pratikakis, Jeffrey S. Foster, and Michael Hicks. LOCKSMITH: Context-sensitive correlation analysis for race detection. In Proc. of the 27th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2006, pp. 320–331.
37. Peng Di and Yulei Sui. Accelerating dynamic data race detection using static thread interference analysis. In Proc. of the 7th International Workshop on Programming Models and Applications for Multicores and Manycores, 2016, pp. 30–39.
38. Daniel Kroening, Lihao Liang, Tom Melham, Peter Schrammel, and Michael Tautschnig. Effective verification of low-level software with nested interrupts. In the Europe Conference & Exhibition on Design, Automation & Test, 2015, pp. 229–234.
39. Suvam Mukherjee, Arun Kumar, and Deepak D’Souza. Detecting all high-level dataraces in an RTOS kernel. Lecture Notes in Computer Science, vol. 10145, 2017, pp. 405–423.
40. Nikita Chopra, Rekha Pai, and Deepak D’Souza. Data races and static analysis for interrupt-driven kernels. Lecture Notes in Computer Science, vol. 11423, 2019, pp. 697–723.
41. Jia-Ju Bai, Julia Lawall, Qiu-Liang Chen, and Shi-Min Hu. Effective static analysis of concurrency use-after-free bugs in Linux device drivers. In the USENIX Annual Technical Conference, 2019, pp. 255–268.
42. Dirk Beyer, Marie-Christine Jakobs, Thomas Lemberger, and Heike Wehrheim. Reducer-based construction of conditional verifiers. In Proceedings of the 40th International Conference on Software Engineering, 2018, pp. 1182–1193.
Рецензия
Для цитирования:
Андрианов П.С. Анализ корректности синхронизации компонентов ядра операционных систем. Труды Института системного программирования РАН. 2019;31(5):203-232. https://doi.org/10.15514/ISPRAS-2019-31(5)-16
For citation:
Andrianov P.S. Analysis of correct synchronization of operating system components. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2019;31(5):203-232. (In Russ.) https://doi.org/10.15514/ISPRAS-2019-31(5)-16