Архитектура системы верификации кода драйверов Linux

Ахренеть. Этой игрушкой кто-то пользовался?

Пользовались. Вот ссылка, не будь совсем уж Ъ: http://linuxtesting.ru/results/ldv

> Пользовались. Вот ссылка, не будь совсем уж Ъ

Не петросянь. Я спрашиваю о том, есть ли на ЛОР живые юзеры этого LDV.

игрушка, кхм, как ты ее назвал, там, скорее, бласт — http://mtc.epfl.ch/software-tools/blast/index-epfl.php

а они, как мне показалось при чтении по диагонали, его подзаточили под ядро

кстати — емнип один из них тут имеет аккаунт на лоре, и даже че-то рассказывал, когда речь шла о емнип http://linuxtesting.ru/project/lsb_infrastructure

> игрушка, кхм, как ты ее назвал, там, скорее, бласт — http://mtc.epfl.ch/software-tools/blast/index-epfl.php

У них на странице прямо так и написано. Но мне интересно использование LDV для своих драйверов или Си-программ.

насчет живых — не знаю, а вообще есть

www.linux.org.ru/people/V_Rubanov/profile

Он исключительно молчалив %)

да я тоже заметил :-)

раз его скастовали сюда, наверно можно и второй раз скастовать

а вообще я сомневаюсь, что тут на лоре кроме тебя кто-то из драйверописателей интересуется формальной верификацией

Статистически анализ не надежен - какой прок в прогнозе что код с вероятностью NN правильный. А ведь надо еще доказать применимость статистических гипотез к конкретному коду.

Насколько я понял, это средство не только для драйверописателей.

насколько я понимаю, да

ладно, я прекращаю выступать в роли К.О., интересней почитать, че они там накрутили

> какой прок в прогнозе что код с вероятностью NN правильный

Никакого. Применение статистических методов не отменяет классического тестирования. Но хуже-то тоже не будет.

> (ИСП РАН) и Федерального агентства РФ по науке и инновациям

инновациям

Превед Медвед?

Круто

я интересуюсь

раз такое дело, сделал опрос: www.linux.org.ru/polls/polls/7001001

> Статистически анализ не надежен - какой прок в прогнозе что код с вероятностью NN правильный. А ведь надо еще доказать применимость статистических гипотез к конкретному коду

ты где там нашел статистические методы?

[вброс]

Как мне кажется, все эти версификаторы направлены на компенсацию убогости С\С++

[/вброс]

>Список выявленных при помощи LDV проблем можно посмотреть на данной странице.

Я не понял - три десятка багов за 2 года? Это драйвера такие хорошие или инструмент....?

Хы, я тоже написал «статистического» :)

> Как мне кажется, все эти версификаторы направлены на компенсацию убогости С\С++

после того, как доказан какой-то инвариант, например, что индекс не выходит за границы массива, можно (и нужно) нафиг выкинуть код, проверяющий это в рантайме, и тем ускорить исполнение

кроме того, можно не заставлять программиста тратить время — писать код обработки для ситуации, которая доказанно возникнуть не может

хотя, тут, не все так просто

Ну какие проблемы, вон, некоторые жаве проверки отключают на проде. Все равно такие фичи должны быть встроены в язык.

> Как мне кажется, все эти версификаторы направлены на компенсацию убогости С\С++

Как это ложится на проверки зависимостей? Когда что-то нужно сделать обязательно только после чего-то дрогого. Они, очень часто, чисто логические.

> все эти версификаторы направлены на компенсацию убогости

Скомпенсируй свою убогость - научись читать.

Институт РАН сделал что-то полезное, да к тому же для линукса?

Ущипните меня.

Ну и? Я за то, что бы системы верификации была частью языка, а не костылем. Чем язык лучше, тем у него больше встроенных средств обеспечения корректности. Хаскель, который тут любят - только цветочки.

Внезапно: ходил по ссылкам в теме, почитал их сайт. Они там нечто похожее на юнит-тесты на libc написали. Цирк.

> Ну какие проблемы, вон, некоторые жаве проверки отключают на проде. Все равно такие фичи должны быть встроены в язык.

Какие? Вызов метода/функции xxx обязательно делать только после вызова метода/функции yyy или метода/функции ййй? :)

>> Все равно такие фичи должны быть встроены в язык.

Какие? Вызов метода/функции xxx обязательно делать только после вызова метода/функции yyy или метода/функции ййй? :)

Почему нет?

> Внезапно: ходил по ссылкам в теме, почитал их сайт. Они там нечто похожее на юнит-тесты на libc написали. Цирк.

Походу, ты не совсем врубаешься. Юнит тесты - это ЧАСТЬ кода, работающая в коде предназначеном для тестирования.

Здесь ВЕСЬ код драйверов прокручивается на поиск противоречий в специальной среде, эти противоречия выявляющей.

>>> Все равно такие фичи должны быть встроены в язык.

Какие? Вызов метода/функции xxx обязательно делать только после вызова метода/функции yyy или метода/функции ййй? :)

Почему нет?

Потому что это только примитивнейшая зависимость. Можно, конечно, такие зависимости и более сложные в язык запихнуть, но только нет таких языков и не будет. Ибо для записи таких зависимостей нужен совсем другой язык, более для этого подходящий.

