17.04.2014: BLAST 2.7.2 на SV-COMP'2014 и результаты экспериментов
BLAST 2.7.2 был представлен на третьих международных соревнованиях по верификации программ, которые прошли в рамках конференции TACAS 2014 в Гренобле, Франция. В этом году BLAST выиграл золото в категории DeviceDrivers64.
Так как результаты соревнований, в первую очередь, нам интересны с точки зрения применения инструментов верификации в проекте Linux Driver Verification, мы провели несколько экспериментов с лучшими инструментами в категории DeviceDrivers64, а именно BLAST, UFO, FrankenBit и CPAchecker. Мы проверяли корректность работы с мьютексами в более чем 4,5 тысячах драйверов ядра Linux 3.12-rc1.
Мы использовали версии и конфигурации, представленные на соревнованиях, для всех инструментов, кроме CPAchecker, для которого мы взяли конфигурацию, используемую в LDV Tools по умолчанию, потому что конфигурация, представленная на соревнованиях, даёт больше ложных предупреждений об ошибках. Одной из причин этого является то, что конфигурация LDV Tools отключает консервативную обработку функциональных указателей, которые активно используются в драйверах устройств операционной системы Linux.
CPAchecker и BLAST обнаружили одинаковое количество ошибок, но эти ошибки оказались различны. Оба инструмента выявили по 53 ошибки, при этом 12 ошибок были различны. Для инструмента CPAchecker одна ошибка из 54 оказалась ложной. UFO и FrankenBit нашли меньше ошибок (20 и 31), и они также оказались разными. Но поскольку мы столкнулись с проблемами при анализе трасс ошибок, сгенерированных UFO и FrankenBit, мы не можем сказать, какое количество сообщений об ошибках соответствуют фактическим ошибкам. Эксперименты показали, что UFO является самым быстрым инструментом. Он работал в 1,5 раза быстрее, чем BLAST, в 3 раза быстрее, чем FrankenBit и в 3,5 раза быстрее, чем CPAchecker.
Основной вывод по результатм эксперимента заключается в том, что поскольку инструменты обнаружили различные ошибки, имеет смысл использовать их взаимодополняющим образом.
Также мы в очередной раз убедились что трасса ошибок, генерируемая для каждого сообщения об ошибке, имеет решающее значение для того, чтобы понять является ли сообщение ложным или нет. Минимальное требование к трассам ошибок заключается в возможности провести её анализ без знания деталей реализации инструмента верификации. Конечно, идеальным вариантом было бы включение в правила соревнований требования представлять трассы в едином формате, что облегчило бы включение новых инструментов в систему верификации драйверов и позволило бы воспользоваться инструментами визуализации трасс из состава LDV Tools.
