Железо: выданные окна и типизированный доступ к устройствам

Указательного типа в kola нет. Нет «сырого» адреса, который можно разыменовать, и нет приведения целого числа к месту в памяти (SPEC-CARD §12). Тем не менее kola управляет настоящим железом, а до железа добираются по адресам. Сетевая карта или последовательный порт выставляют свои органы управления в виде регистров, расположенных по фиксированным физическим адресам: чтение или запись по такому адресу обращается к устройству, а не к оперативной памяти. Это называется вводом-выводом через отображение в память, MMIO (memory-mapped I/O). Кроме того, устройства делят с процессором обычную память. При DMA (direct memory access, прямой доступ к памяти) устройство само читает и пишет RAM: например, сетевая карта забирает исходящие пакеты из кольца дескрипторов, которое заполнил драйвер. kola добирается и до того, и до другого через одну конструкцию — окно. О ней эта глава.

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

Выдачи

Если вы читали главу о файловой системе, схема вам знакома. Песочница по умолчанию закрыта, а выход из неё — выдача: оператор привязывает имя к части внешнего мира, программа запрашивает это имя, а манифест перечисляет имена, которые пакету разрешено запрашивать. --fs-root db=/var/lib/thing выдаёт каталог. Окна применяют ту же идею к физической памяти.

Капабилити называется sys.mmio: Mmio и входит в корневой набор, который получает main. Она выпускает окна по имени, и каждый запрос возвращает Option:

sys.mmio.window(b"uart0")    // -> Option[MmioWindow]  регистры устройства
sys.mmio.ram(b"ring0")       // -> Option[RamWindow]   память, общая с железом
sys.mmio.io_window(b"com1")  // -> Option[IoWindow]    портовый ввод-вывод x86

Имя, которое никто не выдал, даёт None, а не ошибку, так что программа может заметить отсутствие выдачи и продолжить работу. Вот программа целиком:

use std::log;

fn main(sys: Sys) -> u8 !{io, log} {
    match sys.mmio.ram(b"ring0") {
        Some(w) => {
            log::info(f"ring0 granted, len={w.len}");
            w.write32(0, 0xC0FFEEu32);
            let back = w.read32(0);
            log::info(f"read back {back}");
            0
        }
        None => { log::error("no ring0 grant"); 2 }
    }
}

$ kola run grant.kl --ram-window ring0=0x1000:0x100 --log stderr
[info] ring0 granted, len=256
[info] read back 12648430

$ kola run grant.kl --log stderr
[error] no ring0 grant

RamWindow — это обычная память, общая с железом. MmioWindow — блок регистров устройства. IoWindow нужен для портового ввода-вывода x86: это старое второе адресное пространство, к которому процессоры x86 обращаются специальными инструкциями in и out, а не обычными загрузками и записями. У каждого вида окна есть флаг и парная переменная окружения:

Значение записывается как base:len (port:len для портового ввода-вывода, порт не больше 0xFFFF). Длина обязательна, потому что она становится .len окна. При запуске под операционной системой (обычная программа) база игнорируется. В автономной (freestanding) сборке, которая работает прямо на железе без операционной системы, это настоящий физический адрес.

Выдачи в тестах

Тест, запрашивающий окно, получит None, если прогон его не выдаёт, поэтому драйверы пишут из двух половин. Модель (поведение устройства, конечный автомат, кодировщик) — чистый код на kola, который можно тестировать вообще без выдач. Драйвер принимает окно и тестируется прогоном, которому переданы флаги. Внутри теста набор капабилити называется sim, и kola test принимает те же флаги выдачи:

fn poke(w: &RamWindow) -> u32 !{io}
    req w.len >= 8
{
    w.write32(0, 42u32);
    w.read32(0)
}

test a_granted_window_inside_a_test(mut sim: Sim) {
    match sim.mmio.ram(b"scratch") {
        Some(w) => { let v = poke(&w); assert v == 42u32; }
        None => { assert false; }
    }
}

