О дедуктивной верификации Си программ, работающих с разделяемыми данными
https://doi.org/10.15514/ISPRAS-2015-27(4)-4
Аннотация
В статье рассматривается задача дедуктивной верификации кода ядра ОС Linux, написанного на языке Си и выполняющегося в окружении с высокой степенью параллелизма. Существенной особенностью этого кода является наличие работы с разделяемыми данными, что не позволяет применять классические методы дедуктивной верификации. Для преодоления этих сложностей в работе представлены предложения по формированию подхода к спецификации и верификации кода, работающего с разделяемыми данными, основанные на доказательстве соответствия этого кода заданной спецификации некоторой дисциплины синхронизации. Подход иллюстрируется примерами упрощенной модели спецификации спин-блокировок и внешнего интерфейса механизма синхронизации RCU (Read-copy-update), широко используемого в ядре ОС Linux.
Об авторах
М. У. Мандрыкин
ИСП РАН
Россия
Россия
А. В. Хорошилов
ИСП РАН; МГУ имени М.В. Ломоносова, 2-й учебный корпус, факультет ВМК; Московский физико-технический институт (государственный университет); НИУ ВШЭ
Россия
Россия
Список литературы
1. http://linuxtesting.org/astraver.
2. P. Cuoq, F. Kirchner, N. Kosmatov, V. Prevosto, J. Signoles, B. Yakobowski, “FRAMA-C, A Software Analysis Perspective”, Proceedings of International Conference on Software Engineering and Formal Methods 2012 (SEFM’12), October 2012.
3. L. Correnson, Z. Dargaye, A. Pacalet, “WP (Draft) Manual”',
4. http://frama-c.com/download/frama-c-wp-manual.pdf.
5. Y. Moy. Automatic Modular Static Safety Checking for C Programs: Ph.D. Thesis. Université Paris-Sud. - 2009. - January. http://www.lri.fr/~marсhe/moy09phd.pdf.
6. http://kerneis.github.io/cil/doc/html/cil/.
7. P. Baudin, J.-C. Filliâtre, C. Marché, B. Monate, Y. Moy, V. Prevosto, “ACSL: ANSI/ISO C Specification Language. Version 1.7”, http://frama-c.com/download/acsl.pdf.
8. F. Bobot, J.-C. Filliâtre, C. Marché, A. Paskevich, “Why3: Shepherd your herd of provers”, Boogie 2011: First International Workshop on Intermediate Verification Languages, 2011.
9. J.-C. Filliâtre, A. Paskevich,“Why3 - where programs meet provers'', In Programming Languages and Systems, pp. 125-128, Springer Berlin Heidelberg, 2013.
10. L. De Moura, N. Bjørner, “Z3: An efficient SMT solver”', In Tools and Algorithms for the Construction and Analysis of Systems, pp. 337-340, Springer Berlin Heidelberg, 2008.
11. C. Barrett, C. L. Conway, M. Deters, L. Hadarean, D. Jovanović, T. King, A. Reynolds, C. Tinelli, “CVC4”, In Computer aided verification, pp. 171-177, Springer Berlin Heidelberg, January, 2011.
12. A. Riazanov, A. Voronkov, “The design and implementation of Vampire”, In AI communications, vol. 15(2, 3), pp. 91-110, 2002.
13. S. Schulz. “System Description: E 1.8”', In Proceedings of the 19th LPAR, Stellenbosch, pp. 477-483, LNCS 8312, Springer Verlag, 2013.
14. Y. Bertot, P. Castéran, “Interactive theorem proving and program development: Coq'Art: the calculus of inductive constructions”', Springer Science & Business Media, 2013.
15. S. Owre, S. Rajan, J. M. Rushby, N. Shankar, M. Srivas, “PVS: Combining Specification, Proof Checking, and Model Checking”', In proceedings of Computer-Aided Verification '96, pp. 411-414, 1996.
16. T. Hubert, C. Marché, “Separation analysis for deductive verification”', In Heap Analysis and Verification, Braga, Portugal, March, 2007.
17. J.-P. Talpin, P. Jouvelot, “Polymorphic type region and effect inference”, Technical Report EMP-CRI E/150, 1991.
18. M. Mandrykin, A. Khoroshilov, “High level memory model with low level pointer cast support for Jessie intermediate language”, In Programming and Computer Software, Vol. 41, No. 4, pp. 197-208, 2015.
19. P. E. McKenney, J. Appavoo, A. Kleen, O. Krieger, R. Russell, D. Sarma, M. Soni, “Read-copy update”, In AUUG Conference Proceedings, p. 175, 2001.
20. C. Flanagan, S. N. Freund, S. Qadeer, “Thread-modular verification for shared-memory programs”, In ESOP 2002, Number 2305 in LNCS, Springer, pp. 262-277, 2002.
21. E. Cohen, M. Dahlweid, M. Hillebrand, D. Leinenbach, M. Moskal, T. Santen, W. Schulte, S. Tobies, “VCC: A practical system for verifying concurrent C”, In Theorem Proving in Higher Order Logics, pp. 23-42, Springer Berlin Heidelberg, 2009.
22. E. Cohen, M. Moskal, S. Tobies, W. Schulte, “A precise yet efficient memory model for C”, In Electronic Notes in Theoretical Computer Science, vol. 254, pp. 85-103. 2009.
23. E. Cohen, M. Moskal, W. Schulte, S. Tobies, “Local Verification of Global Invariants in Concurrent Programs”, In Computer Aided Verification, Springer Berlin Heidelberg, pp. 480-494, January, 2010.
24. E. Cohen, M. Moskal, W. Schulte, S. Tobies. “A practical verification methodology for concurrent programs”, Tech. Rep. MSR-TR-2009-15, Microsoft Research, 2009. (http://research.microsoft.com/pub)
25. J.-C. Filliâtre, C. Marché, “The Why/Krakatoa/Caduceus platform for deductive program verification”, In Proceedings of the 19th International Conference on Computer Aided Verification, Lecture Notes in Computer Science, Springer, 2007.
26. M. Moskal, W. Schulte, E. Cohen, M. A. Hillebrand, S. Tobies, “Verifying C programs: a VCC tutorial”', MSR Redmond, EMIC Aachen, 2012.
27. P.E. McKenney, S. Boyd-Wickizer, J. Walpole, “RCU usage in the Linux kernel: one decade later”, Technical report, 2013.
Рецензия
Для цитирования:
Мандрыкин М.У., Хорошилов А.В. О дедуктивной верификации Си программ, работающих с разделяемыми данными. Труды Института системного программирования РАН. 2015;27(4):49-68. https://doi.org/10.15514/ISPRAS-2015-27(4)-4
For citation:
Mandrykin M.U., Khoroshilov A.V. Towards Deductive Verification of C Programs with Shared Data. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2015;27(4):49-68. (In Russ.) https://doi.org/10.15514/ISPRAS-2015-27(4)-4
Послать статью по эл. почте 