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

Автоматический вывод регионов — мимо цели, а не дорого

Довод важнее вывода: отвергать надо было не по цене.

Почему мимо. Регионы в MLKit привязаны к области видимости (Ground Rule). Наша беда другая: значение уже мертво, но имя ещё в области видимости. Разбор конкретного места в напечатанном C показал, что вывод регионов воспроизвёл бы там известный режим отказа MLKit (примеры sumit и concat с Θ(N²)), а не удачный случай.

Цена, для полноты. У MLKit 20 836 строк региональной машинерии — 35,7 % компилятора, 8 фаз из 11, сложность O(n⁴), алгоритм неполон. На бенчмарке logic чистые регионы утилизируют 0,1 % мусора и текут в 196 раз.

Что взято вместо. Регион на вызов с копией результата наружу — тот же приём, что уже сделан в отказоустойчивости. В двадцать раз дешевле и измерен: arena-never-releases.

Общий урок. «Дорого» — слабый довод, его перебивают упорством. «Мимо цели» — сильный: он говорит, что даже сделанное идеально не поможет.

Связано: memory-per-category-is-regions, arena-never-releases