$ kola test tw.kl --ram-window scratch=0x0:0x40
tw.kl: test a_granted_window_inside_a_test ... ok
...
$ kola test --interp tw.kl
tw.kl: test a_granted_window_inside_a_test ... FAILED (seed 1802464353)
error[card §8]: assertion failed

Выдачи в манифесте

Пакет объявляет имена окон, которые может запрашивать, отдельным списком для каждого вида: mmio_windows, ram_windows, io_windows (см. Пакеты). Запрос необъявленного имени проваливает аудит:

[caps]
allowed = ["Sys", "Mmio", "log"]
ram_windows = ["ring0"]

$ kola audit ringdrv          # с ram_windows = []
error[pack budget]: granted window `ring0` probed via Mmio::ram / Mmio::bind_ram but not declared in [caps] ram_windows = [] — the audit signal is "wants ring0", so the name must be on the manifest (design-kernel-lowlevel.md §1.8).
audit: FAILED (1 violation(s)) — see the `error[...]` line(s) above; `kola audit` exits 1

$ kola audit ringdrv          # с объявленным именем
audit: caps within budget — pack `ringdrv` (used=["Mmio", "Sys"] ⊆ allowed=["Sys", "Mmio", "log (effect)"])
audit: ram windows — declares ["ring0"], probes ["ring0"]
audit ok: 0 violation(s) — every budget checked in this run is within its declared limits

Смещения и доказательства

Каждая операция над окном несёт встроенные контракты, которые вы не пишете и не можете отключить:

• off + size <= self.len: обращение лежит внутри окна.

• off % size == 0: естественное выравнивание для любого обращения шире байта. Четырёхбайтное обращение должно начинаться со смещения, кратного 4; иначе многие процессоры и устройства выдают исключение или ведут себя неправильно. Побайтовые массовые операции (copy_in, copy_out, zero) несут только ограничение границ.

Это обычные контракты, и доказывает их обычный прувер, поэтому работает и обычный приём: то, что нужно знать об окне, записывается в req функции драйвера, и обязательства внутри тела следуют из него. Вот кольцо дескрипторов в 256-байтном окне. Дескриптор — небольшая запись фиксированного размера, которая сообщает устройству, где лежит буфер и какой он длины. Кольцо — массив таких записей: драйвер заполняет его с одного конца (хвоста), а устройство забирает с другого (головы).

use std::log;

const RING_BYTES: usize = 256;   // выданная длина, которая нужна драйверу
const HEAD: usize  = 0x00;       // индекс потребителя (u32)
const TAIL: usize  = 0x04;       // индекс производителя (u32)
const MAGIC: usize = 0x08;       // метка раскладки (u64)
const DESC_BASE: usize = 0x10;   // первая ячейка дескриптора
const DESC_SIZE: usize = 16;
const SLOTS: usize = 15;         // 0x10 + 15 * 16 = 256

fn ring_init(w: &RamWindow) !{io}
    req w.len >= RING_BYTES
{
    w.zero(0, RING_BYTES);
    w.write64(MAGIC, 0x6b6f6c6172696e67u64);
    w.write32(HEAD, 0u32);
    w.write32(TAIL, 0u32);
}

// Где начинается ячейка `i`. Благодаря `ens` у вызывающего доказывается граница копирования.
fn slot_off(i: usize) -> usize !{}
    req i < SLOTS
    ens ret + DESC_SIZE <= RING_BYTES
{
    DESC_BASE + i * DESC_SIZE
}

fn ring_push(w: &RamWindow, slot: usize, desc: &[u8], tail: u32) !{io}
    req slot < SLOTS, desc.len == DESC_SIZE, w.len >= RING_BYTES
{
    let off = slot_off(slot);
    w.copy_in(off, desc);
    w.write32(TAIL, tail);
}

