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

Память «на категорию» — это регионы, техника с именем и историей

Идея владельца: выделять память не на каждое значение, а на категорию целиком — поработали, категория кончилась, освободили одним действием.

Это настоящая техника, называется региональное управление памятью (regions, arenas). Так сделано в MLKit (диалект ML, где регионы выводятся автоматически), в Cyclone, и по сути на этом же стоят времена жизни Rust.

Идея уже наполовину в дереве flang, просто не была так названа. Цель C выделяет всё сдвигом указателя в области и освобождает одним действием (flang_runtime.h:32–52) — только область одна на весь вызов. А в отказоустойчивости уже сделана настоящая двухобластная схема с копированием живого наружу.

Где ловушка. Компилятор должен уметь доказать, что из области ничего не утекло. Значение из категории, попавшее туда, где категория закончилась, — это обращение к освобождённой памяти, то есть ровно та беда, от которой бежали.

Почему у flang шанс лучше среднего. Анализ происхождения значений уже есть — на нём стоят тотальность и постусловия.

Связано: arena-never-releases, region-inference-misses-the-point, safety-standards-ban-dynamic-memory