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

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

tailgunner (14.11.2011 16:04:06)

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

Manhunt (14.11.2011 16:05:40)

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

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

tailgunner (14.11.2011 16:07:30)

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

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

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

www_linux_org_ru (14.11.2011 16:13:21)

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

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

tailgunner (14.11.2011 16:21:15)

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

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

www_linux_org_ru (14.11.2011 16:21:15)

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

tailgunner (14.11.2011 16:24:51)

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

www_linux_org_ru (14.11.2011 16:25:45)

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

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

www_linux_org_ru (14.11.2011 16:33:05)

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

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

tailgunner (14.11.2011 16:35:11)

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

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

www_linux_org_ru (14.11.2011 16:41:37)

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

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

Aceler (14.11.2011 16:42:15)

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

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

Круто

yoghurt (14.11.2011 16:58:00)

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

yoghurt (14.11.2011 16:59:18)

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

www_linux_org_ru (14.11.2011 17:29:10)

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

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

www_linux_org_ru (14.11.2011 17:30:18)

[вброс]

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

[/вброс]

dizza (14.11.2011 17:46:48)

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

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

r (14.11.2011 17:51:06)

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

Aceler (14.11.2011 17:57:20)

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

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

www_linux_org_ru (14.11.2011 18:10:04)

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

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

www_linux_org_ru (14.11.2011 18:16:28)

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

dizza (14.11.2011 18:28:11)

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

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

x86_64 (14.11.2011 18:30:31)

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

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

tailgunner (14.11.2011 18:32:31)

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

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

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

dizza (14.11.2011 18:46:21)

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

dizza (14.11.2011 18:47:21)

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

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

x86_64 (14.11.2011 18:47:34)

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

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

Почему нет?

tailgunner (14.11.2011 18:50:08)

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

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

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

x86_64 (14.11.2011 18:51:40)

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

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

> Почему нет?

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

x86_64 (14.11.2011 18:53:52)

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

ei-grad (14.11.2011 18:57:14)

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

dizza (14.11.2011 19:04:33)

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

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

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

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

x86_64 (14.11.2011 19:09:35)

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

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

x86_64 (14.11.2011 19:13:26)

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

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

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

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

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

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

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

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

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

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

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

x86_64 (14.11.2011 19:24:30)

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

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

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

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

tailgunner (14.11.2011 19:28:48)

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

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

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

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

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

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

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

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

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

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

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

tailgunner (14.11.2011 19:47:37)

<вброс>

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

</вброс>

rtvd (14.11.2011 19:51:26)

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

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

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

x86_64 (14.11.2011 19:55:18)

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

tailgunner (14.11.2011 19:57:00)

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

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

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

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

tailgunner (14.11.2011 19:58:20)

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

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

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