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

Стена «слой связывается асинхронно» стоит 263 синхронных места вызова, а не одной правки

Пять модулей JavaScript (src/bounded.mjs, src/conc.mjs, src/failures.mjs, src/io.mjs, src/monad.mjs) держатся в рабочем пути flang check тем, что их решение зовут из синхронного кода: вывод типов (checkTypes) и разбор. Сторона на flang связывается асинхронно и стоит около четверти секунды на слой, значит позвать её можно только оттуда, где есть await.

Три способа снять стену, и у каждого цена измерена, а не оценена.

Способ первый — связать слои заранее и передать их внутрь синхронной двери. Образец в дереве есть: так уже сделана ведомостьСлоем, и так же внутрь checkTypes уже едет размещение процессов. Цена — 263 места вызова checkTypes в 81 файле; из них 64 вызова в 18 файлах строят программы с процессами, планами или монадами, то есть ровно те, где проверка без слоя замолчала бы. Замолчавшая проверка — худший исход из возможных, поэтому дверь обязана отказывать громко, и все 64 места надо провести руками.

Способ второй — связывать слои безусловно на входе команды. Цена по часам измерена связыванием каждого слоя по отдельности: failures.flang 292 мс, bounded.flang 231, io.flang 261, conc.flang 248, monad.flang 356 — итого 1 388 мс на каждый прогон, включая программы, где ни процессов, ни планов, ни монад нет. При том что flang check --proof на простой программе идёт около секунды, это ×2,4 за молчание. Дешевле — связывать по признаку, прочитанному с разобранной программы (так уже сделаны замок и пакет), но признак не снимает цену способа первого: дверь всё равно синхронная.

Способ третий — поднять асинхронность выше по цепочке, сделав разбор и вывод типов асинхронными. Цена — 948 мест вызова parse( плюс те же 263 вызова checkTypes в дереве: await пришлось бы протащить через всё.

Чем подтверждено. Числа мест — разбор ввозов дерева (grep по flang/**/*.mjs). Цепочка вызовов снята прогоном: перехватчик load из node:module вписывает печать следа в первую строку тела названных функций (правится копия исходника в памяти загрузчика, файл на диске не трогается), и flang check --proof на программе с процессами даёт, например:

достижимыеОтказы (src/failures.mjs) ← checkFailureCoverage (src/types.mjs:3765)
  ← checkTypes (src/types.mjs:943) ← markProven (src/types.mjs:1486)
  ← markProven (bin/flang.mjs:1201) ← async loadProgramFromSource

Времена связывания — linkProgram + createRuntime на каждом слое отдельным прогоном. Ветка worktree-agent-ac8d41bfd9b3d78cf, коммит 1a8fb1dc.

Отдельно измерено, что стена держит НЕ ВСЕХ. У src/conc.mjs четыре из шести потребителей в рабочем пути (parser, types, io, failures) берут ТОЛЬКО словари и коды — 11 имён, ничего не решающих, — а решающий runConcurrentExamples зовётся из compat.runExamples, куда ведёт всего один синхронный шаг из асинхронной checkProgram. То есть conc.mjs (2 140 строк) снимается не стеной, а разделением, тем же приёмом, каким выехали as-written.mjs и set-shapes.mjs: словарь остаётся, машина уезжает за отложенный ввоз. Оценка выигрыша — около 1 800 строк рабочего пути при нуле снятых файлов; цена — 30 файлов дерева, ввозящих conc.mjs, из которых переставить надо четыре.

Чем ограничено. Числа мест вызова считают вхождения текста, а не исполненные вызовы: часть из 263 стоит в проверках, которые строят программы без процессов, и стены не почувствует. Разделение conc.mjs не переключает решения — JavaScript продолжает считать, уходит только ввоз; это то же различие «вынут из решения» и «вынут из загрузки», что записано у obligations.mjs.

Связано: one-named-reason-for-a-group-hides-the-others, four-pieces-of-javascript