• Table of contents
• Formalizing Safety Rules 2
  • Understanding and Informal Description of the Rule
  • Development of the Rule Model
    • Rule Model Description
    • Developing Aspect Rule Models
    • Model Comments
  • Test Development
    • Common Notes
    • Test Driver
    • Test Task
    • Choosing the Linux Kernel
    • Regression Testing
  • Verification of Linux Kernel Drivers
  • Creating Final Account

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.

Development of the Rule Model¶

Rule Model Description¶

All rule models are described in $LDV_TOOLS_SRC/kernel-rules/model-db.xml. So that the most easy way to add one more rule model is to copy description of the existing one (e.g. "100_1a") and to update some information in this description.

There is a <model> XML element for each rule model. The identifier of the model is declared by ''id'' attribute. Most likely the identifier of the new rule model will be in form: identifier of the rule concatenated with ''_1a''.

Child elements of the <model> element include:

• rule – identifier of the rule. There can be several models for the same rule.
• status – status of readiness. ''public'' means it is ready for public use, other values (e.g., ''default'' or ''private'') mean it is not recommended for some reasons. You should use ''private'' during development
• kind – kind of the model. ''aspect'' means the model is defined with CIF aspects, ''plain'' means it is defined as a library. You should use ''aspect'' kind.
• error – error label. For now, it must be LDV_ERROR.
• engine - a verifier to be used for analysis. You should use ''blast''.
• description – informal description of the model. Optional, usually used if there are several models for the same rule. So you may not fill it.
• files - list of relative to $LDV_TOOLS_SRC/kernel-rules files defining the model. It contains the following child elements (for ''aspect'' models):
  • aspect – a file containing CIF advices that are applied to all source files of a driver under analysis (this file contains an actual definition of the model, see below).
  • config – a config file. It should be models/config-tracers.h for new rule models.
• hints – hints to a verifier such as extra options to be used for this particular model. Most likely you need to leave this element empty.

An example of the model element:

<model id="100_1a">
    <rule>0100</rule>
    <status>public</status>
    <kind>aspect</kind>
    <error>LDV_ERROR</error>
    <engine>blast</engine>
    <description></description>
    <files>
        <aspect>./models/model0100.aspect</aspect>
        <config>./models/config-tracers.h</config>
    </files>
    <hints></hints>
</model>

Developing Aspect Rule Models¶

Developing Aspect Rule Models

Model Comments¶

Model comments are used by error trace visualizer to highlight important elements of error traces produced by a verifier. It makes analysis of error traces much easier, so it is highly recommended to write model comments from the very beginning. The comments should be short but it should clearly express corresponding situation. For example, comments to ldv_assert should explain what is a problem detected.

You can use one of the following kinds of model comments:

• LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name=''function name to match with'') - describes a model function. The name argument is mandatory. Its value should be equal to a model function name defined at the following line.
• LDV_COMMENT_ASSERT - describes what is a problem detected if the assertion failed.
• LDV_COMMENT_CHANGE_STATE - decribes changes in model state.
• LDV_COMMENT_RETURN - describes a returned value of a model function.
• LDV_COMMENT_OTHER - is used to describe any other interesting elements of a model.

Model comments are written as usual C comments, for example:

/* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name=''ldv_check_alloc_flags'') Check that a memory allocating function was called with a correct value of flags in spin locking. */
void ldv_check_alloc_flags(gfp_t flags)
{
  /* LDV_COMMENT_ASSERT If spinlock is locked then a memory allocating function should be called with GFP_ATOMIC flag set. */
  ldv_assert(ldv_spin == LDV_SPIN_UNLOCKED || flags & GFP_ATOMIC);
}

/* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name=''ldv_spin_lock'') Lock spinlock. */
void ldv_spin_lock(void)
{
  /* LDV_COMMENT_CHANGE_STATE Lock spinlock. */
  ldv_spin = LDV_SPIN_LOCKED;
}

