[personal profile] gdsfh
Делаю вот одну шнягу на окамле. Там есть файл, в нём "блоки данных", состоящие из подблоков малой длины.
И подумал я, что дёргать каждый раз 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 тут:
https://gist.github.com/gdsfh/47b34f009e25cee8c254

То, что получилось в окамле после ручного преобразования, тут:
https://gist.github.com/gdsfh/80f17a917cbd00b3bc66

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

Примерный расклад размеров блока и подблоков моих данных выражен тут:
https://gist.github.com/gdsfh/ed43540d260ef388d7cb

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

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

А читалку эту -- так и буду использовать в будущем проекте "ocaml persistent data structures". Но этот проект я отодвигаю подальше -- есть более важные в плане денег вещи.
From:
Anonymous( )Anonymous This account has disabled anonymous posting.
OpenID( )OpenID You can comment on this post while signed in with an account from many other sites, once you have confirmed your email address. Sign in using OpenID.
User
Account name:
Password:
If you don't have an account you can create one now.
Subject:
HTML doesn't work in the subject.

Message:

If you are unable to use this captcha for any reason, please contact us by email at support@dreamwidth.org


 
Notice: This account is set to log the IP addresses of people who comment anonymously.
Links will be displayed as unclickable URLs to help prevent spam.

Profile

gdsfh

August 2013

S M T W T F S
    123
45678910
111213 14151617
18192021222324
25262728293031

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags
Page generated Jul. 27th, 2017 04:41 pm
Powered by Dreamwidth Studios