Towards Deductive Verification of C Programs with Shared Data
https://doi.org/10.15514/ISPRAS-2015-27(4)-4
Abstract
The paper takes a look at the problem of deductive verification of Linux kernel code that is concurrent and accesses shared data. The presence of shared data does not allow to apply traditional deductive verification techniques, so we consider how to verify such code using proof of its compliance to a specification of a synchronization discipline. The approach is demonstrated on examples of spinlock specification and a simplified specification of RCU (Read-copy-update) API.
About the Authors
M. U. Mandrykin
ISP RAS
Russian Federation
Russian Federation
A. V. Khoroshilov
ISP RAS; Lomonosov Moscow State University, 2nd Education Building, Faculty CMC, GSP-1; Moscow Institute of Physics and Technology; Higher School of Economics, National Research University
Russian Federation
Russian Federation
References
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. Uni-versité 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: AN-SI/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 prov-ers”, 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 Hei-delberg, January, 2011.
12. A. Riazanov, A. Voronkov, “The design and implementation of Vampire”, In AI commu-nications, 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.
Review
For citations:
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
Email this article 