Test Development¶

Common Notes¶

Do not pay too much attention to tests. Tests just should show that you are developing the rule model in the proper way. Your actual purpose is described in the next Section.

To create tests for a new rule model you can simply copy existing tests for other rule model.

Tests for rule models should be placed to $LDV_TOOLS_SRC/ldv-tests/rule-models/:

• Test drivers are placed to subdirectories of $LDV_TOOLS_SRC/ldv-tests/rule-models/drivers. These subdirectories are to be named in accordance with the rule model identifiers, e.g. $LDV_TOOLS_SRC/ldv-tests/rule-models/drivers/08_1a. Inside these subdirectories test should be placed to subdirectories which names start with ''test-''.
• Test tasks are placed to files starting with ''regr-task'' in $LDV_TOOLS_SRC/ldv-tests/rule-models/. Be careful, after merging your branch to the master branch of LDV tools all test tasks starting with ''regr-task'' will be automatically added to QA night test task (regr-tests/test-sets/medium). New tests should be passed, so test them carefully before merging.

Test Driver¶

Each test driver consists of Makefile and a set of C and H source files. Each driver should be compatible with a kernel it is developed for.

Состоит из набора исходных кодов .c, .h файлов и Makefile. Драйвер должен компилироваться с тем ядром, для которого он предназначен. В Makefile указывается директива obj-m, определяющая собираемые модули (файлы .ko).

Называйте модули согласно вердикту: начинайте название с U где результат должен быть unsafe, и с S — где safe. Если срабатывание ложное — добавляйте букву F (например, "FU" или "FS").
    Создав несколько .c файлов с кодом, можно запустить скрипт drivers/gen_makefile.pl, чтобы автоматически сгенерировать Makefile драйвера с модулем .ko на каждый сишник .c.
    Повторю, основной критерий качества тестов на функцию: если функция вовсе не инструментируется, то хотя бы один из её тестов должен провалиться. В модели 08_1 на каждую функцию написано три теста: 0, 1 и 2 вызова (только 1 вызов — правильный, safe).
    Несколько папок с тестами нужны для возможности их отдельного запуска. Дело в том, что API ядра меняется, и, если в один архив попадут много тестов на разные функции, то с большой вероятностью этот драйвер будет пригоден для тестирования только с одним ядром. Поэтому для существенно разных функций имеет смысл делать разные папки с драйверами (особенно, если эти функции появились в какой-то определённой версии ядра!).

Test Task¶

Для первого запуска регрессионных тестов вам необходимо сформировать файл задания, где описано хотя бы минимум то, что вы хотите запускать (см. далее Первая часть). После первого запуска надо будет разобраться с полученными результатами (автоматически будет сформирована Вторая часть) и, если все правильно, то можно поменять исходный файл с заданием на сгенерированный.

Файл задания состоит из записей вида

driver=08_1--test-nonseek.tar.bz2;origin=external;kernel=linux-2.6.37;model=08_1;module=drivers/08_1/test-nonseek/S-nonseek-alone-test.ko;main=ldv_main0_sequence_infinite_withcheck_stateful;verdict=safe

Первая часть переменных описывает параметры запуска

driver=08_1--test-nonseek.tar.bz2;origin=external;kernel=linux-2.6.37;model=08_1

driver имя архива драйвера, формируется по именам папок от drivers/ с заменой "/" на "--". Например 08_1--test-nonseek.tar.bz2 лежит в drivers/08_1/test-nonseek/.
    origin
        external - внешний драйвер (для модельных тестов, как правило, будет указан данный вид драйверов)
        kernel - внутренний драйвер 
    kernel - версия ядра
    model - идентификатор модели

Вторая часть описывает ожидаемый результат (ее можно не описывать в самом начале)

module=drivers/08_1/test-nonseek/S-nonseek-alone-test.ko;main=ldv_main0_sequence_infinite_withcheck_stateful;verdict=safe

