27.08.2014: Выпущен инструментарий LDV Tools 0.6
Наиболее важные изменения, которые вошли в LDV Tools 0.6:
- Поддержка совместимости с ядром ОС Linux версий 3.14-3.16.
- Улучшения в 5 существующих спецификациях правил:
- Добавлены 11 новых спецификаций правил:
- Memory releasing in the USB subsystem.
- RCU critical section for rcu_dereference().
- Initialization of USB request blocks.
- SCSI DMA (un)mapping.
- PCI DMA (un)mapping.
- Memory regions allocation/releasing.
- Memory caches allocation/releasing.
- DMA pools allocation/releasing.
- SKB allocation/releasing.
- IRQ request/free.
- Kernel threads creation/stop.
- Обновлена версия инструмента верификации CPAchecker до 1.3.4 (r12604).
- Исправлена большая часть проблем с памятью, в особенности утечки памяти, в Aspectator и C-Backend компонента CIF (теперь он потребляет до тысячи раз меньше памяти на больших аспектных файлах) .
- Оптимизация Aspectator, которые сокращают время инструментирования до 25 раз для некоторых больших аспектных файлов.
- Альтернативная реализация скрипта загрузки результатов верификации в базу данных, которая работает в несколько десятков раз быстрее предыдущей.
Результаты валидации инструментария LDV Tools версий 0.6 и 0.5 с различными инструментами верификации на наборе, состоящем из 41 известной ошибки в ядре Linux*, представлены ниже в таблице.
| LDV Tools 0.6 | LDV Tools 0.5 | ||||
| BLAST | CPAchecker | BLAST | CPAchecker | ||
| Найденные ошибки | 17 | 13 | 15 | 14 | |
| Пропуск ошибок | Ошибки в инструментах верификации | 3 | 2 | 3 | 3 |
| Нехватка памяти (63 гигабайта) | 1 | 2 | 1 | 0 | |
| Нехватка времени (50 минут) | 0 | 6 | 0 | 4 | |
| Неподдерживаемые спецификации правил | 0 | 0 | 7 | 7 | |
| Другие | 20 | 18 | 15 | 13 | |
Инструменты верификации BLAST и CPAchecker смогли найти на одну ошибку больше благодаря улучшению спецификации правила SKB allocation in pm_runtime context. Дополнительно BLAST нашел еще одну ошибку для одной из новых спецификаций. CPAchecker не смог найти три ошибки из-за увеличения времени анализа, но нашел ошибку, которая раньше не находилась из-за исключения.
Соответствующий исходный код доступен в репозитории по тегу v0.6. Инструкции по скачиванию и установке LDV Tools описаны здесь.
* Текущий набор валидации имеет ряд существенных отличий от набора, использованного ранее для валидации LDV Tools 0.5.