fn main(sys: Sys) -> u8 !{io, log} {
    match sys.mmio.ram(b"ring0") {
        Some(w) => {
            if w.len < RING_BYTES { log::error("ring0 is too small"); return 1; }
            ring_init(&w);
            let d = [0xEFu8, 0xBE, 0xAD, 0xDE, 0, 0, 0, 0, 64, 0, 0, 0, 1, 0, 0, 0];
            ring_push(&w, 14, &d, 1u32);
            let tail = w.read32(TAIL);
            let mut back = [0u8; 16];
            w.copy_out(0xF0, &mut back);
            log::info(f"tail={tail} b0={back[0]} b12={back[12]}");
            0
        }
        None => { log::error("no ring0 grant"); 1 }
    }
}

Карта регистров в виде именованных констант — не просто вопрос стиля. Константное смещение сворачивается при компиляции, так что и граница, и выравнивание решаются там же. Единственная проверка в main (if w.len < RING_BYTES) даёт пруверу тот факт, который нужен каждому req ниже.

kola report checks перечисляет все обязательства в файле и то, как каждое из них было закрыто:

$ kola report checks ringdrv.kl
fn ring_init
  proven   w.zero(0usize, ..)  [proved #0 + #256 <= w.len from req+guards]
  proven   w.write64(8usize, ..)  [proved #8 + 8 <= w.len from req+guards]
  proven   w.write64(8usize, ..) align  [8 % 8 == 0 (const offset)]
  ...
fn slot_off
  proven   16usize + (i * 16usize [novf: product bounded by width])  [sum bounded by width]
  proven   i * 16usize  [product bounded by width]
  proven   ens at tail  [ens discharged at this exit]
fn ring_push
  proven   req slot_off(slot)  [req discharged at this call site]
  proven   w.copy_in(off, ..)  [proved off + desc.len <= w.len from req+guards]
  ...
fn main
  proven   req ring_init(w)  [req discharged at this call site]
  proven   req ring_push(w, 14usize, &d, 1u32)  [req discharged at this call site]
  proven   w.copy_out(240usize, ..)  [proved #240 + #16 <= w.len from req+guards]
  ...
13 mmio site(s): 13 proven at compile time, 0 runtime

В прикладном коде недоказанная граница допустима: она превращается в проверку во время выполнения, и если та не проходит, срабатывает трап с диагностикой. В ядре этот трап принять некому. Если в отчёте драйвера есть хоть одно место с проверкой окна во время выполнения, в нём сидит падение, которое ещё не нашёл ни один тест, поэтому для кода ядра цель — ноль таких мест. Если функция не доходит до проверяемого IR, отчёт говорит об этом и называет причину, так что чистый счёт по проанализированным функциям никогда не выдаётся за чистый счёт по всей программе. Отчёт отражает прувер того компилятора, который вы запускаете, поэтому его стоит перезапускать, а не цитировать.

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

// req off + FRAME <= w.len
({ KRamWindow kt1 = (*(w)); size_t kt2 = (size_t)(off); size_t kt3 = (size_t)(k_dma__FRAME);
   /*IR:ram-bounds*/ k_dma_writeback((void *)(kt1.base + kt2), kt3); (void)0; });

// без req
({ KRamWindow kt1 = (*(w)); size_t kt2 = (size_t)(off); size_t kt3 = (size_t)(n);
   if (kt2 > kt1.len || kt1.len - kt2 < kt3)
       k_trap("ram dma_writeback out of range: off + len > window len (card §7)");
   k_dma_writeback((void *)(kt1.base + kt2), kt3); (void)0; });

Здесь же видно, что значит «непрозрачная база»: адрес появляется только как kt1.base + kt2 и собирается в точке использования из базы, которую не может назвать ни одно выражение kola, и смещения, которое kola вычислила и доказала.

Если границу или выравнивание доказать нельзя, вы получаете проверку во время выполнения. Невыровненное константное смещение — не ошибка компиляции, а обязательство, которое не выполнится при запуске:

use std::log;

fn read_status(w: &RamWindow) -> u32 !{io}
    req w.len >= 0x20
{
    w.read32(0x06)     // 6 % 4 != 0: невыровненное обращение к слову
}

fn main(sys: Sys) -> u8 !{io, log} {
    match sys.mmio.ram(b"regs") {
        Some(w) => {
            if w.len < 0x20 { return 2; }
            let s = read_status(&w);
            log::info(f"status={s}");
            0
        }
        None => { log::error("no grant"); 1 }
    }
}

$ kola report checks misrun.kl
fn read_status
  proven   w.read32(6usize)  [proved #6 + 4 <= w.len from req+guards]
  RUNTIME  w.read32(6usize) align
...
$ kola run misrun.kl --ram-window regs=0x0:0x40 --log stderr
trap: error[card §7]: ram read32 misaligned: off 0x6 % 4 != 0 on window `regs`
  --> misrun.kl:6:5
   = help: a RAM-window word access must be naturally aligned: the op's builtin contract is `off % N == 0`

Виды окон

Одна капабилити выпускает окна нескольких типов. Каждое различие между ними отражает то, что делает железо за окном.

У MmioWindow восемь операций, read8/16/32/64 и write8/16/32/64, и больше ничего. Каждое обращение volatile: компилятор не вправе объединить, повторить или выбросить его, как сделал бы с обычной памятью, потому что у чтения регистра бывают побочные эффекты (оно забирает очередной байт из очереди приёма или сбрасывает бит состояния). Кроме того, обращения упорядочены так, как их видит устройство. Обычно процессор ради скорости переставляет операции с памятью, а барьер — это инструкция, которая такие перестановки запрещает. Обращению к MmioWindow барьер не нужен: запись выполняется после всех предыдущих записей, а чтение — до всех последующих загрузок. Поэтому записать дескриптор в RamWindow, а затем записать регистр-«звонок» (doorbell, регистр, сообщающий устройству, что появилась новая работа) безопасно ровно в таком виде.

У RamWindow те же восемь операций с теми же контрактами и вдобавок побайтовое массовое семейство: copy_in(off, src), copy_out(off, dst) и zero(off, n). Скопировать дескриптор в ячейку — это одно копирование памяти, а не шестнадцать записей по байту. Поскольку это обычная память, простые операции этого окна относятся к ряду io. Два его семейства относятся к hw; о них ниже.

У IoWindow шесть операций, а не восемь. Инструкции x86 in и out работают максимум с 32 битами, поэтому 64-битной пары у типа нет, и попытка её вызвать — ошибка компиляции с объяснением причины:

fn probe(w: &IoWindow) -> u64 !{hw}
    req w.len >= 8
{
    w.read64(0)
}

error[card §7]: `IoWindow` has no `read64`: x86 port I/O is 8/16/32-bit only
  --> io64.kl:4:5
   = help: an I/O-space window lowers to in/out (inb/inw/inl, outb/outw/outl) — there is no 64-bit port op. Use read32/write32, or split the access; for a 64-bit MMIO register use `sys.mmio.window` (a memory window has read64) (design-kernel-lowlevel.md §2.3)

В автономной сборке IoWindow превращается в in/out на x86 и отвергается на всех остальных архитектурах.

Сужение окна RAM

У RamWindow два ослабления. Оба !{}, не требуют выдачи и ничего не стоят во время выполнения, потому что сузить уже имеющееся полномочие всегда безопасно. Это тот же ход, что Dir → DirRo в главе о файловой системе.

w.ro() даёт RamWindowRo, у которого есть read8/16/32/64, copy_out, .len и одна собственная операция, snapshot (о ней ниже). Операций записи, copy_in, zero и операций DMA у этого типа просто нет, так что читатель, который пытается писать, не скомпилируется:

// Ослабление бесплатно: ни выдачи, ни эффекта, ни аргумента-капабилити.
fn narrow_it(w: &RamWindow) -> RamWindowRo !{} {
    w.ro()
}

fn bump(ro: &RamWindowRo) !{io}
    req ro.len >= 8
{
    let s = ro.read32(0);
    ro.write32(0, s + 1u32);
}

error[card §7]: `RamWindowRo` is the READ-ONLY half of a RAM window — `write32` writes, and the write half does not exist on this type
  --> rowrite.kl:5:5
   = help: `w.ro()` ATTENUATES a `RamWindow`: the result carries `read8/16/32/64`, `copy_out`, `.len` and `snapshot`, and nothing that mutates ...

w.atomic() даёт AtomicWindow, у которого есть .len и больше ничего. До его ячеек можно добраться только одним способом: передать окно как аргумент с ячейками в операцию Atomic:: (Машина). Код, у которого есть AtomicWindow, не может обратиться к этим ячейкам иначе. Это исключает классическую ошибку: одно ядро пишет ячейку атомарно, а другое — обычной записью; на некоторых машинах это работает, но ни в одной модели памяти не корректно. atomic() не расходует исходное окно, так что гарантию даёт тип параметра того кода, которому вы передаёте AtomicWindow.

Окна, которые ядро создаёт само

Ещё две операции создают RamWindow, и обе предназначены для ядер, а не для выдач. Mmio::reserve(name, size, align) просит компилятор выделить память, которой владеет kola и до которой можно добраться только через возвращённое окно; имя и оба размера должны быть константами. Mmio::bind_ram(name, base, len) создаёт окно над адресом, который программа узнаёт во время выполнения, например над PCI BAR или базой кадрового буфера из протокола загрузки, а bind_window/bind_io_window делают то же для окон устройств. Имя по-прежнему должно быть объявлено в списке пакета для своего вида (ram_windows, mmio_windows, io_windows); на необъявленное имя ответ — None.

reserve и bind_ram работают и в сборках под ОС: адрес игнорируется, и используется обнулённый буфер запрошенной длины, что честно моделирует обычную память. bind_window и bind_io_window доступны только в автономных сборках. Регистр устройства не возвращает при чтении то, что в него записали, так что буфер на его месте позволил бы тесту «записать, затем прочитать» пройти на хосте и упасть на железе.

Seqlock

У RamWindowRo есть одна собственная операция: snapshot(seq_off, off, &mut dst) -> bool, чтение по протоколу seqlock. Писатель на другом ядре делает слово последовательности нечётным, записывает данные и снова делает слово чётным. Читатель копирует данные, пока слово чётное и не меняется за время копирования; иначе он повторяет попытку. Смысл в том, чтобы избежать разорванного чтения — копии, в которой смешаны байты двух разных записей, — и при этом не заставлять писателя ждать читателей. Так публикуют данные кольца дескрипторов сетевых карт и модули ядра, отдающие своё состояние в пользовательское пространство.

Сторона записи — одна операция на полном окне, publish(seq_off, off, &src) -> bool:

use std::log;

const SEQ: usize = 0x40;   // слово последовательности (u32)
const DATA: usize = 0x00;  // данные, которые оно охраняет

// У читателя есть только окно для чтения.
fn read_epoch(ro: &RamWindowRo, dst: &mut [u8]) -> bool !{io}
    req ro.len >= 0x80, dst.len == 8
{
    ro.snapshot(SEQ, DATA, dst)
}

// Писатель: одна операция владеет обеими границами упорядочивания.
fn publish_epoch(w: &RamWindow, src: &[u8]) -> bool !{io, hw}
    req w.len >= 0x80, src.len == 8
{
    w.publish(SEQ, DATA, src)
}

fn main(sys: Sys) -> u8 !{io, hw, log} {
    match sys.mmio.ram(b"hdr") {
        Some(w) => {
            if w.len < 0x80 { return 2; }
            let payload = [0xEFu8, 0xBE, 0xAD, 0xDE, 0, 0, 0, 0];
            let published = publish_epoch(&w, &payload);
            let ro = w.ro();
            let mut buf = [0u8; 8];
            let ok = read_epoch(&ro, &mut buf);
            log::info(f"published={published} ok={ok} b0={buf[0]}");

            w.write32(SEQ, 3u32);              // нечётное слово: публикация в процессе
            let mut buf2 = [0u8; 8];
            let ok2 = read_epoch(&ro, &mut buf2);
            let again = publish_epoch(&w, &payload);
            log::info(f"mid-publish ok={ok2} b0={buf2[0]} publish={again}");
            0
        }
        None => { log::error("no hdr grant"); 1 }
    }
}

$ kola run seq.kl --ram-window hdr=0x0:0x80 --log stderr
[info] published=true ok=true b0=239
[info] mid-publish ok=false b0=0 publish=false

kola run --native печатает те же две строки. Посмотрите на вторую. Слово последовательности нечётное, читатель отказался, и buf2 по-прежнему заполнен нулями: dst записывается только при успехе, так что разорванный снимок не возникает вообще, даже с предупреждением. Числа повторных попыток в параметрах нет: правильная граница зависит от критической секции писателя, а не от вызывающего. publish симметричен: если слово уже нечётное, он отвечает false и ничего не пишет, так что две публикации не могут переплестись в разорванную страницу.

Внутри среды выполнения publish читает чётное слово последовательности, записывает его нечётным, ставит барьер store-store (он не даёт записи нечётного слова переместиться за записи данных), копирует src.len байтов по смещению off и записывает слово чётным с семантикой release. Контракты у него те же два, что у snapshot (off + src.len <= self.len и seq_off + 4 <= self.len). Он относится к ряду hw, потому что сказать «с упорядочиванием, на которое полагается другое ядро» может только ряд эффектов. Данные копируются, потому что операция, владеющая обеими границами упорядочивания, должна владеть и тем, что происходит между ними, а замыканий, через которые можно было бы передать среде выполнения критическую секцию, в kola нет.

Модели устройств

Окно выдаёт физическую память, а у процесса под операционной системой её нет. Что стоит за окном, когда программа запущена на ноутбуке, зависит от вида окна.

RamWindow ничего не нужно: обычная память уже хорошо моделирует обычную память — записали байт, прочитали его же. Поэтому драйвер кольца работал с выдачей и без модели, и поэтому kola run и kola run --native дают для него одни и те же байты.

MmioWindow или IoWindow модель нужна, потому что регистр — не память. Регистр только для чтения игнорирует записи; регистр состояния сбрасывается при чтении; счётчик отвечает текущим временем. Поведение регистра — функция, поэтому модель — это три функции над объявленным вами типом состояния:

fn p_new() -> M !{}
fn p_read(m: &mut M, off: usize, width: usize, now: u64) -> u64 !{}
fn p_write(m: &mut M, off: usize, width: usize, val: u64, now: u64) !{}

width задаётся в байтах (1, 2, 4 или 8). now — часы набора капабилити: виртуальные под Sim, настенные под Sys. Три функции привязываются по общему префиксу: --sim-mmio timer0=tm использует tm_new, tm_read и tm_write (mod::tm ищет их в модуле mod). Вот таймер со счётчиком только для чтения и флагом состояния, который сбрасывается при чтении, вместе с драйвером к нему:

use std::log;

const T_CTRL: usize  = 0x00;  // чтение и запись: бит включения
const T_COUNT: usize = 0x08;  // только чтение: текущий счёт
const T_STAT: usize  = 0x10;  // флаг ожидания, сбрасывается при чтении

// Модель: три чистые функции над собственной структурой состояния.
struct TimerModel { ctrl: u64, base: u64, fired: bool }

fn tm_new() -> TimerModel !{} {
    TimerModel { ctrl: 0, base: 0, fired: false }
}

fn tm_read(m: &mut TimerModel, off: usize, width: usize, now: u64) -> u64 !{} {
    if off == T_CTRL { return m.ctrl; }
    if off == T_COUNT {
        if m.ctrl == 0 { return 0; }
        return now - m.base;
    }
    if off == T_STAT {
        let s = if m.fired { 1u64 } else { 0u64 };
        m.fired = false;           // сбрасывается при чтении
        return s;
    }
    0
}

fn tm_write(m: &mut TimerModel, off: usize, width: usize, val: u64, now: u64) !{} {
    if off == T_CTRL {
        m.ctrl = val & 1;
        m.base = now;
        m.fired = true;            // включение поднимает флаг ожидания
    }
    // T_COUNT и T_STAT только для чтения: запись в них игнорируется.
}

// Драйвер: написан для окна и ничего не знает о модели.
fn timer_arm(w: &MmioWindow) -> u64 !{hw}
    req w.len >= 0x18
{
    w.write64(T_CTRL, 1u64);
    w.write64(T_COUNT, 999u64);    // регистр только для чтения: игнорируется
    let c = w.read64(T_COUNT);
    let s0 = w.read64(T_STAT);     // 1: ожидание
    let s1 = w.read64(T_STAT);     // 0: сброшен первым чтением
    let mut acc = (s0 << 8) | s1;
    if c != 999 { acc = acc | (1u64 << 16); }
    acc
}

fn main(sys: Sys) -> u8 !{io, hw, log} {
    match sys.mmio.window(b"timer0") {
        Some(w) => {
            if w.len < 0x18 { return 2; }
            let acc = timer_arm(&w);
            log::info(f"acc={acc}");
            0
        }
        None => { log::error("no timer0 grant"); 1 }
    }
}

test status_clears_on_read {
    let mut m = tm_new();
    tm_write(&mut m, T_CTRL, 8, 1, 0);
    let first = tm_read(&mut m, T_STAT, 8, 0);
    let second = tm_read(&mut m, T_STAT, 8, 0);
    assert first == 1;
    assert second == 0;
}

test the_count_register_ignores_writes {
    let mut m = tm_new();
    tm_write(&mut m, T_CTRL, 8, 1, 100);
    tm_write(&mut m, T_COUNT, 8, 999, 100);
    let c = tm_read(&mut m, T_COUNT, 8, 140);
    assert c == 40;
}

$ kola test timer.kl
timer.kl: test status_clears_on_read ... ok
timer.kl: test the_count_register_ignores_writes ... ok
...
$ kola run timer.kl --mmio-window timer0=0x0900_0000:0x18 --sim-mmio timer0=tm --log stderr
[info] acc=65792

Тесты проверяют модель напрямую, без выдач и флагов. Каждое чтение регистра сначала связывается через let и только потом попадает в assert: выражение assert не вправе менять состояние, а регистр, сбрасывающийся при чтении, его меняет. Под kola run --native модель компилируется в программу, так что нативная сборка даёт тот же ответ.

Для этих двух видов окон привязка модели обязательна, и проверяется она при запуске, ещё до того, как начнёт работать программа. Обе ошибки отвергаются с указанием недостающего флага:

$ kola run timer.kl --mmio-window timer0=0x0:0x18
error[card §7]: mmio window `timer0` is granted but has no model binding — hosted runs back windows with a SimMmio model
  = help: add --sim-mmio timer0=<prefix> (or KOLA_SIM_MMIO_timer0=<prefix>): the prefix names three program fns `<p>_new`/`<p>_read`/`<p>_write` (design-kernel-lowlevel.md §1.3); `mod::<p>` resolves them in module `mod`

$ kola run timer.kl --sim-mmio timer0=tm
error[card §7]: mmio model `timer0` is bound but the window was never granted — a binding backs a GRANT, it does not create one
  = help: add --mmio-window timer0=0x0:LEN (len is REQUIRED and sizes the window's `.len`; the base is ignored under hosted run/test — design-kernel-lowlevel.md §1.2)

Ряды эффектов: io для памяти, hw для машины

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

Одна капабилити Mmio выпускает окна для обоих рядов, потому что память, общая с железом, — это обычная память, а обращение к регистру устройства — привилегированная операция. Поэтому операции со словами и массовые операции RamWindow относятся к io; его пара операций с кешем для DMA, записи с release и publish — к hw; всё у MmioWindow и IoWindow — к hw. Ряды проверяются:

fn probe(w: &MmioWindow) -> u32 !{io}
    req w.len >= 8
{
    w.read32(0)
}

error[card §6]: `probe` performs `hw` (mmio read) but does not declare it
  --> rowmiss.kl:4:5
   = help: add `hw` to the effect clause, or hand the work to a caller that has it

Процессор держит недавно использованную память в кеше, а на многих чипах движок DMA читает RAM напрямую, не заглядывая в этот кеш. Поэтому прежде чем устройство прочитает буфер, записанный процессором, грязные строки кеша нужно записать обратно в RAM, а после того как устройство запишет буфер, устаревшую копию в кеше процессора нужно выбросить. Пара операций с кешем для DMA делает ровно это: dma_writeback(off, n) выписывает диапазон из кеша данных, а dma_invalidate(off, n) выбрасывает кешированную копию, чтобы процессор увидел то, что записал движок. Обе несут то же ограничение границ, что и массовое семейство. Они доступны только в автономных сборках, и нативная сборка под ОС объясняет почему:

const FRAME: usize = 64;

// Выписать один кадр из кеша данных до того, как его прочитает движок DMA.
fn tx_frame(w: &RamWindow, off: usize) !{hw}
    req off + FRAME <= w.len
{
    w.dma_writeback(off, FRAME);
}

fn main(sys: Sys) -> u8 !{io, hw} {
    match sys.mmio.ram(b"ring0") {
        Some(w) => {
            if w.len < FRAME { return 2; }
            tx_frame(&w, 0);
            0
        }
        None => 1,
    }
}

$ kola run --native dma.kl --ram-window ring0=0x0:0x1000
codegen: native codegen: `w.dma_writeback(...)` in `tx_frame` has no HOSTED native lowering (design-hot-datapath.md §2.1b: a hosted process has no cache to maintain) — interpret it (`kola run|test`), or build `--freestanding`, where the per-arch KOLA_HOT_DMA table lowers it ...

$ kola build --freestanding dma.kl -o out
build ok (freestanding): 2 native fn(s), 0 exported item(s) (0 fn, 0 const, 0 type) → out/dma.o

В интерпретаторе операции с кешем ничего не делают, и это верно: процессу под ОС нечего выписывать. Значения те же самые, а эффект, ради которого операция существует, там не наблюдается.

Где кончается симуляция

Интерпретатор — оракул для значений, и только для них. Он скажет, что кодирование дескрипторов правильное, что смещения в пределах окна, что конечный автомат переходит из состояния в состояние верно. Он не может сказать, что барьер стоит на месте, что строка кеша выписана или что два ядра видят одно и то же. Не скажет этого и сравнение двух исполнителей с одним и тем же слепым пятном. Интерпретатор однопоточный, поэтому запись с release, барьер и обычная запись для него выглядят одинаково.

Реальный пример показывает этот разрыв. Кеш работает блоками фиксированного размера — строками, поэтому цикл выписывания проходит диапазон по строке за шаг. На MIPS операции с кешем для DMA берут размер строки из конфигурационного регистра CP0. Однажды среда выполнения читала не тот селектор регистра. Полученное значение заставляло цикл делать слишком большой шаг и проходить окно всего один раз, так что вторая строка кеша каждого кадра не выписывалась, и движок DMA отправлял устаревшие байты: кадры в сети обрывались ровно на 32-м байте. Все прогоны под ОС проходили, кросс-ассемблирование тоже, потому что неверный селектор регистра ассемблируется без единой ошибки. Показал это только запуск на настоящем чипе.

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