module - модуль драйвера
    main - имя сгенерированной точки входа
    verdict - полученный по результатам верификации вердикт

В том случае, если вердикт unknown, в дополнительных полях показывается, какой инструмент упал и перечисляются выявленные проблемы:

verdict=unknown;RCV_status=fail;problems=Blocks_SAT,Exception

Choosing the Linux Kernel¶

Ядро для тестирования рекомендуется выбирать на основе уже имеющихся в репозитории (дабы не раздувать размеры репозитория).

Имеющиеся версии можно посмотреть здесь:

ldv-tests/regr-tests/test-sets/big/
        linux-2.6.31.6.tar.bz2
        linux-2.6.32.15.tar.bz2
        linux-2.6.34.tar.bz2 
    ldv-tests/rule-models
        linux-2.6.37.tar.bz2
        linux-3.5.tar.bz2

В будущем планируется сделать систему автоматической загрузки нужных версий ядра из локального или одного из глобальных хранилищ. Тогда можно будет себя не ограничивать в выборе версий ядер.
Запуск тестов и анализ результатов

Для начала тесты нужно установить:

prefix=/path/to/your/installation/directory make install-testing

где /path/to/your/installation/directory - путь к установленному ldv-tools. После этого архивы с установленными тестами появятся в директории /ldv-tests/rule-models/. Там же будет лежать и ваш файл задания.

Regression Testing¶

First of all you need to create an empry working directory. Then you need to move to it and run the following command (path to LDV tools executables should be added to $PATH environment
Для запуска следует создать рабочую папку, перейти в неё и выполнить следующую команду:

rm -rf * && LDV_DEBUG=100 LDVDBTEST=ldvdb LDVUSERTEST=ldvreports regr-test.pl --test-set /home/shchepetkov/ldv/ldv-tests/rule-models/regr-task-118_1a

где:

rm -rf * - удаляет все файлы и папки из рабочей директории, возможно оставшиеся после предыдущего запуска. Рабочая папка перед запуском должна быть пустая! 

LDVDBTEST=ldvdb LDVUSERTEST=ldvreports - переменные окружения, указывающие на пользователя и базу данных. Подставьте сюда свои значения. Учтите, в результате из этой базы удалятся результаты всех предыдущих запусков!

regr-test.pl - скрипт, отвечающий за запуск тестов. Его содержимое можно посмотреть тут: /bin/regr-test.pl

--test-set /home/shchepetkov/ldv/ldv-tests/rule-models/regr-task-118_1a - тут задаётся абсолютный путь до файла с заданием. --test-set <name> - одна из опция запуска скрипта, как раз указывающая на файл с заданием. Чтобы посмотреть остальные доступные опции, следует выполнить команду:

regr-test.pl --help

Итак, по окончанию запуска результаты буду залиты на сервер статистики. Так же в папке появятся файлы и директории, которые создаёт скрипт регрессионного тестирования:

ls -1

current.sorted
 launcher-results-dir
 launcher-working-dir
 original.sorted
 regr-task-new
 regr-test.diff
 work

Тут нам будут интересны 3 файла - original.sorted, current.sorted и regr-test.diff. Первый - ваш отсортированный тест задания. Второй - это тест задания, сгенерированный скриптом regr-test.pl автоматически на основе результатов запуска. Если ожидаемые результаты не сходятся с фактическими, то разница будет записана в третий файл - regr-test.diff. В этом случае его необходимо посмотреть, понять в чем проблема и исправить её. Если же файл пустой, то тесты успешно проёдены.

Для большего удобства анализирования результатов можно установить стороннюю программу meld. Она занимается сравниванием содержимого текстовых файлов. Команда:

meld current.sorted original.sorted

покажет вам различие между этими файлами. Получается гораздо нагляднее и быстрее, чем если просто смотреть regr-test.diff.

Verification of Linux Kernel Drivers¶

TBD.

Creating Final Account¶

TBD.