Category: производство

Category was added automatically. Read all entries about "производство".

medved

Издержки верификации: скоро могут оказаться ниже нуля :)

Краткий анализ современных проектов по верификации наводит на мысль, что верификация позволит сократить затраты на создание программ уже в ближайшем будущем :). Правда, это похоже на тезис что Java (или там Haskell) могут быть быстрее Си. Да, могут, но в каких-то редких случаях, а в обычной жизни практичнее ожидать, что Си все-таки будет быстрее.

Прежде всего посмотрим на динамику снижения затрат на верификацию. Верификация ранее считалась совсем уж непрактичной, и было от чего, ибо ручная верификация требовала на пару порядков больше усилий, нежели само создание кода.
Однако велись интенсивные работы по автоматизации верификации. В результате, можно оценить, что затраты на верификацию в проектах, где применяется частичная автоматизация (seL4, CompCert) сократились до примерно 1 к 6 - 1 к 10, ну т.е. уже примерно на порядок выше чем собственно кодирование.
Отмечу, что два вышеуказанных проекта можно считать вполне себе промышленными, а не чисто академическими: было создано вполне себе реальное оптимизированное микро-ядро архитектуры L4 и вполне себе реальный оптимизирующий компилятор С.

Однако, если взглянуть детальнее, то создатели seL4 отмечают, что создание промежуточного прототипа/спецификации на Хаскеле (на основе которого потом очень быстро написали реализацию на Си), позволило сократить затраты на создание проекта примерно в 2 раза. А именно, затраты на создание ядра L4 чисто на Си, на основании других проектов оцениваются в 4-6 человеко-лет. Создание же спецификации на Хаскеле оценивается в 2 человеко-года, а последующая реализация на Си - в 2 человеко-месяца, т.е. на порядок меньше. Сама же верификация потребовала 20 человеко-лет (из них 11 специфичны для seL4, а 9 - это разработка тулзни общего назначения, однако тоже задействованной в проекте).

Т.е. предварительная формальная спецификация позволяет сократить проект примерно в два раза. Собственно, это не так уж и удивительно, ибо для меня практическая польза от формализации и заключалась в том, чтобы лучше понимать требования (и соответственно допускать меньше ошибок при реализации). Приятно видеть, что эта полезность продемонстрирована и измерена и на масштабном проекте.

Однако вернемся к затратам на верификацию. В вышеупомянутых двух проектах, несмотря на автоматизацию, значительная доля доказательств производилась в ручную - порядка 150 тыщ строк кода в случае seL4, а общее кол-во кода имеющего отношение к верификации в районе 200 тыщ. Это при том что спецификация на Хаскелл и реализация на Си потребовали где-то в районе 8 тыщ строчек кода каждая.
Также разработчики CompCert отмечают что большая часть доказательств проводилась в перво-порядковой логике, а значит тут можно было бы воспользоваться автоматическими пруверами типа SMT-солверов. К сожалению Coq их не очень поддерживал на тот момент, да и сейчас насколько я знаю не очень поддерживает. Т.е. можно ожидать, что интеграция этих пруверов в Coq позволило доказать большинство, хотя и не все теоремы, автоматически. Что означает сокращение издержек на верификацию еще в 2-3-4 раза. Т.е. верификация уже может быть сопоставима с затратами на кодирование - 1 к 2 - 1 к 3.

Разработчкик seL4 так же отмечают, что верификация следующего проекта аналаогичного seL4 потребовала бы по их оценкам 6 человеко-лет. Т.е. суммарно 2+6 = 8 человеко лет против 4 человека-года для более раннего проекта без использования верификации.

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

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

Конечно, можно не верифицировать, а оставить лишь предварительную формальную спецификацию и выигрыш в два раза останется за не-верификационным подходом :). Но это уже не так важно.

Кстати, насчет сокращения издержек вследствие предварительной спецификации. Часто такие спецификации пишут на (чистых) функциональных языках. Ну т.е. фактически реализуют программу, но на функциональном языке, ибо таковые спецификации исполнимы. А программы на функк языках часто короче аналогичных императивных в 2-10 раз.
Т.е. опыт проекта seL4 говорит что не стоит боятся делать предварительный прототип, по крайней мере, для достаточно крупного проекта. Если его делать на функциональном языке, то можно рассчитывать на бонусы :).