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

Распределённость делится на мир и провод в отношении 459 к 119, и печатать компилятор умеет только провод

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

Счёт разводит их окончательно. flang/conc/distributed.mjs — 1062 строки на конец 20 августа; счёт ниже снят утром того дня, когда в файле было 589 строк кода (без комментариев и пустых), и они делились так:

частьстрокна flang
создатьУзел — сокеты, часы, таблица процессов, планировщик444нет
конструкторыВариантов — проба по экспортам чужого модуля15нет
мир459нет
кодирование, сроки, состояния связи, виды кадра, размещение, адрес54было
раскодирование31стало
границы кадров в потоке22стало
перевод плана в дерево надзоров12выразимо
провод119107 из 119

То есть «написать узел ещё раз» стоит 459 строк на каждую цель, семь раз, и семь копий расходятся на первой же правке. А «напечатать провод» стоит один раз на flang и ноль на каждую следующую цель.

Что из этого следует для формулировки. «Распределённость у восьми целей» законно значит только одно: два узла на разных целях печати поймут провод друг друга байт в байт, прочитают размещение одинаково и посчитают срок одинаково. Это НЕ значит «узел на Rust готов»: сокетов и часов компилятор не печатает и печатать не может — мир в язык не втаскивают.

Чем подтверждено. flang/test/self-distributed-celi.test.mjs: эталон flang/self/distributed.flang печатается в каждую из восьми целей, собирается настоящим тулчейном, запускается и отвечает на 456 вопросов — 3648 сверок, расхождений 0. Изъятие: убери один из четырёх видов кадра в эталоне — краснеют все восемь целей разом. Ветка vypusk/raspredelyonnost, 20 августа 2026.

Цена цели измерена, а не оценена (эта машина): печать 3,1—3,5 с у всех восьми; сборка — Python 0,1 с, Go 0,9 с, Rust 1,2 с, Java 1,2 с, Elixir 1,8 с, C 2,0 с, C# 5,5 с. Дешевле всего Python: тулчейна для сборки нет вовсе.

Почему не Elixir, хотя он и напрашивался. BEAM отдала бы связь даром, но вместе со связью — чужие ответы на все три вопроса распределённости (имя, отказ, доставка), и испытание проверяло бы BEAM, а не переносимость нашей модели. Провод, напечатанный компилятором в восемь целей и совпавший побайтово, переносимость как раз доказывает.

Чем ограничено. Раскодирование расходится со свидетелем на ПОРЧЕНОМ проводе: свидетель на неизвестной метке бросает, а тотальная функция бросать не умеет и возвращает «ничто». Ни одного такого кадра Закодировать не порождает, поэтому расхождение названо и оставлено. Последние 12 строк провода не перенесены не по трудности: надзорыИзПлана у свидетеля не экспортирована, и сверить эталон не с чем, не тронув файл на JavaScript. У границ кадра была та же беда и другой выход: собиратель тоже закрыт, но у него есть НАБЛЮДАЕМОЕ поведение — сколько писем узел принял из рваного потока, — и сверка пошла по нему, а не по формуле.

Связано: at-most-once-is-the-only-provable-half, what-a-scheduler-needs-proved, a-seed-orders-only-inside-one-node, number-at-the-entry-boundary-is-narrower-than-number-in-the-language


Поправка от 20 августа. Здесь стояло «мир — 459 строк, на flang нет», и строка «создатьУзел — сокеты, часы, таблица процессов, планировщик | 444 | нет». В части про сокеты и часы это неверно, и ошибка была в ЕДИНИЦЕ ЗАМЕРА: считали функции, а решение и мир лежат в них вперемешку.

Тот же кусок, посчитанный по строкам (распределённость, создатьУзел, строки 320–915 — 596 строк): мира 42 строки, и все они одного из восьми видов — createConnection, createServer, write, destroy, on, setInterval, setTimeout, Date.now. Остальные 554 — решения О сокете и О часах.

Правило, на котором разница видна без спора: «связь молчит дольше срока — считать её потерянной». Мира тут нет ни на строку: на входе две отметки часов и число, на выходе да или нет. Часы читает хозяин, РЕШАЕТ язык.

Из этого сделано: слой связи целиком переехал в flang/conc/link.flang (400 строк) чистой машиной состояний — 11 событий мира, 8 велений хозяину, одна функция «Шаг связи». Настоящий узел её ЗОВЁТ, а не повторяет: 19 прогонов flang/conc/distributed.test.mjs по настоящим сокетам зелены, а снятие из эталона одной строки — сравнения молчания со сроком — краснит ровно испытание «провод заморожен».

Печатается решение во все восемь целей: flang/test/svyaz-celi.test.mjs, 2184 вопроса каждой цели, 17 472 сверки, расхождений 0; снятие того же правила краснит все восемь разом. (Числа выросли с 1032 и 8256, когда к машине прибавились одиннадцатое событие и пятый признак связи — срок первого знакомства.)

Что в исходной заметке осталось верным. Таблица процессов и планировщик узла (219 строк кода) — по-прежнему мир и по-прежнему пишутся руками. И вывод про «узел на Rust не готов» тоже верен: печатается решение, а хозяина на цель пишут отдельно. Изменилась ЦЕНА этого хозяина, а не его необходимость.

Вторая поправка от 20 августа, к самой таблице. Последняя строка «на flang выразимо» со значением «эталона пока нет» — перевод плана в дерево надзоров — закрыта: эталон написан и сверен, и export в чужом файле для этого НЕ понадобился (см. a-reference-is-checked-against-a-third-artifact-in-the-tree). То есть из 119 строк провода на flang выражены 119 из 119. Считать это концом работы нельзя: после пересчёта выше «провод» перестал быть той единицей, в которой стоит мерить.

Связано: a-decision-about-the-world-is-portable-even-when-the-world-is-not, a-reference-is-checked-against-a-third-artifact-in-the-tree, a-this-is-not-a-refusal-rule-without-a-deadline-is-a-breakage