Это так тонко что даже подозрительно...

Не, мы про спецификации разного уровня говорим. Я вот высмеиваю верификаторы низкоуровневых спецификаций, вроде запрета на выход за границы массива.

> после того, как доказан какой-то инвариант, например, что индекс не выходит за границы массива, можно (и нужно) нафиг выкинуть код, проверяющий это в рантайме, и тем ускорить исполнение

При чём здесь формальный верификатор? Проверку инварианта на выход за границы массива должен делать компилятор. А если корректность инварианта зависит от среды исполнения, т.е. это нельзя доказать статически, то и рантаймовую проверку выкидывать нельзя.

> Не, мы про спецификации разного уровня говорим. Я вот высмеиваю верификаторы низкоуровневых спецификаций, вроде запрета на выход за границы массива.

В одних языках надо одно проверять. В других - другое. В общем объеме необходимых проверок - это ничего не значащая величина.

> то и рантаймовую проверку выкидывать нельзя.

Вообще-то, если среда не меняется в процессе работы, то можно. Вынести эти проверки на этап инициализации...

>> то и рантаймовую проверку выкидывать нельзя.

Вообще-то, если среда не меняется в процессе работы, то можно. Вынести эти проверки на этап инициализации...

От выноса проверки из цикла быть рантаймовой она не перестанет.

Кроме того, это тоже должен по-хорошему должны делать и внимательный программист, и компилятор. При чём здесь формальные верификаторы мне не понятно.

Раздел «Документация»?

>>> то и рантаймовую проверку выкидывать нельзя.

Вообще-то, если среда не меняется в процессе работы, то можно. Вынести эти проверки на этап инициализации...

От выноса проверки из цикла быть рантаймовой она не перестанет.

Только это будет уже на рантайм-проерка выхода за границы массива а рантайм-проверка на допустимост параметров системы.

Кроме того, это тоже должен по-хорошему должны делать и внимательный программист, и компилятор. При чём здесь формальные верификаторы мне не понятно.

Вот внимательность программиста и проверяется.

> это тоже должен по-хорошему должны делать и внимательный программист, и компилятор

Особенно убедительно выглядит про «внимательного программиста».

При чём здесь формальные верификаторы мне не понятно.

При том, что компилятор тоже может выполнять верификацию, и, следовательно, быть верификатором.

> Только это будет уже на рантайм-проерка выхода за границы массива а рантайм-проверка на допустимост параметров системы.

Это будет рантайм-проверка на то, выйдет ли указатель, по которому осуществляется доступ, за границы массива. То есть, по мне она так и останется «рантайм-проверкой на выход за границы массива», просто станет более умной. :-) В любом случае, это уже проблемы терминологии.

Кроме того, это тоже должен по-хорошему должны делать и внимательный программист, и компилятор. При чём здесь формальные верификаторы мне не понятно.

Вот внимательность программиста и проверяется.

Вы про что? Кем проверяется? И на каком этапе - статически или в рантайме?

> При том, что компилятор тоже может выполнять верификацию, и, следовательно, быть верификатором.

Согласен. Более того, этот «верификатор»-компилятор сам стремится исправить код на более оптимальный. Но в такой формулировке верификаторами пользуются все, кто компилирует с ключом -O, отличным от нуля. Речь ведь изначально шла про верификацию во время исполнения кода, а не статическими средствами, не?

> в такой формулировке верификаторами пользуются все, кто компилирует с ключом -O, отличным от нуля

Простым, нерасширяемым верификатором.

Речь ведь изначально шла про верификацию во время исполнения кода

Видимо, я пропустил момент, когда разговор о статической верификации перешел в разговор о динамической (более того, я впервые слышу о «динамической верификации» %)).

<вброс>

Линукс - ре-ше-то :)

</вброс>

>> в такой формулировке верификаторами пользуются все, кто компилирует с ключом -O, отличным от нуля

Простым, нерасширяемым верификатором.

Хм... вот насчет нерасширяемости - теперь не верно. Теперь же можно скрипты на питоне писать для gcc. С доступом ко внутренним структурам. Теоритически туда любые проверки запихать можно.

А кто-нибудь уже нашел, где у них собственно список проверяемых правил?

> вот насчет нерасширяемости - теперь не верно.

Всё еще верно.

Теперь же можно скрипты на питоне писать для gcc

Это уже не компилятор, а чекер на основе компиляторного промежуточного представления.

> Видимо, я пропустил момент, когда разговор о статической верификации перешел в разговор о динамической (более того, я впервые слышу о «динамической верификации» %)).

Статью из новости я, естественно, не читал, однако если правильно помню, их система верификации именно динамическая, по крайней мере, как я бы её назвал (хотя честно признаю, что в этом не разбираюсь): Код драйвера «чистится» от «ядерных» особенностей, инструментируется проверками на блокировки/разблокировки/что ещё они там проверяют, для полученного кода строится набор тестов, покрывающий все возможные варианты его работы, после чего «вычищенный» и инструментированный драйвер (т.е. уже по сути дела не драйвер, а инструментированный чекер с идентичной структурой кода) запускается на всех этих тестах. Раз код (пусть и модифицированный) запускается и вставленные проверки осуществляются во время исполнения - значит, динамическая(рантаймовая) верификация.

Поправьте, что не так.