ИИтог

В языке Valen проверка заимствований идёт по функции задом наперёд

инструментыРедакция ИИтогHacker News🔥41Рейтинг ИИтог41Влияние25Новизна45Релевантность70Неожиданность45Участники5Достоверность60

В блоге verdagon.dev вышла статья о borrow checker (проверке заимствований) языка Valen. Автор начинает с признания: идея казалась странной, но сработала, и он сам в это не вполне верит, ведь проверка «путешествует назад во времени». Если без драматизма, она обходит функцию в обратном порядке. Обратный обход, по словам автора, нередко применяют в оптимизациях компилятора, но для проверки безопасности памяти, насколько ему известно, так не делал никто. Это не обычная проверка по принципу «разделяемое либо изменяемое» (shared-xor-mutable): в Valen этот принцип необязателен, а из кода можно вызывать функции на Rust с сохранением безопасности памяти на границе. Проверка похожа на ту, что в Rust, но допускает безопасный изменяемый алиасинг (несколько ссылок на одни данные).

Valen компилирует функцию в четыре этапа. Из статьи видно, что второй этап, статическая типизация: она проставляет типы переменным (например, превращает let fuel = 5 в let fuel i64 = 5). Третий, статическая группировка (static grouping): прямой проход сверху вниз, который определяет, куда указывает каждая ссылка. Например, для first_ref = &s.fuel_cells[0] он вычисляет, что ссылка указывает на целое число где-то в массиве s.fuel_cells[], и это становится частью типа переменной. Первый этап автор пропускает. Четвёртый этап проверяет обращения к освобождённой памяти (use-after-free) и идёт в обратном порядке: от последнего оператора функции к началу. Автор также упоминает пятый, «секретный» этап, расчёт атрибутов для LLVM, но он вне темы статьи. Термин «группа» (group) автор собирается заменить на «путь» (path) и просит высказывать мнения. В первой версии (V1) группировка запоминала ещё и момент создания ссылки (строку кода), в новой версии (V2) это не нужно именно благодаря обратному проходу.

Алгоритм отслеживает три события: DECLARE (объявление переменной), USE (использование) и MUTATE (изменение группы). Есть список pending: в нём всё, что использовано ниже по коду и должно найти своё объявление выше. Если при движении вверх встречается MUTATE, затрагивающий что-то из pending, это ошибка.

Пример 1. В функции foo сначала берётся ссылка buff = &e.buffs[0], затем вызывается e.add_buff() (изменяет группу g), затем идёт print_int(buff). Проход начинается с последней строки: USE buff (группа g.buffs[]), buff попадает в pending. Строкой выше, MUTATE группы g. Компилятор проверяет, что ничто из pending не указывает внутрь e, но buff указывает на g.buffs[], то есть внутрь изменяемой группы. Значит, buff стал недействительным выше строки, где используется, это use-after-free, и компилятор выдаёт ошибку. Автор добавляет: первый, кто сломает алгоритм, получит приз.

Пример 2. Тот же код, но e.add_buff() перенесён в начало. Проход добавляет buff в pending по строке print_int, затем на строке с объявлением buff убирает его из pending, список пуст. Встретив MUTATE, он ничего не находит в pending, затем видит USE e и добавляет e в список. Дойдя до начала функции без изменений того, что ожидает объявления, алгоритм заключает: программа безопасна по памяти.

Почему назад, автор называет три причины: удобство, циклы и скорость. Удобство: так проще понять, где переменная используется в последний раз. В функции attack при прямом проходе пришлось бы делать лишнюю выборку и навигацию, потому что последнее использование не узнать в момент встречи; при обратном, это проще. Циклы: в примере с while, где в теле есть observe(e), add_element(&arr) и set e = &arr[0], прямому проходу пришлось бы заглядывать вперёд, чтобы понять, что e снова присвоена и использование корректно; без set e использование e недопустимо, так как e недействительна после предыдущей итерации. Автор рассматривал и другие подходы, последний из них выглядел заманчиво, но требовал очень сложных структур данных и страдал той же проблемой «выборки и навигации», так что проще оказалось сразу идти назад. Скорость: автор «довольно уверен» (замеров нет), что V2 быстрее, поскольку каждый узел обрабатывается один раз в прямом проходе третьего этапа и один раз в обратном проходе четвёртого. Это пока не O(n): MUTATE всё ещё проверяет весь список pending, хотя автор думает, что эту проверку можно сильно ускорить. Сравнивать циклы не с чем: в V1 полной поддержки циклов не было.

Для циклов нужны доработки: MUTATE и DECLARE обрабатываются иначе (в разборе появляются списки revived_after_this и mutations_after_this), а на событие LOOP START (начало цикла) алгоритм реагирует отдельной проверкой для каждого элемента pending. Разбор корректного примера с циклом в доступном тексте обрывается на этой проверке, итог её не виден.

Ключевые факты

  • Borrow checker языка Valen выполняет проверку на use-after-free обратным проходом: от последней строки функции к началу; по словам автора, насколько ему известно, это единственная такая проверка.
  • Функция компилируется в четыре этапа; третий (статическая группировка) идёт вперёд и вычисляет, куда указывает каждая ссылка, а четвёртый, обратный.
  • Алгоритм хранит список pending из использованных ниже переменных и сообщает об ошибке, если встречает MUTATE, затрагивающий что-то из него.
  • Три причины идти назад по версии автора: удобство определения последнего использования, циклы и скорость; выигрыш в скорости он оценивает как «довольно уверен» и не измерял.
  • Для циклов нужны дополнительные шаги: иная обработка MUTATE и DECLARE и реакция на LOOP START; в первой версии (V1) полной поддержки циклов не было.

Почему это важно

Идея необычна для проверки безопасности памяти: обратный проход по функции известен по оптимизациям компилятора, но, по словам автора, насколько ему известно, для такой проверки его раньше не применяли. Автор утверждает, что он упрощает определение последнего использования переменной и обработку циклов, где прямому проходу приходится заглядывать вперёд.

Кому это важно

Тем, кто интересуется проектированием языков программирования и компиляторов, а также borrow checker в духе Rust. Для широкой аудитории это нишевый разбор идеи в одном языке. Нейросетей в материале нет.

Как это применить

Это не готовый инструмент, а описание алгоритма. Разработчик компилятора может перенять схему: события DECLARE, USE и MUTATE, список pending и обратный проход. Сведений о выпуске, версиях или условиях использования Valen в доступном тексте нет.

Можно ли доверять

Это авторская статья-объяснение из блога; автор пишет, что ни одна её часть не создана ИИ. Утверждение об уникальности обратной проверки он сам оговаривает («насколько мне известно»). Выигрыш в скорости не измерен, а формального доказательства корректности нет: автор лишь приглашает читателей попробовать сломать алгоритм. Доступный текст обрывается посреди разбора циклов.

Риски и подводные камни

Алгоритм пока не линейный: MUTATE проверяет весь список pending, а ускорение этой проверки лишь предполагается. Циклы требуют доработок, и итог проверки LOOP START в доступном тексте не виден. Терминология ещё меняется: автор собирается заменить «группу» на «путь», а в примерах использует имя ArrayList вместо Array из реального компилятора. Сравнивать скорость циклов не с чем, поскольку в V1 их полной поддержки не было.

«Потому что он путешествует назад во времени. Или, если без драматизма, он обходит функции в обратном порядке, что всё равно очень странно.»

— Автор статьи на verdagon.dev