Из четырёх утверждений, которых ждут от планировщика процессов, ядро не берёт ни одного — и причина у каждого своя

Планировщик процессов на flang (flang/self/conc.flang, 2319 строк) — удобный пробный камень: от него ждут ровно четырёх утверждений, и они известны заранее. Проверены поимённо, и доказать удалось ноль. При этом восемь утверждений другого рода закрылись сразу и без теоремы, так что дело не в сложности планировщика, а в РОДЕ цели.

Общая часть этого уже записана и здесь не повторяется: замкнутую цель надо считать — вот откуда взялись восемь закрытых; две трети отказов ядра — сравнение длины результата с длиной входа — вот куда попали отказы. Новое здесь — что от этих двух правил остаётся конкретной предметной области.

Четыре ожидаемых утверждения и вердикт каждому.

«обработчик завершается» — доказано, но НЕ в планировщике: тотальность обработчика доказывает сам flang по программе, и по корпусу процессов это 22 из 23 (двадцать третий, «разобрать пакет» в flang/conc/examples/budget.flang, держится объявленным запасом 2000 витков — и это нарочно). В планировщике обработчик приезжает ИМЕНЕМ, строкой; утверждать о строке, что она завершается, нельзя ни в какой форме.
«запас витков не даёт бесконечного цикла» — не выразимо, и причина новая: завершение шага планировщика держится на ПАРЕ, а не на числе. По одному ребру («после пробега») строго убывает «предел пробегов минус пробегов»; по другому («тишина», когда готовых нет) пробега не происходит вовсе, зато убывает длина списка таймеров. Свести пару в одно число нельзя — пробег вправе поставить сколько угодно таймеров, границы у их числа нет, — а убывает принимает ровно ОДНО выражение. Это отказ не по форме цели, а по форме МЕРЫ, и в двух соседних заметках такого случая нет.
«надзор перезапускает ровно упавшего» — не выразимо. Ветвление идёт по признаку и по строке-стратегии, а ядро не читает условие как факт в ветви. Переписать под разбор по закрытой сумме мало: индукция по сумме закрывает случай ссылкой на пример только когда ветвь НЕ ЗАВИСИТ от груза варианта (так устроено единственное работающее место — flang/self/distributed.flang, «одна отправка даёт не более одного кадра»), а здесь зависит. Остаётся «список из одного элемента длиной 1» — пересказ тела, и он не значит ничего.
«сообщение из ящика вынимается ровно один раз» — не выразимо: это утверждение о длине списка после хвост, то есть ровно та форма, которую ядро отвергает в 55 случаях из 85.

Что закрылось вместо них. Восемь замкнутых целей, и две из них не украшение, а сторож на настоящий разрыв:

обеспечивает «стратегий надзора ровно три»    (длина результат) равен 3
обеспечивает «разрядов ровно тридцать два»    (длина результат) равен 32
обеспечивает «у поручения адресат зовётся кому» результат равен "кому"

Третье не пересказ тела: тело спрашивает словарь («Поле процесса у действия» от («Имя поручения»)), а цель называет ОТВЕТ. На стволе эти двое расходились — словарь отвечал на «поручить» пустой строкой.

Побочный измеренный факт, важный для цены. Постусловие, помеченное «доказано вычислением замкнутой цели», вычислитель ВСЁ РАВНО считает после каждого возврата. Обнаружено снятием: порча, выбросившая третью стратегию, прилетела в сверку отказом FLANG_PROPERTY, а не другим ответом, и уронила прогон вместо того, чтобы покраснеть. То есть «доказано» снимает цену в напечатанном коде, но не в прогоне на вычислителе, и всякая сверка, которая зовёт эталон, обязана считать его ОТКАЗ расхождением, а не падением.

Чем подтверждено. Ветка work/planirovshchik на основании 2bfcb7d0, node flang/bin/flang.mjs check flang/self/conc.flang --proof --pretty: утверждений 15, доказано 15, сетка 0, объявлено-не-доказано 0. До работы было

Отвергнутые кандидаты мерены тем же вызовом на копии файла: 4 постусловия

про длину списка — «объявлено, не доказано», 8 постусловий «результат не меньше нуля» на арифметике генератора — «сетка».

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

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