Драйвер MSI на flang

docs/examples/driver/msi/msi.flang — контроллер MSI моста PCIe JH7110 (плата VisionFive 2, мост PLDA XpressRICH), переписанный на flang с драйвера из ядра NetBSD. Источник — файлы jh7110_pcie_msi.c (сам контроллер) и jh7110_pcievar.h (типы и адреса регистров) в каталоге sys/arch/riscv/starfive нашей ветки дерева NetBSD; в апстриме этого драйвера нет. Проверялось одно утверждение: перенос драйвера на язык с доказательствами упирается в объём, а не в возможность.

Границы. В ядро это не собирается, на плате не пробовалось, рабочий драйвер не заменяет. Дерево NetBSD при этой работе только читалось.

Приём: драйвер ничего не пишет, он отвечает, что записать

Каждая функция чистая: «состояние контроллера и событие → новое состояние, список записей в регистры и список разрядов, которые надо раздать». Тот же приём, что у драйвера UART docs/examples/driver/uart.flang и у распределителя памяти.

тотальная функция «Занять вектор»
  принимает контроллер: «Состояние MSI», вектор: неотрицательное, безопасен: признак
  возвращает «Отклик MSI»

Хозяина на C в этом каталоге нет. Его работа — цикл: прочитать слово состояния MSI, позвать «Раздать прерывание», для каждого разряда отклика выполнить запись «сброс» и, если поле «звать» истинно, позвать обработчик вектора.

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

Что языку пришлось заменить:

побитовых операций нет — слово состояния разбирается спуском по остаткам от двух («Шаг раздачи», «Младший бит взведён», «Бит взведён»), а сдвиг единицы на номер вектора — умножением («Вес вектора»);
шестнадцатеричных литералов нет — адреса регистров записаны десятичными, и каждый перевод стоит отдельным обещанием: «PLDA_IMASK_LOCAL — 0x180, оно же 384», «PLDA_ISTATUS_LOCAL — 0x184, оно же 388», «PLDA_IMSI_ADDR — 0x190, оно же 400», «PLDA_ISTATUS_MSI — 0x194, оно же 404»;
тишины return NULL нет — неизвестный вектор даёт отказ, названный словами в поле «отказ» отклика; в железо и в состояние при этом ничего не пишется (семья обещаний «ОТКАЗ ЧЕСТЕН»).

Что лежит в файле

Файл один, 426 строк .

Типы: «Запись в регистр» (адрес, значение), «Разряд» (вектор, сброс, звать), «Вектор MSI» (занят, обработчик, безопасен), «Состояние MSI» (звонок, адрес маски, маска, векторы, включён), «Отклик MSI» (состояние, записи, разряды, отказ).

Функции по группам:

группа	функции
константы регистров и их различие	«Регистр местной маски», «Регистр местного состояния», «Регистр звонка», «Регистр состояния MSI», «Бит MSI в местной маске», «Число векторов», «Адреса регистров различны»
граница и биты	«Вектор в пределах», «Вес вектора», «Бит взведён», «Младший бит взведён», «Маска со взведённым», «Маска со сброшенным», «Предел маски»
годность состояния	«Годное состояние»
таблица векторов	«Номера векторов», «Свежие векторы», «Шаг правки», «Проход правки», «Правка вектора»
установка и снятие обработчика	«Занять вектор», «Освободить вектор»
раздача прерывания	«Шаг раздачи», «Начало раздачи», «Раздать прерывание»
запуск	«Запустить контроллер»

Взято из драйвера: разбор слова состояния MSI и раздача по векторам (jh7110_pcie_msi_dispatch), установка обработчика с проверкой границы и взведением бита маски (jh7110_pcie_msi_intr_establish), снятие обработчика со сбросом того же бита (ветвь MSI в jh7110_pcie_intr_disestablish), запуск — чтение звонка, перевзвод захвата MSI, обнуление таблицы, снятие маски (jh7110_pcie_msi_init), все адреса регистров и константы.

Оставлено: программирование capability MSI устройства (jh7110_pcie_msi_program — смещения находит pci_get_capability во время работы), распределение выровненных отрезков векторов (jh7110_pcie_msi_find_run, jh7110_pcie_msi_alloc_common), переговоры MSI/MSI-X/INTx (jh7110_pcie_intr_alloc), функции MSI-X (в этом мосте его нет), взаимное исключение, выделение памяти и отладочная печать — это работа хозяина.

Как запустить

bootstrap/flang check docs/examples/driver/msi/msi.flang --proof
bootstrap/flang test  docs/examples/driver/msi/msi.flang

