Распределитель памяти
docs/examples/allocator/allocator.flang — распределитель памяти, записанный чистой функцией. Куча — данные: список свободных отрезков и общий размер. Запрос — значение: «Взять» столько-то или «Вернуть» адрес и длину. Распределитель — функция «Шаг кучи», которая возвращает новую кучу, адрес и признак «удалось»:
тотальная функция «Шаг кучи»
принимает куча: «Куча», запрос: «Запрос»
возвращает «Отклик кучи»Память функция не трогает — она отвечает, что теперь считать занятым. Приём тот же, что у драйвера UART docs/examples/driver/uart.flang и у драйвера MSI.
Программа отвечает на вопрос «выразим ли распределитель на flang и что о нём доказуемо». Замена malloc в напечатанном на C рантайме ею не является: рантайму память нужна раньше, чем появится первое значение «Куча».
Что лежит в файле
Файл один, 416 строк .
Типы: «Отрезок» (начало, длина), «Куча» (свободные отрезки, всего), «Запрос» (варианты «Взять» и «Вернуть»), «Отклик кучи» (куча, адрес, удалось). Размер кучи — константа функции «Размер кучи», 4096.
Что делают функции:
- «Выдать» проходит свободные отрезки свёрткой («Пройти свободные», шаг — «Шаг выдачи»), берёт первый отрезок не короче запроса и оставляет его остаток свободным. Если места нет, отклик отказный и куча не меняется.
- «Вернуть кусок» вставляет отрезок в список свободных по порядку начал («Пройти вставку», шаг — «Шаг вставки»). Нулевой возврат и возврат за границу кучи отвергаются, куча при этом цела.
- «Годная куча» — свободные отрезки идут по возрастанию и не накладываются («Шаг годности»).
- «Шаг кучи» ветвится по виду запроса и зовёт «Выдать» либо «Вернуть кусок».
- «Отклик первой выдачи», «Отклик второй выдачи», «Отклик возврата» — замкнутый след из трёх шагов на свежей куче; их постусловия считаются вычислением.
Как запустить
bootstrap/flang check docs/examples/allocator/allocator.flang --proof
bootstrap/flang test docs/examples/allocator/allocator.flangОтчёт --proof печатает вердикт по каждому постусловию и последней строкой — сколько утверждений доказано, сколько на сетке, сколько объявлено без доказательства. На этой странице этих чисел нет: они меняются вместе с ядром. Замер на определённую дату, до и после правки свёртки, стоит в разделе о неравенствах на странице какие обещания ядро берёт.
Что доказано и что нет
Все функции файла тотальны, и завершение каждой доказано композицией. Утверждений вида «объявлено, не доказано» в отчёте нет.
Доказано обо всех входах — всё, что записано равенством терму той же ветви или условием на признак: отказ честен («ОТКАЗ ЧЕСТЕН: места нет — куча не изменилась», «ОТКАЗ ЧЕСТЕН: нулевой возврат отвергается, куча цела», «ОТКАЗ ЧЕСТЕН: возврат за границу кучи отвергается, куча цела»), выдача идёт только из отрезка («ВЫДАЁТ ТОЛЬКО ИЗ ОТРЕЗКА: адрес выдачи есть начало отрезка»), вместо взятого отрезка встаёт его остаток («НИЧЕГО НЕ ПОТЕРЯНО: вместо взятого отрезка встаёт его остаток»), возвращённый отрезок встаёт в список, порядок вставки, весь замкнутый след трёх шагов — включая годность кучи после каждого шага и «свободного стало ровно на выданное меньше».
Доказано индукцией по свёртке: «просят столько же, сколько запросили» и «свободных отрезков остаётся столько же» у «Пройти свободные», «возвращаемый отрезок по дороге не меняется» у «Пройти вставку». Для этого свёртка обязана идти по самому доводу-списку: «Пройти свободные» принимает список отрезков, а не кучу, потому что при свёртка куча.«свободные» принцип индукции ядром не читается.
На сетке (проверено примерами функции, не доказано) остаются постусловия, записанные неравенством или вычитанием:
| постусловие | функция |
|---|---|
| «конец не левее начала» | «Конец отрезка» |
| «НИЧЕГО НЕ ПОТЕРЯНО: остаток плюс выданное — прежняя длина» | «Остаток отрезка» |
| «ВНУТРИ КУЧИ: адрес не левее начала отрезка» | «Выдать из отрезка» |
| «ВНУТРИ КУЧИ: конец выданного не правее конца отрезка» | «Выдать из отрезка» |
| «НЕ ПЕРЕСЕКАЮТСЯ: конец выданного не правее начала остатка» | «Выдать из отрезка» |
| «НЕ ПЕРЕСЕКАЮТСЯ: выданное и остаток — по проверке» | «Выдать из отрезка» |
| «НИЧЕГО НЕ ПОТЕРЯНО: остаток плюс выданное — прежняя длина отрезка» | «Выдать из отрезка» |
| «ГРАНИЦА НЕ ПЯТИТСЯ: прежняя не правее новой» | «Шаг годности» |
Причина одна: арифметики неравенств у ядра нет — ни рефлексивности «не больше», ни монотонности сложения, ни закона «(а минус б) плюс б равно а». Поэтому «выданное внутри кучи» и «ничего не потеряно», записанные неравенством, остаются сеткой, а та же мысль, записанная равенством («остаток начинается ровно там, где кончается выданное»), доказана. Правило для пишущего: границы отрезков записывайте равенствами.
Отдельно о типах: у полей «начало» и «длина» тип число, а не неотрицательное, потому что сумма двух неотрицательное в языке даёт число. Обещание «конец не левее начала» поэтому не просто не доказано — при отрицательной длине оно неверно, и отказ ядра здесь по существу.
Чего здесь нет
- Слияния соседних свободных отрезков. Возврат вставляет отрезок по порядку начал и с соседями его не сливает; куча дробится. Слияние — ещё один шаг свёртки того же вида, он не написан.
- Годности в общем виде. «Годная куча» ничего не обещает, и утверждения «из годной кучи «Шаг кучи» делает годную» для произвольной кучи нет. Годность доказана только на замкнутом следе трёх шагов.
- Живучести. Доказано, что каждый шаг переводит кучу из состояния в состояние; что распределитель когда-нибудь отдаст память ждущему — свойство бесконечной последовательности, а не одного шага.