gds (gds) wrote,
gds
gds

coq + imperative algorithm proving

Делаю вот одну шнягу на окамле. Там есть файл, в нём "блоки данных", состоящие из подблоков малой длины.
И подумал я, что дёргать каждый раз Unix.read (обёртку над read()) не очень гуманно в плане количества вызовов ОС, например.
И решил я реализовать более умный алгоритм чтения-кеширования, читающий в блок размера "дисковый блок * 2", по выравненным смещениям, стараясь читать по границе блока, чтобы не читать ненужные блоки. Однако, кое-где явно нет нужды пропускать данные через буфер, когда ясно, что "цельные блоки" можно прочитать напрямую в строку-получателя.
Но оказалось, что я не смог отладить этот сугубо императивный алгоритм руками, и у меня вообще не было уверенности в том, что он работает правильно. Эти гадские смещения, длины! Невозможно интуитивно проверить, правильно ли сделал. Очень БЕСЕД, знаете ли.

Тогда я взял Coq.


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

Далее я решил брать не штатную экстракцию Coq -> OCaml, чтобы не заворачивать всё в манатки, а вручную переписать код. Для этого я принял обозначения: идентификаторы, начинающиеся с малой буквы, будут присутствовать в рантайме, а идентификаторы, начинающиеся с большой буквы, связаны с внутренней логикой доказательства (то есть, виртуальные смещения/длины в строке-получателе, например, ну и все доказательства в целом), и в рантайме будут отсутствовать.

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

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

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

И вот, в окамловском коде нет нужды пихать ассерты на каждый чих, во все внутренние функции. Благодаря доказательствам, их достаточно повесить в функции, выданные наружу пользователю -- read_char, read_string, read_into_substring.

Какой именно алгоритм чтения-кеширования взять -- я представлял вполне, даже зарисовал его в носкии-арте в исходниках. Всего получилось 7 различных стратегий чтения. Например, 7ая -- случай, когда конец региона файла далеко относительно "размера блока * 3", но последнее чтение, которое будет касаться запрошенных данных, вполне может прочитать остаток файла в буфер, вплоть до конца региона файла. 2ая -- случай, когда конец файла относительно начала буфера находится в [размер блока * 2 .. размер блока * 3), конец данных в буфере больше размера блока, и тут мы можем сначала взять всё, что в буфере, передвинуть буфер, прочитать до конца региона файла и больше не читать из файла вообще.

Большое внимание пришлось уделить автоматизации доказательств. В целом получилось в стиле "разрушим все значения таких-то типов, выполним подстановки, упростим, применим арифметику". Однако, в некоторых редких случаях пришлось явно создавать доказательства, чтобы они присутствовали среди гипотез, таким образом, были доступны для тактик, обращающих внимание на гипотезы. В некоторых случаях пришлось анализировать цель доказательства и смотреть: "если там есть подвыражение x mod n, то генерим две гипотезы: 0 <= x mod n и x mod n < n, и оно будет использоваться для доказательств".

Чтобы не было нужды писать "_" (типа, "coq, выведи сам значение") для доказательств, я их сделал implicit argument'ами, их тип выводится на основании explicit arguments, а значение формируется тактиками, формирующими тела доказательств.

Код Coq тут: http://tinyurl.com/nvqxk8s

То, что получилось в окамле после ручного преобразования, тут: http://tinyurl.com/pf2y9yj

Тесты сразу же показали, что читалка во всех случаях работает так же, как простой Unix.read, в плане корректности прочитанных данных. Это меня очень обрадовало.

Примерный расклад размеров блока и подблоков моих данных выражен тут: http://tinyurl.com/pdnrc22

Однако, пичалька в том, что прирост производительности -- всего 10..15%.

Тем не менее, прирост моих знаний и умений, вызванных решением этой проблемы, гораздо больше в абсолютной величине. Задача была интересной и необычной. Мне очень понравилось.

А читалку эту -- так и буду использовать в будущем проекте "ocaml persistent data structures". Но этот проект я отодвигаю подальше -- есть более важные в плане денег вещи.
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 12 comments