Отчёт --proof печатает вердикт по каждому постусловию и последней строкой — сколько утверждений доказано, сколько на сетке, сколько объявлено без доказательства. Этих чисел на странице нет: они меняются вместе с ядром. Замер на определённую дату, до и после правки свёртки, стоит в разделе о неравенствах на странице какие обещания ядро берёт.

Что доказано и что нет

Все функции тотальны. У двух — «Вес вектора» и «Бит взведён» — завершение доказано постоянным шагом, и для них в напечатанный код ставится проверка убывания: спуск идёт по типу число (разность неотрицательное минус 1 в неотрицательное не втекает), а на IEEE-754 постоянный шаг не всегда меняет величину. У остальных — композицией, без проверок в напечатанном коде.

Утверждений вида «объявлено, не доказано» в отчёте нет.

Доказано обо всех входах:

граница номера вектора — «ВЕКТОР МЕНЬШЕ ТРИДЦАТИ ДВУХ — СВОЙ», «ВЕКТОР ОТ ТРИДЦАТИ ДВУХ И ВЫШЕ — ЧУЖОЙ»; на железе выход за неё — запись за конец массива обработчиков;
адреса — каждый перевод из шестнадцатеричной записи, «ЗВОНОК НЕ ПУТАЕТСЯ С ОСТАЛЬНЫМИ ТРЕМЯ», «ЗВОНОК ПИШЕТСЯ ПО СВОЕМУ АДРЕСУ И ТОЛЬКО ПО НЕМУ» (запуск пишет ровно две записи, и обе названы поимённо), «W1C ПИШЕТСЯ ПО PLDA_ISTATUS_MSI И ТОЛЬКО ПО НЕМУ», «МАСКА ПИШЕТСЯ ПО СВОЕМУ АДРЕСУ, А НЕ ПО ЗВОНКУ»;
разбор маски на одном шаге — взведённый бит даёт ровно один разряд и растит счёт ровно на один, сброшенный не даёт ничего;
отказ — «ОТКАЗ ЧЕСТЕН: чужой вектор назван словами», «… в железо не пишут», «… состояние не трогают», «СВОЙ ВЕКТОР ОТКАЗА НЕ ДАЁТ» — у занятия и у освобождения;
таблица векторов — «ПРОХОД СОБИРАЕТ РОВНО СТОЛЬКО, СКОЛЬКО ПРОШЁЛ» и «ЦЕЛЬ ПРОХОДОМ НЕ МЕНЯЕТСЯ» у «Проход правки» доказаны индукцией по свёртке, и из них — «ТАБЛИЦА НЕ МЕНЯЕТ ДЛИНЫ» у «Правка вектора». Для этого свёртка вынесена в отдельную функцию, у которой она — всё тело: свёртка под проекцией поля принципа индукции ядру не показывает;
годность у раздачи — «ШАГ СОХРАНЯЕТ ГОДНОСТЬ ЦЕЛИКОМ» у «Раздать прерывание»: раздача состояния не меняет.

На сетке (проверено примерами функции, не доказано):

постусловие	функция	почему
«это тот же нулевой разряд, что читает Бит взведён»	«Младший бит взведён»	справа рекурсивная функция; ядро сверяет равенство на конечном наборе значений
«ШАГ СОХРАНЯЕТ ГОДНОСТЬ ЦЕЛИКОМ: из годного состояния выходит годное»	«Занять вектор»	годность содержит неравенство «маска меньше предела», а арифметики неравенств у ядра нет
«ШАГ СОХРАНЯЕТ ГОДНОСТЬ ЦЕЛИКОМ: из годного состояния выходит годное»	«Освободить вектор»	то же

Что от годности всё-таки доказано у занятия и освобождения: длина таблицы не меняется, бит вектора в маске взводится и сбрасывается, звонок и адрес маски не меняются, на чужом векторе состояние не трогают.

Одно доказанное обещание пусто как запись. «НЕ ТЕРЯЕТ ВЕКТОРОВ (ИНВАРИАНТ ЦИКЛА)» у «Шаг раздачи» — «если до шага разрядов было столько же, сколько взведённых бит, то и после» — выполняется при любом теле, которое прибавляет к счёту и к списку разрядов одно и то же. Содержание несут четыре обещания рядом: они пришпиливают прирост к конкретному числу. Инвариант оставлен ради формулировки, а не ради доказательной силы.

Чего не гарантирует

Работы на плате и сборки в ядро. Не пробовалось.
Годности состояния после занятия и освобождения в общем виде — сетка, см. выше.
Распределения векторов, программирования capability MSI, MSI-X — не переписаны.
Взаимного исключения и памяти — у чистой функции их нет, это работа хозяина.