15.03.2013: BLAST 2.7.1 на соревнованиях SV-COMP'2013 и результаты экспериментов
BLAST 2.7.1 был представлен на Вторых международных соревнованиях по верификации программ, которые прошли в рамках конференции TACAS 2013. В этом году BLAST завоевал бронзу в категории DeviceDrivers64. Второе место в этой категории занял инструмент CPAchecker, который уже интегрирован в систему верификации Linux Driver Verification. Победителем в категории DeviceDrivers64 стал новый инструмент UFO.
Поскольку результаты соревнований, в первую очередь, интересуют нас с точки зрения применения инструментов верификации в проекте Linux Driver Verification, мы провели небольшой эксперимент. Были запущены представленные на соревнавание версии BLAST, CPAchecker и UFO для проверки корректности работы с мьютексами в более чем 5-ти тысячах драйверов Linux 3.8-rc1.
Результаты показали, что CPAchecker пропускает достаточно много ошибок в анализируемом коде. Мы сообщили о ряде проблем разработчикам CPAchecker и совместно исправили их. Как следствие, текущая версия CPAchecker намного более пригодна для верификации драйверов Linux по сравнению с версией, представленной на соревнования.
Анализ результатов UFO показал, что инструмент не смог доказать корректность более 400 драйверов. Также была выявлена основная проблема использования UFO - анализ трасс ошибок. К сожалению, инструмент генерирует лишь фрагментарную информацию о пути в ошибочное состояние программы, что делает анализ результатов его работы проблематичным и, по сути, означает малопригодность текущей версии инструмента для практического применения.
В ходе обсуждений с разработчиками UFO на конференции выяснилось, что проблема следует из многочисленных трансформаций кода, которые активно используются внутри UFO. Надеемся, что в скором времени эта проблема будет преодолена.
Ещё одно интересное наблюдение по результатам эксперимента касалось времени проверки корректности. В ходе анализа драйверов Linux 3.8-rc1 время, потраченное на получение определённых результатов (SAFE или UNSAFE), оказалось более чем в 3 раза меньше по сравнению с временем, которое было потрачено на анализ, завершившийся вердиктом UNKNOWN. Согласно правилам соревнований, если инструменты набирают одинаковое количество очков, то лучший выбирается по минимальному времени работы, затраченному на получение определённых результатов. Пользователи же инструментов верификации должны ждать результатов анализа независимо от его вердикта, поэтому учёт времени работы только для получения определенных вердиктов может ввести в заблуждение.
На основе наших наблюдений мы сформулировали следующие предложения по правилам соревнований, чтобы сделать результаты более релевантными для пользователей инструментов верификации.
- Трасса ошибки является ключевым результатом работы инструмента, поэтому она должна выдаваться в понятном виде. Желательно, чтобы все инструменты поддерживали единый формат выдачи трассы, чтобы упростить его автоматическую обработку.
- Время затрачиваемое на анализ, завершившийся результатом UNKNOWN должно учитываться. По крайней мере, оно должно быть представлено в таблице суммарных результатов соревнований.
