Formalizing Safety Rules 2¶

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.

Formalizing safety rules consists of following activities that can be fully or partially repeated several times.

Understanding and informal description of the rule¶

Just one time per each rule you need to reserve a rule identifier by creating a feature request here. 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.

To understand the rule you need to:

• Read available documentation of the relevant kernel core API, e.g. here or in books like LDD3.
• 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.
• 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.
• Analyze verification results that you will obtained at one of the following steps.
• Discuss it with developers of the LDV project, if nothing else helps.

Each time after understanding more details about the rule, you should update informal description of the rule, that includes:

• Short name, that should be a part of the name of the feature request you have created before.
• Summary, that should outline the essense of the rule.
• Detailed description, that should clearly describe all incorrect usages of the relevant kernel core API.
• 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.
• Some auxiliary information like absence of required functionality in LDV tools to formalize or/and to check some part of the rule.

You can find an example of a good description of a rule here. But nobody prevent you from creating a much better description.