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

Вычисленный адресат стоит ровно одного названного отказа, и платит за него отправитель

Типизированная ссылка закрыла статическую половину дыры: тип груза сверяется с типом ссылки при проверке типов. Динамическая половина оставалась открытой и была названа в typed-process-reference-is-already-expressible: строка, приехавшая с провода, вправе назвать процесс, принимающий совсем другое.

Закрывается это одним правилом в слое процессов: при отправке планировщик сличает объявленный принимает адресата с именем варианта письма и отказывает названно — FLANG_PROCESS_ACCEPTS, — приписывая отказ ОТПРАВИТЕЛЮ. Адресата выбрал он, и выбрал по строке, за которую отвечает он же.

Улика ДО. flang/conc/examples/node-name-of-a-foreign-kind.flang: узел получает с провода имя «Журнал», чеканит на него «Ссылка» от «Задание» и шлёт работу, а «Журнал» объявлен принимающим «Строка журнала». Программа собирается без единого замечания (flang check, код возврата 2 — это «processes и runs не судит никто», а не замечание). Прогон на BEAM до правки:

"живые":["узел-7","Узел"]  "отказы":[["Журнал","FLANG_MATCH_NOT_EXHAUSTIVE"]]
"ok":true  "исход":"покой"  код возврата 0

Умер ПОЛУЧАТЕЛЬ, кодом про неполный разбор, а прогон дошёл до покоя и назвался удавшимся. После правки, тот же прогон:

"живые":["узел-7","Журнал"]  "отказы":[["Узел","FLANG_PROCESS_ACCEPTS"]]

Получатель жив, отказ у отправителя и назван.

Чем подтверждено, что правка бьёт только сюда. Все 14 программ flang/conc/examples/ напечатаны в JavaScript и прогнаны, каждый объявленный прогон, до и после: 25 строк «пример, прогон, исход, живые, отказы», сверено diff-ом полных списков. Разошлась ровно одна строка из 25 — та самая. Ветка u/ssylka-na-process2, двоичный собран из перепечатанного семени.

Ссылка ПЕРЕСЫЛАЕТСЯ письмом, и по ней приходит ответ — это отдельная программа, flang/conc/examples/node-reply-by-reference.flang, и без неё разговор о распределённых службах был бы половинчатым. Ссылка лежит полем груза:

вариант «Посчитать» содержит «вход»: строка, «ответить»: «Ссылка» от «Итог»

Имени сборщика в коде работника нет ни буквой — есть ссылка, приехавшая в письме. Оба имени приезжают полями сообщений. Прогон на BEAM: состояние «Сборщика» → {"итоги":["узел-7: раз"]}, "живые":["узел-7","Сборщик","Узел"], "отказы":[], код возврата 0. Тип ответа при этом сверяется обычной проверкой типов — на обычном применении полиморфной функции «Послать» от «Т».

Попутно измерено, и это меняет счёт. Сегодняшний компилятор про отправить не проверяет НИЧЕГО — ни существования адресата, ни типа груза, даже когда адресат написан буквами в исходнике. Два прогона: программа, шлющая "узел-7" груз чужого типа, и программа, шлющая процессу "нет такого", — обе проходят flang check без единого замечания. Прежняя проверка addresseeOf жила во второй реализации на JavaScript, а та удалена; в компилятор на самом языке она не переехала. Значит ссылка сегодня — не замена прежней проверке, а ЕДИНСТВЕННАЯ статическая проверка груза, какая вообще есть.

Цена, названная числом. Правок четыре: два планировщика цели печати (flang/src/emit/js/flang_conc.js, flang/src/emit/elixir/flang_conc.ex) и два печатника плана (flang/self/emit-js.flang, flang/self/emit-elixir.flang), где в план добавлены два поля: объявленный тип и имена его вариантов. Плюс эталон слоя (flang/self/conc.flang) и множество отказов (flang/self/failures.flang, вид одиннадцатый). Перепечатка семени — 22 минуты, пик 25,2 ГиБ.

Достижимость нового вида решается точно, а не оценкой сверху. Отказ возможен тогда и только тогда, когда адресат отправить или через ВЫЧИСЛЯЕТСЯ, а не литерал. Это ровно то место, где раньше стоял запрет «адресат обязан быть литералом»: запрета нет, а цена названа и попадает в множество отказов процесса, которое обязан покрыть надзор.

Чем ограничено.

Связано: typed-process-reference-is-already-expressible, an-addressee-must-be-a-literal-for-the-payload-type-not-for-the-scheduler, equality-on-a-type-parameter-is-banned-only-in-bodies