DocumentCode :
3713208
Title :
Towards deductive verification of concurrent Linux kernel code with Jessie
Author :
Mikhail Mandrykin;Alexey Khoroshilov
Author_Institution :
ISP RAS, Moscow, Russia
fYear :
2015
Firstpage :
5
Lastpage :
10
Abstract :
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.
Keywords :
"Linux","Kernel","Synchronization","Concurrent computing","Cognition","Semantics","Context"
Publisher :
ieee
Conference_Titel :
Computer Science and Information Technologies (CSIT), 2015
Type :
conf
DOI :
10.1109/CSITechnol.2015.7358240
Filename :
7358240
Link To Document :
بازگشت