FLANG_MEMORY на parser.flang был не у проверки, а у ведомости: с теми же 170 обещаниями проверка проходит под теми же 24 ГиБ
flang/self/parser.flang с дописанными 170 обещаниями считался «стоящим вплотную к потолку»: под PAMYAT=24G он отвечал FLANG_MEMORY и с 170 обещаниями, и с 85, и с 42. Замер показал другое: flang check на нём проходит под теми же 24 ГиБ — 4 мин 48 с, пик 17,30 ГиБ, код 0, «замечаний нет», и предел шагов при этом не поднимался вовсе. Упиралась в память НЕ проверка, а ведомость (check --proof --json), которую снимали тем же прогоном.
Признак, по которому это видно в чужом выводе: ведомость печатает сводку модуля («функций …, из них с доказанным завершением …»), и только ПОСЛЕ неё — FLANG_CLI: ядро доказательства прекращено / оболочка: кончилась память. Проверка к этому моменту уже прошла. Если в выводе есть сводка, а отказ идёт следом, поднимать надо не предел, а вопрос, нужна ли ведомость этим прогоном.
Замеры. Ветка b/predely, двоичный bootstrap/flang из ствола, пик снят /usr/bin/time -v, всё через vorota/flang-vorota.
| прогон | ворота | обещаний | время | пик RSS | код |
|---|---|---|---|---|---|
parser.flang ствола, check | PAMYAT=40G | 394 | 2 мин 51 с | 9,80 ГиБ | 0 |
он же плюс 170, check --предел-шагов 4000000000 | PAMYAT=100G | 564 | 4 мин 51 с | 17,31 ГиБ | 0 |
он же плюс 170, check без единого ключа | PAMYAT=24G | 564 | 4 мин 48 с | 17,30 ГиБ | 0 |
monad.flang плюс 17, check --предел-шагов 4000000000 | PAMYAT=100G | 37 | 9 мин 41 с | 29,80 ГиБ | 0 |
Цена обещания измерена A/B. Тот же файл, та же команда, разница только в дописанных строках обеспечивает: +43 % обещаний дали ×1,77 памяти и ×1,70 времени. Одно обещание этого класса (постусловие-разворот ветви разбора, если … то результат равен … иначе да) стоит около 44 МиБ пика при двухстах байтах на диске. Рост нелинейный: добавка составила 5 % текста и 77 % памяти.
Размер файла ничего не предсказывает. monad.flang — 74 КБ, в двенадцать раз меньше парсера, — берёт 29,80 ГиБ против 17,30 у парсера. Считается замыкание ввозов, а не названный файл: у монады оно 7 файлов (в нём «Печать в C», 538 КБ, и «Проверка типов»), у парсера 5. Число это flang check печатает сам — «файлов вместе с импортами».
PAMYAT — это адресное пространство, но для проверки оно почти равно занятой памяти. В самих воротах записан замер на ПЕРЕПЕЧАТКЕ компилятора: VmPeak 61,7 ГиБ при VmHWM 25,1 ГиБ, отношение 2,5. Для flang check это неверно — снято из /proc/<pid>/status на живой проверке:
VmPeak 30,5 ГиБ
VmHWM 28,7 ГиБ отношение 1,06Значит запас в 2,5 раза при проверке закладывать не надо: PAMYAT ставится по ожидаемой занятой памяти плюс десятая часть. Обратное — как раз то, из-за чего PAMYAT=24G выглядел «потолком, к которому файл стоит вплотную».
Предел шагов у парсера ни при чём. Прогон под 24 ГиБ прошёл вообще без --предел-шагов: миллиард витков, вшитый в семя, не исчерпался. У monad.flang и proof-kernel.flang дело другое — там ядро действительно упирается и в 1 000 000 000 витков, и в память (29,8 ГиБ у монады объясняют FLANG_MEMORY под PAMYAT=24G сами по себе).
Чем ограничено. Замер на двух файлах и одном классе обещаний. Цена обещания другой формы будет другой; верно то, что она не убывает и что по размеру файла её не угадать. Отдельно НЕ мерено, во сколько раз ведомость дороже проверки — только то, что дороже.
Связано: arena-never-releases, arena-makes-memory-not-time-the-limit-of-a-long-computation, an-inner-step-limit-multiplies-into-the-outer-budget, ветка-если-разворачивается-в-обе-стороны-а-разбор-списка-нет