Project

General

Profile

Formalizing Safety Rules 2 » History » Version 2

Evgeny Novikov, 07/30/2013 11:24 AM

1 1 Evgeny Novikov
h1. Formalizing Safety Rules 2
2
3
Before starting formalizing safety rules you need to create an account at this site. The name of this account should be sent to managers of the LDV project, e.g. via e-mail. Then somebody will add you to developers of the LDV project and you will be able to create and to update feature requests and bug reports "here":http://forge.ispras.ru/projects/ldv-rules/issues. 
4
5
Formalizing safety rules consists of following activities that can be fully or partially repeated several times.
6
7
h2. Understanding and informal description of the rule
8
9
Just one time per each rule you need to reserve a rule identifier by creating a feature request "here":http://forge.ispras.ru/projects/ldv-rules/issues. The rule identifier is a number. This number should be greater by one then the maximum of already reserved numbers. Note that you won''t be able to change the rule identifier. 
10
11 2 Evgeny Novikov
To understand the rule you need to:
12
* Read available documentation of the relevant kernel core API, e.g. "here":https://git.kernel.org/cgit/linux/kernel/git/torvalds/linux.git/tree/Documentation or in books like "LDD3":http://lwn.net/Kernel/LDD3.
13
* Explore source code, especially relevant header files, of the Linux kernel. For navigation through Linux kernel source code you may use http://lxr.linux.no or http://lxr.free-electrons.com.
14
* Analyze existing violations of the given rule. You may use the Internet or https://git.kernel.org/cgit/linux/kernel/git/torvalds/linux.git for this purpose.
15
* Analyze verification results that you will obtained at one of the following steps.
16
* Discuss it with developers of the LDV project, if nothing else helps.
17 1 Evgeny Novikov
18 2 Evgeny Novikov
Each time after understanding more details about the rule, you should update informal description of the rule, that includes:
19
* Short name, that should be a part of the name of the feature request you have created before.
20
* Summary, that should outline the essense of the rule.
21
* Detailed description, that should clearly describe all incorrect usages of the relevant kernel core API.
22
* Links to existing violations of the rule. Also it would be greate to provide some short description of each violation, since they may be rather hard for understanding.
23
* Some auxiliary information like absence of required functionality in LDV tools to formalize or/and to check some part of the rule.
24
25
You can find an example of a good description of a rule "here":http://linuxtesting.org/ldv/online?action=show_rule&rule_id=0032. But nobody prevent you from creating a much better description.