Towards Deductive Verification of Concurrent Linux Kernel Code with Jessie

被引：0
作者：
Mandrykin, Mikhail [1 ]
Khoroshilov, Alexey [1 ]
机构：
[1] RAS, ISP, Moscow, Russia
来源：
TENTH INTERNATIONAL CONFERENCE ON COMPUTER SCIENCE AND INFORMATION TECHNOLOGIES REVISED SELECTED PAPERS CSIT-2015 | 2015年
关键词：
Verification; concurrency; ownership; invariants; C semantics; PROGRAMS;
D O I：
暂无
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
The paper considers the challenge of deductively verifying Linux kernel code written in C programming language with extensive use of low-level memory operations and interactions with the highly concurrent environment. The paper presents an initial approach to specification and verification of concurrent code working with shared data by proving the code's compliance with specified synchronization discipline. The proposal is illustrated with an example specifying a user-side simplified model of the read-copy-update synchronization mechanism widely used within the Linux kernel.
引用
收藏
页码：5 / 10
页数：6
相关论文
共 23 条
  • [1] [Anonymous], 2013, Technical report
  • [2] Barrett Clark, 2011, Computer Aided Verification. Proceedings 23rd International Conference, CAV 2011, P171, DOI 10.1007/978-3-642-22110-1_14
  • [3] Baudin P., Tech. rep
  • [4] Bertot Y., 2013, Interactive theorem proving and program development: CoqA'rt: the calculus of inductive constructions
  • [5] Bobot F., 2011, BOOG 2011 1 INT WORK
  • [6] COHEN E, 2009, ENTCS, V254, P85, DOI DOI 10.1016/J.ENTCS.2009.09.061
  • [7] COHEN E, 2009, MSRTR200915
  • [8] Cohen E, 2010, LECT NOTES COMPUT SC, V6174, P480, DOI 10.1007/978-3-642-14295-6_42
  • [9] Cohen E, 2009, LECT NOTES COMPUT SC, V5674, P23, DOI 10.1007/978-3-642-03359-9_2
  • [10] Correnson L., WP DRAFT MANUAL
123