Метод легковесного статического анализа для поиска состояний гонок
https://doi.org/10.15514/ISPRAS-2015-27(5)-6
Аннотация
В этой статье представлен подход легковесного статического анализа к поиску состояний гонок, названный CPALockator. Он учитывает такую специфику ядер операционных систем, как сложный параллелизм и особые примитивы синхронизации. Метод основан на алгоритме Lockset, но использует две эвристики, которые призваны уменьшить количество ложных предупреждений: модель памяти и модель параллелизма. Основным предметом нашего исследования являются ядра операционных систем, но предложенный подход может быть применен также и для других программ.
Об авторах
П. С. Андрианов
ИСП РАН
Россия
Россия
В. С. Мутилин
ИСП РАН
Россия
Россия
А. В. Хорошилов
ИСП РАН; ВМК МГУ; Московский физико-технический институт (государственный университет); НИУ ВШЭ
Россия
Россия
Список литературы
1. Lanyue Lu, Andrea C. Arpaci-Dusseau, Remzi H. Arpaci-Dusseau, Shan Lu, A Study of Linux File System Evolution, 11th USENIX Conference on File and Storage Technologies (FAST ’13)
2. Мутилин В.С., Новиков Е.М., Хорошилов А.В. Анализ типовых ошибок в драйверах операционной системы Linux. Труды ИСП РАН, том 22, C. 349-374, 2012.
3. 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.
4. Герлиц Е.А., Кулямин В.В., Максимов А.В., Петренко А.К., Хорошилов А.В., Цыварев А.В. Тестирование операционных систем. Труды ИСП РАН, том 26, C. 73-107, 2014.
5. John Erickson, Madanlal Musuvathi, Sebastian Burckhardt, Kirk Olynyk. Effective Data-Race Detection for the Kernel Operating System Design and Implementation (OSDI’10), 2010, USENIX.
6. Thomas Witkowski, Nicolas Blanc, Daniel Kroening, Georg Weissenbacher. Model checking concurrent linux device drivers. ASE'07, Proceedings of the twenty-second IEEE/ACM international conference on Automated software engineering, pp 501-504, ACM, New York, NY, USA, 2007.
7. Polyvios Pratikakis, Jeffrey S. Foster, Michael Hicks. Locksmith: Practical Static Race Detection for C, ACM Transactions on Programming Languages and Systems (TOPLAS), vol. 33(1):Article 3, January 2011.
8. Polyvios Pratikakis, Jeffrey S. Foster, Michael Hicks. Locksmith: Context-Sensitive Correlation Analysis for Race Detection, Proceedings of the 2006 ACM SIGPLAN conference on Programming language design and implementation, pp. 320 - 331, ACM New York, 2006
9. Thomas Witkowski, Nicolas Blanc, Daniel Kroening, Georg Weissenbacher, Model Checking Concurrent Linux Device Drivers, ASE’07, November 4-9, 2007.
10. 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.
11. Daniel Wonisch, Block Abstract Memorization for CPAchecker, TACAS 2012, LNCS 7214, pp. 531-533.
12. Мутилин В.С., Новиков Е.М., Страх А.В., Хорошилов А.В., Швед П.Е. Архитектура Linux Driver Verification. Труды ИСП РАН, том 20, 2011. С. 163-187.
13. Cordeiro, L., Fischer, B.: Verifying Multi-Threaded Software using SMT-based Context-Bounded Model Checking. In: ICSE, pp. 331-340 (2011)
14. 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.
15. CBMC A Tool for Checking ANSI-C Programs, Armin Biere, Alessandro Cimatti, Edmund M. Clarke, and Yunshan Yhu. Symbolic model checking without BDDs. In Tools and Algorithms for Construction and Analysis of Systems, pages 193-207, 1999.
16. E. Clarke, O. Grumberg, S. Jha, Y. Lu, H. Veith. Counterexample-Guided Abstraction Refinement. Proceedings of the 12th International Conference on Computer Aided Verification (CAV '00), pp. 154-169, 2000.
17. Хорошилов А.В., Мандрыкин М.У., Мутилин В.С. Введение в метод CEGAR - уточнение абстракции по контрпримерам. Труды ИСП РАН, том 24, С. 219-292, 2013.
18. Gerard Basler, Michele Mazzucchi1, Thomas Wahl, Daniel Kroening. Symbolic Counter Abstraction for Concurrent Software CAV '09 Proceedings of the 21st International Conference on Computer Aided Verification, pp. 64-78, Springer-Verlag, Berlin, Heidelberg, 2009.
19. 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.
20. 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.
21. C. Popeea, A. Rybalchenko. Threader: a verifier for multi-threaded programs In Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2013), LNCS, vol. 7795, pp. 633-636, 2013.
22. A. Malkis, A. Podelski, A. Rybalchenko. Thread-modular counterexample-guided abstraction refinement, SAS'10 Proceedings of the 17th international conference on Static analysis, pp. 356-372, Springer-Verlag, Berlin, Heidelberg, 2010.
23. S. Qadeer, D. Wu. KISS: Keep it simple and sequential. Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '04), pp. 14 - 24, 2004.
24. I. Rabinovitz and O. Grumberg. Bounded model checking of concurrent programs. In Conf. on Computer-Aided Verification (CAV), pages 82-97, 2005.
25. M. Musuvathi and S. Qadeer. Iterative context bounding for systematic testing of multithreaded programs. In PLDI, pages 446-455, 2007.
26. M. K. Ganai and A. Gupta. Efficient modeling of concurrent systems in BMC. In Intl. SPIN Workshop on Model Checking Software, pages 114-133, 2008.
27. Shuvendu K. Lahiri, Shaz Qadeer, and Zvonimir Rakamaric. Static and Precise Detection of Concurrency Errors in Systems Code Using SMT Solvers. CAV '09 Proceedings of the 21st International Conference on Computer Aided Verification, pp 509-524, Springer-Verlag Berlin, Heidelberg, 2009
28. R. DeLine, K.R.M. Leino. BoogiePL: A typed procedural language for checking object-oriented programs. Technical Report MSR-TR-2005-70, Microsoft Research, 2005.
29. Naghmeh Ghafari1, Alan J. Hu, and Zvonimir Rakamaric. Context-bounded translations for concurrent software: an empirical evaluation. SPIN'10 Proceedings of the 17th international SPIN conference on Model checking software, pp. 227-244, Springer-Verlag Berlin, Heidelberg, 2010
30. S. La Torre, P. Madhusudan, G. Parlato. Analyzing Recursive Programs Using a Fixed-point Calculus. Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '09), pp. 211-222, 2009.
31. Gerard Charly Basler, Model Checking Boolean Programs, abhandlung zur Erlangung des titels Doktor der Wissenschaften der ETH Zurich, 28 October 1978.
32. S. La Torre, P. Madhusudan, G. Parlato. Reducing Context-Bounded Concurrent Reachability to Sequential Reachability. Proceedings of the 21st International Conference on Computer Aided Verification (CAV '09), LNCS 5643, pp. 477-492, 2009.
33. Jan Wen Voung, Ranjit Jhala, Sorin Lerner, RELAY: Static Race Detection on Millions of Lines of Code. ESEC/FSE’07, 2007
34. Kahlon V., Yang Y., Sankaranarayanan S., Gupta A.: Fast and accurate static data-race detection for concurrent programs. In: CAV’07. LNCS, vol. 4590, pp. 226-239. Springer (2007)
35. Vineet Kahlon, NishantSinha, Yun Zhang. Static data race detection for concurrent programs with asynchronous calls. ESEC/FSE '09 Proceedings of the the 7th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering, pp. 13-22 ACM New York, NY, USA, 2009
36. B. Steensgaard. Points-to analysis in almost linear time. Proceedings of the 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '96), pp. 32-41, 1996
Рецензия
Для цитирования:
Андрианов П.С., Мутилин В.С., Хорошилов А.В. Метод легковесного статического анализа для поиска состояний гонок. Труды Института системного программирования РАН. 2015;27(5):87-116. https://doi.org/10.15514/ISPRAS-2015-27(5)-6
For citation:
Andrianov P.S., Mutilin V.S., Khoroshilov A.V. Lightweight Static Analysis for Data Race Detection in Operating System Kernels. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2015;27(5):87-116. (In Russ.) https://doi.org/10.15514/ISPRAS-2015-27(5)-6
Послать статью по эл. почте 