flang компилятор доказывает, что программа не зациклится 0.6.2 GitHub

Область памяти не отдаёт ничего до конца вызова: 1655 МиБ на сортировку 4000 чисел

Главная находка замера памяти (ветка work/pamyat-regiony, отчёт docs/memory-and-regions.md).

Утечек нет вообще — valgrind даёт ноль байт в ноль блоков. Но:

сортировка слиянием 4000 чисел
  пик памяти        1655 МиБ
  живой результат    125 КиБ
  отношение          13 558×
  рост               быстрее квадрата

Это не цена доказуемости. Проверено отдельно: без счётчика шагов те же 1653 МиБ, разница 0,1 %. Обычный дефект, а не плата за гарантии.

Исправление измерено, не оценено. Прототип «область на вызов с копией результата наружу», поставленный прямо на напечатанном C без правки компилятора:

былостало
пик памяти1653 МиБ3,4 МиБ
времявтрое быстрее
valgrindчисточисто

В 486 раз меньше памяти, за 200–300 строк. Названы четыре изъяна прототипа, включая скрытую ошибку с fl_grow (grow->capacity переживает откат), найденную рассуждением и подтверждённую по коду.

Позже замер скорости показал, что 1655 МиБ были мягче реальности. Сортировка вставками — тотальная, доказанная, написанная прямо — на 4000 элементах набрала 178 ГиБ и не досчитала за две с половиной минуты, процесс пришлось снять.

250 элементов  →   80 МиБ
500            →  604 МиБ
1000           →  5,6 ГиБ
1500           →  отказ
4000           →  178 ГиБ, не досчитала

Рост кубический. Алгоритм квадратичен по времени, и это нормально; кубическая память — нет. То есть это уже не правка, а работа, и она важнее скорости: программа, съевшая 178 ГиБ, не медленная — она просто не работает.

Сделано 15 августа, перемерено 18-го

Прототип стал деревом: коммит e342156 поставил fl_region_open / fl_region_close вокруг тела каждой функции, способной к рекурсии. Все числа выше — ДО него, и разошлись они с деревом на два порядка:

былостало
слияние 40001 655 МиБ6,1 МиБ, 0,48 с
вставки 10005,6 ГиБ, 9,68 с46 МиБ, 2,48 с
вставки 4000178 ГиБ, не досчитала710 МиБ, 151 с, досчитала

Урок про заметку, а не про память: число, названное «самым тяжёлым во всём замере», простояло устаревшим три дня, потому что правку сделали в другом файле и не вернулись к отчёту. Оно успело попасть в задание, где его назвали доказательством непригодности языка. Правка была; непригодности нет.

Сделано 18 августа: область на накопитель свёртки

fl_region_recycle в рантайме плюс печать области вокруг цикла свёртки в обеих реализациях бэкенда C. Вставки на 4 000: 8 МиБ вместо 710, то есть в 88,7 раза; против исходных 178 ГиБ — в 22 785 раз. Ответ побайтово тот же, восемь целей зелены (597 из 597), неподвижная точка перепечатана.

Плата названа: 1,37 раза по времени (151 → 207 с на 4 000). Откат витка копирует накопитель, а «Приписать в начало» теряет при этом хвостовой запас массива. Первая сборка стоила 1,74 раза; порог FL_REGION_LOOP_GAIN = 16 против FL_REGION_GAIN = 4 вернул 55 секунд из 111: накопление отказывается от отката по построению, перестройка проходит с k ≈ 32.

И сторож, которого не было. Пик памяти в этом дереве не мерил НИКТО — потому число и прожило три дня после того, как стало неправдой. Заведён ./ярлык память:проверка (flang/scripts/memory-guard.mjs): прогон на 250, 1 000 и 4 000, пик через /usr/bin/time -f %M, порог вдвое от измеренного — то же правило, по которому в дереве уже стоят пределы витков.

Остаток назван местом. Рост теперь квадратичный: n²/2 значений, из них живых n. На 4 000 — 4 тысячи живых и почти 8 миллионов мёртвых, 99,95 % пика. Причина одна: область даётся по признаку рекурсии (emit/c.mjs:972), а свёртка не рекурсивна, и n её накопителей копятся в арене вызова. Проба области на свёртку, поставленная руками на напечатанном C: 4 000 элементов — 6,1 МиБ вместо 710, ответ побайтово тот же. Разбор и цена по частям — docs/zamer-skorosti.md.

Отдельное предупреждение: дефект с разворачиванием общего подграфа при глубоком копировании уже есть в дереве и там не записан.

Связано: memory-per-category-is-regions, a-measured-zero-is-valuable

Поправка 24 августа 2026: на откате области куски теперь уходят системе

«Не отдаёт ничего до конца вызова» верно про арену как таковую и неверно про откат области: с 24 августа fl_arena_rollback отдаёт системе весь хвост цепочки за отметкой, кроме первых FL_ARENA_KEEP кусков. Пик check flang/self/types.flang --proof от этого −36,3 %, parser.flang --proof −61,2 %, время не изменилось. Разбор и обе цены — arena-gives-chunks-back-on-rollback.