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

Воспроизводимость по семени кончается ровно на границе узла, и обе половины теперь числа, а не слова

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

Раньше в контракте стояло «по-видимому, невозможно». Теперь это числа.

Внутри узла — 6 семян, 12 прогонов, 36 доставок в журнале. Внутри семени журналы совпадают побайтово; между семенами вышло 6 разных журналов из 6. Вторая половина обязательна: «одно семя — один журнал» зелено и у генератора, который всегда возвращает ноль, поэтому проверка без «разные семена — разные журналы» не проверяет ничего.

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

Ловушка, из-за которой проверка чуть не оказалась пустой. У примера распределённости по одному процессу на узел, а там, где готов ровно один процесс, семени нечего выбирать — прогон был бы зелёным при любом генераторе. Понадобилось размещение, ставящее ОБА процесса на один узел; программа при этом не меняется ни на байт, потому что размещение — данные узла, а не текст программы. Это же свойство и сделало проверку возможной.

Вторая ловушка, поменьше. Сообщения надо вбрасывать в узел ОДНОЙ записью в трубу: узел разбирает кусок stdin синхронно, и тогда все они ложатся в ящик до первого пробега. Пиши по одному — и чередование начнёт зависеть от того, как хозяин нарезал трубу, то есть от чего угодно, кроме семени.

Чем подтверждено. flang/conc/distributed.test.mjs, испытания 11 и 12; ветка vypusk/raspredelyonnost, 20 августа 2026. Числа сняты прогоном на этой машине (Linux 7.0.0, Node v26.7.0, вся сеть внутри 127.0.0.1).

Чем ограничено. Про воспроизводимость внутри узла сказано только то, что проверено: один узел, два процесса, локальная доставка, ни одного сокета и ни одного таймера. Узел, у которого есть сосед, получает письма от сети, и семя их порядок не выбирает.

Связано: distribution-splits-into-world-and-wire, at-most-once-is-the-only-provable-half, quiescence-hides-deadlock