Конфигурируемый метод поиска состояний гонок в операционных системах с использованием предикатных абстракций
https://doi.org/10.15514/ISPRAS-2016-28(6)-5
Аннотация
В статье представлен конфигурируемый метод для поиска состояний гонок. Метод позволяет настраивать требуемую точность анализа, выбирая баланс между затрачиваемыми ресурсами и количеством ложных предупреждений подключением двух расширений: уточнением путей на основе предикатных абстракций и анализом потоков. Метод основан на алгоритме Lockset и использует упрощенную модель памяти для уменьшения количества ложных предупреждений. Предлагаемый подход был реализован в инструменте CPALockator, который был апробирован на модулях ядра операционной системы Linux, что позволило обнаружить несколько состояний гонок, которые были признаны и исправлены разработчиками.
Об авторах
П. С. Андрианов
Институт системного программирования РАН
Россия
Россия
В. С. Мутилин
Институт системного программирования РАН
Россия
Россия
А. В. Хорошилов
Институт системного программирования РАН; Московский государственный университет имени М.В. Ломоносова; Московский физико-технический институт (государственный университет); Национальный исследовательский университет «Высшая школа экономики»
Россия
Россия
Список литературы
1. Мутилин В.С., Новиков Е.М., Хорошилов А.В. Анализ типовых ошибок в драйверах операционной системы Linux. Труды ИСП РАН, том 22, 2012 г., стр. 349-374. DOI: 10.15514/ISPRAS-2012-22-19
2. Nancy Levenson, Safeware: System Safety and Computers, 1995
3. Nachum Dershowitz, Software horror stories, http://www.cs.tau.ac.il/~nachumd/pub.html
4. Cordeiro, L., Fischer, B.: Verifying Multi-Threaded Software using SMT-based Context-Bounded Model Checking. In: ICSE, pp. 331-340 (2011)
5. E. Clarke, D. Kroening, N. Sharygina, K. Yorav. SATABS: SAT-based predicate abstraction for ANSI-C. Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'05), pp. 570-574, 2005.
6. A. Gupta, C. Popeea, A. Rybalchenko. Predicate abstraction and refinement for verifying multi-threaded programs In Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2011), pp. 331-344, 2011.
7. A. Gupta, C. Popeea, A. Rybalchenko. Threader: a constraint-based verifier for multi-threaded programs In Proceedings of the 23rd International Conference on Computer Aided Verification (CAV 2011), LNCS, vol. 6806, pp. 412-417, 2011.
8. Stefan Savage, Michael Burrows, Greg Nelson, Patric Sobalvarro, Thomas Anderson Eraser: A Dynamic Data Race Detector for Multithreaded Programs ACM Transactions on Computer Systems, Vol. 15, No. 4, November 1997, Pages 391-411.
9. Dirk Beyer, Thomas A. Henzinger, and Gregory Theoduloz, Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis, ACM Transactions on Computer Systems, Vol. 15, No. 4, November 1997, Pages 391-411.
10. Андрианов П.С., Мутилин В.С., Хорошилов А.В. Метод легковесного статического анализа для поиска состояний гонок. Труды ИСП РАН, том 27, вып. 5, 2015 г., стр. 87-116. DOI: 10.15514/ISPRAS-2015-27(5)-6
11. Dirk Beyer , M. Erkan Keremoglu , Philipp Wendler, Predicate abstraction with adjustable-block encoding, Proceedings of the 2010 Conference on Formal Methods in Computer-Aided Design, October 20-23, 2010, Lugano, Switzerland
12. Мандрыкин М.У., Мутилин В.С., Хорошилов А.В. Введение в метод CEGAR - уточнение абстракции по контрпримерам. Труды ИСП РАН, том 24, 2013, стр. 219-292. DOI: 10.15514/ISPRAS-2013-24-12
13. Shostak R., Deciding Combinations of Theories, Journal of the ACM, 1-12, 1984
14. Beyer Dirk, Zuerey Damien, Majumdar Rupak., Csisat: Interpolation for la+euf, CAV, 304-308, 2008
15. Bruttomesso Roberto, Cimatti Alessandro, Franzen Anders, Griggio Alberto, Sebastiani Roberto., The mathsat 4 smt solver, CAV, 299-303, 2008
16. Alexey Khoroshilov, Mikhail Mandrykin, Vadim Mutilin, Eugene Novikov, Alexander Petrenko, Ilya Zakharov. Configurable toolset for static verification of operating systems kernel modules. Programming and Computer Software, vol. 41, № 1, 2015, pp. 49-64. DOI: 10.1134/S0361768815010065
17. Alexey Khoroshilov, Mikhail Mandrykin, Vadim Mutilin, Eugene Novikov, Pavel Shved. Using Linux Device Drivers for Static Verification Tools Benchmarking. Programming and Computer Software, vol. 38, № 5, 2012, pages 245-256. DOI: 10.1134/S0361768812050039
18. Alexey Khoroshilov,Vadim Mutilin, Ilya Zakharov. Pattern-based environment modeling for static verification of Linux kernel modules. Programming and Computer Software, vol. 41, № 3, 2015, pages 183-195. DOI: 10.1134/S036176881503007X
Рецензия
Для цитирования:
Андрианов П.С., Мутилин В.С., Хорошилов А.В. Конфигурируемый метод поиска состояний гонок в операционных системах с использованием предикатных абстракций. Труды Института системного программирования РАН. 2016;28(6):65-86. https://doi.org/10.15514/ISPRAS-2016-28(6)-5
For citation:
Andrianov P.S., Mutilin V.S., Khoroshilov A.V. Adjustable method with predicate abstraction for detection of race conditions in operating systems. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2016;28(6):65-86. (In Russ.) https://doi.org/10.15514/ISPRAS-2016-28(6)-5
Послать статью по эл. почте 