/
Поиск
RU
ENRU

Голое железо: узлы устройств, freestanding-сборки и layout-утверждения

kola создавался для стека, под которым нет операционной системы: гипервизора, файловой системы, маршрутизатора на плате с MIPS. Поэтому C ABI и цель «голое железо» — часть самого смысла существования языка. Из этого вытекают два направления, и о них эта глава. Первое — доступ к устройству через ОС: Dev, капабилити для символьных устройств в пространстве пользователя. Второе — поставка туда, где ОС нет вовсе: kola build --freestanding, статическая арена вместо malloc и объектный файл, чей список неопределённых символов показывает, на чём программа ещё может упасть. Между ними стоит layout_assert: он позволяет заявить раскладку структуры в C и поручить её проверку компилятору C.

Выданные окна MMIO и RAM описаны в главе Железо: выданные окна и типизированный доступ к устройствам, интринсики Cpu и атомики SMP — в главе Машина: Cpu, упорядочивание памяти и атомарные операции. Здесь они упоминаются только там, где пересекаются с темой главы.

Dev: узел устройства — собеседник, а не окно

В Linux и других Unix-системах драйвер обычно предстаёт перед обычными программами как узел устройства — специальный файл вроде /dev/widget. Программа открывает его как файл и получает файловый дескриптор (небольшое целое число, которым ядро обозначает открытый объект). Дальше она общается с драйвером вызовами ioctl — каждый из них представляет собой пронумерованный запрос с небольшим буфером аргументов — и может запросить mmap, чтобы страница памяти драйвера отобразилась прямо в её адресное пространство. Допустим, демону в пространстве пользователя нужно общаться с модулем ядра через /dev/widget. Для железа в kola уже есть капабилити Mmio (memory-mapped I/O: регистры устройства, которые процессор читает и пишет так, будто это память), и она выдаёт окна трёх видов (MmioWindow, RamWindow, IoWindow). Добавить четвёртый было бы легко, но kola этого не делает, и причин две.

Первая — назначение капабилити: отвечать на вопрос аудита. Если бы Mmio охватывала ещё и открытие узлов устройств, строка Mmio в манифесте перестала бы отличать драйвер на голом железе, который трогает регистры UART, от демона, который открывает узлы и шлёт ioctl. Рецензент вынес бы из неё ложный вывод в обе стороны.

Вторая — природа самой вещи. Окно — это выданный диапазон адресов. В момент выдачи ничего не может сломаться, и по ту сторону никого нет. У узла устройства есть жизненный цикл и протокол: open может не удаться, ioctl — это запрос, который драйвер вправе отклонить, а у самого драйвера своя машина состояний. Это гораздо ближе к сетевому соединению, чем к диапазону памяти. На окно похожа только отображённая страница, да и та приходит через протокол. Fs не подходит по похожей причине: /dev/widget — абсолютный путь вне любого корня песочницы, а ioctl и mmap — не файловые операции.

Поэтому sys.dev: Dev — отдельная капабилити. Это маркер полномочия, и его можно бросить на любом пути. Device — линейный дескриптор: его нужно израсходовать ровно один раз на каждом пути выполнения (здесь — вызовом close), потому что он владеет файловым дескриптором, и к нему без изменений применимы правила из главы Ресурсы и линейность.

Основные операции

impl Dev {
    // Поиск выдачи: неизвестное имя — None, а не ошибка.
    fn open(self: &Dev, name: &[u8]) -> Option[Device] !{io}
    // Дверь через точку монтирования: Result, потому что отсутствие
    // монтирования и отказ в выпуске — разные сбои с разными исправлениями.
    fn mint(self: &Dev, name: &[u8]) -> Result[Device, (DevErr, OsErr)] !{io}
}

impl Device {                                  // линейный: владеет fd
    fn ioctl_read(self: &mut Device, code: u32, out: &mut [u8])
        -> Result[usize, (DevErr, OsErr)] !{io}
    fn map_ro(self: &mut Device) -> Result[RamWindowRo, (DevErr, OsErr)] !{io}
    fn close(self: Device) !{io}               // расходует
}

Как и любая операция, которая доходит до ОС, операция с устройством, способная завершиться неудачей, возвращает Result[T, (DevErr, OsErr)]: ветвиться следует по DevErr, а печатать — OsErr (после use std::os; метод os.name() даёт его каноническое имя).

  • open возвращает None для неизвестного имени, а также для выданного узла, которого нет на месте. С точки зрения программы это один и тот же факт: такого устройства у неё нет.

  • ioctl_read выполняет один ioctl на чтение. Список разрешённых кодов принадлежит выдаче, а не программе: код не из списка даёт Err((DevErr::Denied, _)), и проверка происходит до обращения к устройству. Среда выполнения проверяет и то, что объявляет сам код. Если объявленный размер больше out или код предназначен только для записи, запрос отклоняется с Denied ещё до системного вызова: код выбирает список выдачи, а буфер — программа.

  • map_ro создаёт одно отображение выданной длины только для чтения и держит его, пока жив дескриптор. Повторный вызов даёт AlreadyMapped.

Варианты DevErr разделены по тому, что вызывающему делать дальше. Unavailable значит, что то, что стоит за узлом, не работает (ENODEV, ENXIO); по нему шлюз решает, обслуживать ли запросы вообще. IoFailed — временный сбой: ваше состояние в силе, повторите. WouldBlock — пока ничего нет: состояние в силе, опрашивайте дальше. Stale — ваше состояние недействительно, и повтор не поможет никогда: отбросьте позицию и установите связь заново. Как числа ESTALE и EIO похожи, но если спутать одно с другим, повтор превращается в ложное подтверждение того, что данные надёжно записаны. Остальные варианты (Denied, AlreadyMapped, Busy, Interrupted, ReadOnly, Invalid, NoSpace) значат то, что написано в их названиях.

mint — второй способ получить Device: не из узла, а из выданной точки монтирования. Оператор задаёт --dev-mint vol0=/mnt/data:mint=0x80384b01:map=4096 — путь монтирования и один код ioctl, превращающий дескриптор пути в дескриптор устройства, — а sys.dev.mint(b"vol0") выполняет open, ioctl и close внутри среды выполнения. Промежуточный дескриптор пути никогда не становится значением kola, так что программа не может удержать его и тем самым помешать размонтированию. У выпущенного Device те же операции. Глагол выпуска привязан к выдаче и на дескрипторе недоступен: ioctl, возвращающий произвольный дескриптор, позволил бы протащить полномочия мимо аудита, поэтому компилятор его отклоняет.

fn launder(d: &mut Device) !{io} {
    let x = d.mint(0x1234u32);
}
$ kola check launder.kl
error[card §7]: `mint` is bound to the GRANT, never free on a `Device` handle
  --> launder.kl:2:13

Строка подсказки после сообщения предлагает исправление — выдачу --dev-mint. Имя относится либо к одному виду выдачи, либо к другому: open не видит точек монтирования, а mint — узлов.

Не только чтение

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

  • ioctl на запись: ioctl_write, ioctl_exchange, ioctl_control, ioctl_payload и ioctl_file. Они выдаются по коду через write=CODE или через описатели payload= / file=, если структура ioctl содержит указатель или дескриптор. Эти поля среда выполнения заполняет сама, так что программа никогда не держит в руках адрес. Пишущий Device нельзя передать дочернему процессу.

  • Потоки записей: read_stream и wait_readable, выдаются через stream=RECORD_BYTES.

  • Прямой доступ к накопителям: nvme_admin (nvme=OPCODE) и scsi_in (scsi=OPCODE), а также «сырые» пишущие варианты под отдельными выдачами scsi_raw=, ata_raw= и nvme_raw=. open_class открывает диск, найденный самой программой, внутри класса, который оператор выдал через --device-class.

  • Сетевые устройства: --dev-tap создаёт интерфейс TAP, а --dev-tun — интерфейс TUN с операциями над пакетами (try_packet_read, try_packet_write). Оба работают только в Linux.

Каждое из них с точным синтаксисом выдачи и ошибками описано в STD-CARD, в разделе «Devices». Одна ловушка переносимости касается их всех: код ioctl — это число конкретной ОС. _IOR('K', 2, [u8; 64]) в Linux равен 0x80404b02, а в macOS — 0x40404b02, так что выдача, написанная для одной системы, на другой называет совсем другой запрос.

map_ro возвращает обычное окно только для чтения

Устройство часто публикует своё состояние в общей странице, которую драйвер может переписывать прямо во время чтения. Обычный протокол для этого — seqlock: перед записью писатель переводит счётчик последовательности в нечётное значение, после записи — в чётное, а читатель копирует данные и проверяет, что счётчик был чётным и не изменился; если нет, чтение повторяется. Устройству со страницей состояния поэтому нужен читатель seqlock, и напрашивается отдельный тип окна для устройств со своим читателем. В kola такого нет. У RamWindow есть двойник только для чтения, RamWindowRo, который получается из любого RAM-окна ослаблением, то есть выводом более слабой капабилити из той, что у вас уже есть (w.ro(), без всякой выдачи), и map_ro возвращает именно этот тип. Поэтому читатель seqlock над страницей состояния устройства — тот же snapshot, что работает над кольцом дескрипторов сетевой карты (общей очередью, через которую карта и драйвер обмениваются адресами буферов).

RamWindowRo — это RamWindow без пишущей половины. У него есть операции read*, copy_out, .len и snapshot, а write*, copy_in, zero и операций DMA нет вовсе. Читатель устройства, который попытается писать, не пройдёт чекер:

fn poke(w: &RamWindowRo) !{io}
    req w.len >= 8usize
{
    w.write32(0usize, 1u32);
}
$ kola check poke.kl
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
  --> poke.kl:4:5

Выдачи и модели

Узел выдаётся так же, как корень файловой системы: оператор связывает имя с путём, программа просит имя, а путь в программе не появляется вовсе.

kola run gw.kl \
    --device widget=/dev/widget:map=32:ioctl=0x80384b01 \
    --sim-dev widget=gw

# та же выдача через переменные окружения — для unit-файла или контейнера
KOLA_DEVICE_widget=/dev/widget:map=32:ioctl=0x80384b01
KOLA_SIM_DEV_widget=gw

map=LEN — длина отображения. ioctl=CODE можно повторять, и получившийся список — это и есть список разрешённых кодов. Вместе выдачи для поставляемого образа точно говорят, какие узлы устройств открывает программа и какие коды ioctl ей позволено слать.

Привязка --sim-dev определяет, с каким миром работает программа. Если модель привязана, устройством служит она — и под run, и под test. Без модели kola run и kola run --native открывают настоящее устройство: настоящий open, настоящий разрешённый ioctl, настоящий mmap. Под kola test выдача без модели отклоняется при запуске, потому что настоящий ioctl читал бы машину, на которой идёт тест:

$ kola test --interp t.kl --device widget=/dev/widget:map=32:ioctl=0x80384b01
error[card §7]: device `widget` is granted but has no model binding — a TEST backs a device node with a SimDevice model, because a real ioctl would read the host

Окну обычной памяти модель не нужна: обычная память сама себе модель. Устройству нужна, потому что смысл ioctl и mmap определяет само устройство. Модель — это набор чистых функций над структурой состояния, которую вы определяете сами, по одной на операцию, с именами от привязанного префикса:

  • p_new() -> M

  • p_attach(m: &mut M, now: u64) -> bool: открылся ли узел? false заставляет open вернуть None.

  • p_ioctl(m: &mut M, code: u32, out: &mut [u8], now: u64) -> Result[usize, DevErr]

  • p_map(m: &mut M, now: u64) -> Result[(), DevErr]: удалось ли отображение?

  • p_page(m: &mut M, off: usize, dst: &mut [u8], now: u64): через неё проходит каждое чтение отображённой страницы.

  • p_mint(m: &mut M, code: u32, now: u64) -> Result[(), DevErr] — только для выдачи через точку монтирования. Компилятор отклоняет такую выдачу, если в модели этой функции нет, и выдачу узла, если она есть.

Все они !{}. Пишущие, потоковые и TUN-выдачи добавляют свои обратные вызовы, они перечислены в STD-CARD.

Эти модели подчиняются трём правилам. now — параметр, а не Clock внутри модели: за детерминизм отвечает вызывающий. Модель называет исход вариантом DevErr и никогда не возвращает errno: модель — переносимый код на kola, а значения errno зависят от ОС (ESTALE в Linux равен 116, в macOS — 70); OsErr::Other добавляет исполнитель. И у каждой операции, способной не удаться, есть своя функция модели. Операция без функции модели в симуляции не может не удаться — именно поэтому существует p_map: без неё устройство, которое модель уже объявила исчезнувшим, всё ещё выдавало бы свежее отображение.

Шлюз от начала до конца

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

use std::log;

// ---- модель: чистые функции над вашей собственной структурой состояния
struct Gw { pulls: u64, probes: u64 }

fn gw_new() -> Gw !{} { Gw { pulls: 0, probes: 0 } }

// Открылся ли узел? `false` заставляет `sys.dev.open` вернуть `None`.
fn gw_attach(m: &mut Gw, now: u64) -> bool !{} { true }

// Проверка живости: при первом вызове устройство живо, потом пропадает.
fn gw_ioctl(m: &mut Gw, code: u32, out: &mut [u8], now: u64) -> Result[usize, DevErr] !{} {
    m.probes = m.probes + 1;
    if m.probes > 1 { return Err(DevErr::Unavailable); }
    for i in 0..out.len { out[i] = 1u8; }
    Ok(out.len)
}

// Удалось ли отображение?
fn gw_map(m: &mut Gw, now: u64) -> Result[(), DevErr] !{} {
    if m.probes > 1 { Err(DevErr::Unavailable) } else { Ok(()) }
}

// Страница — 8-байтовые слова little-endian: 0 seq, 8 magic | mounted << 32, 16 fenced.
// Слово последовательности нечётно при первом чтении (идёт публикация), потом чётно.
fn gw_word(pulls: u64, base: usize) -> u64 !{} {
    if base == 0 {
        if pulls == 1 { 1 } else { 2 }
    } else if base == 8 {
        0x4b4f5246u64 | (1u64 << 32)
    } else {
        0
    }
}

fn gw_page(m: &mut Gw, off: usize, dst: &mut [u8], now: u64) !{} {
    m.pulls = m.pulls + 1;
    for i in 0..dst.len {
        let a = off + i;
        let w = gw_word(m.pulls, a - a % 8);
        dst[i] = wrap[u8](w >> widen[u64]((a % 8) * 8));
    }
}

// ---- шлюз
fn read_status(ro: &RamWindowRo, dst: &mut [u8]) -> bool !{io}
    req ro.len >= 32usize
    req dst.len == 12usize
{
    ro.snapshot(0usize, 8usize, dst)
}

fn le32(b: &[u8], i: usize) -> u32 !{}
    req i + 4 <= b.len
{
    widen[u32](b[i]) | (widen[u32](b[i + 1]) << 8) | (widen[u32](b[i + 2]) << 16) | (widen[u32](b[i + 3]) << 24)
}

fn main(sys: Sys) -> u8 !{io, log} {
    let mut dev = match sys.dev.open(b"widget") {
        None => { log::info("no widget node: serving nothing"); return 1; }
        Some(d) => d,
    };
    let mut junk = [0u8; 8];
    match dev.ioctl_read(0xdeadu32, &mut junk) {
        Err((DevErr::Denied, _)) => log::info("undeclared code: Denied"),
        _ => log::error("an undeclared code reached the device"),
    }
    let mut probe = [0u8; 8];
    match dev.ioctl_read(0x80384b01u32, &mut probe) {
        Ok(n) => log::info(f"attach probe n={n}"),
        Err(_) => { log::info("mount is gone"); dev.close(); return 2; }
    }
    match dev.map_ro() {
        Err(_) => { log::info("map_ro failed"); dev.close(); 3 }
        Ok(ro) => {
            let mut hdr = [0u8; 12];
            let ok = read_status(&ro, &mut hdr);
            let magic = le32(&hdr, 0);
            let mounted = le32(&hdr, 4);
            let fenced = le32(&hdr, 8);
            log::info(f"ok={ok} magic={magic} mounted={mounted} fenced={fenced}");
            dev.close();
            0
        }
    }
}
$ kola run gw.kl --device widget=/dev/widget:map=32:ioctl=0x80384b01 --sim-dev widget=gw
[info] undeclared code: Denied
[info] attach probe n=8
[info] ok=true magic=1263489606 mounted=1 fenced=0

$ kola run --native gw.kl --device widget=/dev/widget:map=32:ioctl=0x80384b01 --sim-dev widget=gw
[info] undeclared code: Denied
[info] attach probe n=8
[info] ok=true magic=1263489606 mounted=1 fenced=0

$ kola run gw.kl                       # no grant at all
[info] no widget node: serving nothing

Эти два запуска — настоящее сравнение. C-бэкенд компилирует функции модели в нативную программу и вызывает их напрямую, так что оба исполнителя проходят одну и ту же машину состояний. Важно понимать, что такое сравнение может показать и чего не может. Если ошибка есть с обеих сторон — скажем, оба исполнителя пропускают повтор, — вывод всё равно совпадёт. Эталонная программа в репозитории (golden/dev-widget.kl) ловит такое, публикуя в странице собственный счётчик чтений модели и сверяя его с фиксированным значением. Модель, считающая свои вызовы, — дешёвый способ научить дифференциальный тест видеть поведение, а не только значения. В общем случае симулированное устройство доказывает логику драйвера: порядок подключения, политику допуска, дисциплину повторов. Кодировку ioctl, настоящее отображение и настоящий порядок операций с памятью доказывает только запуск на реальном узле /dev.

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

Дверь через точку монтирования выглядит так же, только с шестой функцией модели:

use std::log;
use std::os;

struct Vol { minted: bool }

fn vol_new() -> Vol !{} { Vol { minted: false } }
fn vol_attach(m: &mut Vol, now: u64) -> bool !{} { true }

// Шестая функция, для выдачи через монтирование: выдала ли файловая система дескриптор?
fn vol_mint(m: &mut Vol, code: u32, now: u64) -> Result[(), DevErr] !{} {
    if code != 0x80384b01u32 { return Err(DevErr::Denied); }
    m.minted = true;
    Ok(())
}

fn vol_ioctl(m: &mut Vol, code: u32, out: &mut [u8], now: u64) -> Result[usize, DevErr] !{} {
    if !m.minted { return Err(DevErr::Unavailable); }
    for i in 0..out.len { out[i] = 7u8; }
    Ok(out.len)
}

fn vol_map(m: &mut Vol, now: u64) -> Result[(), DevErr] !{} {
    if m.minted { Ok(()) } else { Err(DevErr::Unavailable) }
}

fn vol_page(m: &mut Vol, off: usize, dst: &mut [u8], now: u64) !{} {
    for i in 0..dst.len { dst[i] = 0u8; }
}

fn main(sys: Sys) -> u8 !{io, log} {
    match sys.dev.mint(b"vol0") {
        Ok(d) => {
            let mut d = d;
            let mut out = [0u8; 4];
            match d.ioctl_read(0x80384b01u32, &mut out) {
                Ok(n) => log::info(f"minted handle answers {n} byte(s), first={out[0]}"),
                Err(_) => log::info("ioctl refused"),
            }
            d.close();
            0
        }
        Err((_, os)) => { log::error(f"mint refused: {os.name()}"); 1 }
    }
}
$ kola run mint.kl --dev-mint vol0=/mnt/data:mint=0x80384b01:map=4096:ioctl=0x80384b01 --sim-dev vol0=vol
[info] minted handle answers 4 byte(s), first=7

Ветка match не может связать имя как mut, поэтому в ветке Ok(d) оно перепривязывается: let mut d = d;.

Что видит прувер

Два req у read_status работают по-настоящему. Обе встроенные проверки границ у snapshot — для данных и для слова последовательности — снимаются благодаря им, так что функция не несёт ни одной проверки времени выполнения (см. Контракты, трапы и тесты):

$ kola report checks gw.kl
...
fn read_status
  proven   ro.snapshot(8usize, ..)  [proved #8 + dst.len <= ro.len from req+guards]
  proven   ro.snapshot(seq 0usize, ..)  [proved #0 + #4 <= ro.len from req+guards]
...

Проверенный IR — это внутреннее представление программы, которое анализирует прувер; выразить в нём пока можно не всё. Операций Dev в нём нет, как нет и Mmio::window с Mmio::ram. Поэтому функция, которая ищет выдачу, не анализируется, а функции драйвера, принимающие &RamWindowRo, — анализируются. У шлюза такая форма получается сама собой: подключиться один раз в main, а читать во вспомогательных функциях. Если нужно, чтобы функция проходила kola check --require-analyzed, держите последовательность подключения вне её.

Сторона манифеста

Пакет, открывающий узлы устройств, объявляет их имена, и это объявление проходит через [deps] так же, как выданные корни файловой системы:

[pack]
name = "devgw"
version = "0.1.0"

[caps]
allowed = ["Dev", "Sys", "log"]
devices = ["widget"]
$ kola audit .
audit: caps within budget — pack `devgw` (used=["Dev", "Sys"] ⊆ allowed=["Dev", "Sys", "log (effect)"])
audit: devices — declares ["widget"], opens ["widget"]
audit ok: 0 violation(s) — every budget checked in this run is within its declared limits

Если убрать строку devices, аудит назовёт и устройство, и ключ манифеста:

error[pack budget]: device name `widget` requested via `Dev::open`/`Dev::mint`/`Dev::open_class` but not declared in [caps] devices = [] — ...

Sys в allowed не покрывает Dev. allowed перечисляет то, что пакет может достать из корневого набора, поэтому пакет, открывающий узел через sys.dev, обязан указать Dev, а библиотеке, получающей уже открытый Device параметром, не нужно ничего — так же, как библиотеке, которой передали Conn. Подробности о манифесте — в главе Пакеты. Выдачи устройств существуют только в hosted-режиме: во freestanding-образе нет /dev, и freestanding-сборка отклоняет любую конструкцию, связанную с устройствами.

layout_assert: заявленная раскладка

Раскладку дескрипторов оборудования, заголовков сетевых протоколов и структур ABI определяет кто-то другой. Один проект ядра когда-то держал десять написанных вручную самопроверок раскладки, потому что kola не умел сказать, какого размера структура; когда убрали код на Rust, который их перепроверял, половина из них утверждала раскладку, которую ничто не проверяло. layout_assert нужен, чтобы такое утверждение проверялось при сборке.

// Дескриптор, который читает и оборудование: его раскладку выбираем не мы.
pub struct Desc {
    addr: u64,
    len: u32,
    flags: u16,
    next: u16,
}

layout_assert[Desc](16, 8);

pub fn desc_is_chained(d: &Desc) -> bool !{} {
    d.flags & 1u16 == 1u16
}

Раскладка структуры — это её размер, выравнивание (кратность адреса, с которого она должна начинаться) и смещение каждого поля, включая заполнение, которое вставляет компилятор C. layout_assert[T](SIZE, ALIGN); — элемент уровня модуля, а не оператор. Это важно: сборка выпускает только достижимые функции и отбрасывает элементы test, так что утверждение внутри тела функции тихо перестало бы проверяться, как только эту функцию перестали бы вызывать. Как элемент модуля оно выпускается один раз, безусловно, рядом с определениями, о которых говорит, — даже для структуры, которую не использует ни одна функция.

size_of в kola нет. Размер в языке никогда не вычисляется. Вы его заявляете, а C-бэкенд выпускает _Static_assert(sizeof(T) == SIZE) (утверждение времени компиляции из C11: если условие ложно, компилятор останавливается с ошибкой) и _Static_assert(_Alignof(T) == ALIGN), так что судьёй выступает собственный компилятор C целевой платформы, а не его модель внутри kola. Если размер нужен как значение — скажем, чтобы задать длину буфера, — эта возможность его не даёт.

Неверное утверждение проваливает сборку и называет тип и число:

$ kola build --native ring.kl        # with layout_assert[Desc](24, 8);
build/ring.c:808:1: error: static assertion failed: "kola layout_assert[Desc]: claimed sizeof == 24"
error[build]: cc failed: exit status: 1

Утверждение, которое не может выполниться ни в одной реализации C, отклоняется ещё раньше, в kola check:

$ kola check ring.kl                 # with layout_assert[Desc](12, 8);
error[card §9]: layout_assert[Desc](12, 8) can never hold: a C object's size is always a multiple of its alignment (the trailing padding that makes an array of it work)
  --> ring.kl:9:1
   = help: round the size up to 16, or check the alignment claim

Проверяет утверждение только C-бэкенд: kola build, kola run --native, kola test --native. Интерпретатор считает его проверенной пустой операцией, потому что раскладки C у него нет, а kola build --cross его игнорирует. Зелёный kola test в интерпретаторе ничего не говорит об утверждении раскладки.

У каждой структуры, которую выпускает C-бэкенд, уже есть внутренние проверки раскладки: они подтверждают, что компилятор C согласен с собственной моделью раскладки kola. layout_assert проверяет другое — что раскладка совпадает с числом, которое вы взяли из внешней спецификации. kola и cc могут прекрасно договориться о раскладке, которую оборудование не примет.

Что можно заявлять: объявленный вами обычный struct или enum, массив фиксированной длины, кортеж или скаляр. Ссылка, срез, Vec, капабилити, ресурс или конкретизация дженерика отклоняются. Размер и выравнивание должны быть целыми литералами или const модуля; настоящие таблицы раскладки обычно и так состоят из констант, а именованная константа лучше читается в месте утверждения.

Без ОС: kola build --freestanding

C-бэкенд по умолчанию работает в hosted-режиме и использует libc по прямому назначению: malloc и free обслуживают регионы, fprintf и exit реализуют трапы, memcpy и memset перемещают байты, clock_gettime стоит за Clock. На голом железе ничего этого нет.

freestanding-сборка подключает только заголовки, которые поставляет сам компилятор (<stdint.h>, <stddef.h>, <stdbool.h>), обслуживает регионы статической ареной, превращает каждый трап (нарушенный контракт, переполнение, выход за границы) в вызов k_panic, который предоставляет платформа, сама определяет memcpy и memset, а каждую зависящую от ОС опору превращает во внешний хук, на который есть ссылка, только если программа им пользуется. --freestanding даёт объектный файл, но никогда не исполняемый: образ для голого железа раскладывает ваш скрипт компоновщика, поэтому --link здесь отклоняется.

Читаем список неопределённых символов

Объектный файл перечисляет символы (именованные функции и переменные), которые он определяет, и те, которыми пользуется, но не определяет; каждый неопределённый символ компоновщик должен найти где-то ещё, собирая итоговый образ. nm -u печатает этот второй список. Соберём две маленькие функции в режиме freestanding и спросим у nm, что ещё нужно каждой:

// pure.kl: все обязательства сняты
pub fn checksum(xs: &[u8]) -> u64 !{} {
    let mut h = 0xcbf29ce484222325u64;
    for b in xs {
        h = (h ^ widen[u64](b)) *% 0x100000001b3u64;
    }
    h
}

// checked.kl: `+` при переполнении срабатывает трапом, и здесь его ничто не исключает
pub fn total_len(a: u32, b: u32) -> u32 !{} {
    a + b
}
$ kola build --freestanding pure.kl
build ok (freestanding): 1 native fn(s), 1 exported item(s) (1 fn, 0 const, 0 type) → build/pure.o
  checksum
$ nm -u build/pure.o
                                   (nothing)

$ kola build --freestanding checked.kl
build ok (freestanding): 1 native fn(s), 1 exported item(s) (1 fn, 0 const, 0 type) → build/checked.o
  total_len
$ nm -u build/checked.o
                 U k_panic

checksum обходит срез циклом for и умножает с переносом, так что в нём нечему сработать трапом, и объект не ссылается ни на что. total_len использует проверяемое сложение, а исключить переполнение из пустого контракта прувер не может. Эта единственная оставшаяся проверка и добавляет k_panic в список неопределённых. Список неопределённых символов — краткая сводка того, на чём программа ещё может упасть, поэтому проекту для голого железа стоит проверять его в сборке, а не на глаз. Проверяйте его как подмножество разрешённых хуков, а не как число.

Хуки и условия, при которых каждый появляется:

Символ

Нужен, когда

void k_panic(const char *msg)

после прувера остаётся путь к трапу

uint64_t k_now_ns(void)

программа читает clock.now или now_boot, либо модуль собран с -DKOLA_MAIN

int64_t k_now_wall_us(void)

программа читает now_wall

void k_io_write(const char *s)

модуль собран с -DKOLA_LOG_HOOK, и программа пишет в журнал

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

Журнал включается явно. Без -DKOLA_LOG_HOOK запись в журнал отбрасывается, и ссылки на k_io_write нет. С ним хук получает по одной отформатированной строке [level] message за раз. Интерполированные строки во freestanding работают, потому что в kola.h есть собственный форматировщик:

$ kola build --freestanding logbare.kl                       # log::info(f"tick {n}")
$ nm -u build/logbare.o
                 U k_panic
$ KOLA_CC="cc -DKOLA_LOG_HOOK" kola build --freestanding logbare.kl
$ nm -u build/logbare.o
                 U k_io_write
                 U k_panic

k_panic здесь берётся из кода форматирования, который может сработать трапом; простой log::info("tick") ничего не добавляет.

Если компилировать сгенерированный C самостоятельно, а не через kola build --freestanding, список неопределённых символов может меняться по причинам, не имеющим отношения к вашей программе: при -O0 остаётся живой неиспользуемая функция часов, а без -fno-stack-protector компилятор добавляет символы защиты стека. Проверка списка символов в сборке должна смотреть на объект, который выдал kola build --freestanding.

Совсем без компилятора C: --cross

Там, где компилятора C нет, kola build --cross --target <arch> использует собственный бэкенд kola и пишет объектный файл без cc и без компоновщика. Цели: x86_64, aarch64, riscv64, riscv32, mips64el, mips32el, armv7m, loongarch64 и wasm32; подойдёт и полный триплет вроде riscv64-linux-gnu.

$ kola build --cross --target mips32 --format elf -o ring-mips32.o ring.kl
build ok: 1 native fn(s), 1 skipped → ring-mips32.o (mips32el/elf, 716 bytes)
  skipped `desc_is_chained`: slot `d`: `&struct#0` is outside native-mips32

$ file ring-mips32.o
ring-mips32.o: ELF 32-bit LSB relocatable, MIPS, MIPS32 rel2 version 1 (SYSV), not stripped

Собственный бэкенд охватывает меньшую часть языка, чем C-бэкенд, и если не может выпустить функцию, прямо об этом говорит и называет причину. Обычный --target <triple> без --cross — совсем другое: он передаёт триплет тому же компилятору C.

Там, где компилятор C есть, производственной сборкой служит C-бэкенд. Собственный бэкенд закрывает места, где его нет, а на x86-64 и AArch64 он уже собирает исполняемые файлы для Linux, macOS и Windows: kola build --link сначала пробует его и, если программа ему не по силам, с пояснением переходит на cc. Подробнее о бэкендах — в главе Под капотом.

Арена: измеряем кучу, под которую нужен бюджет

Без ОС нет ни malloc, ни brk. Freestanding-программа получает одну арену с выделением сдвигом на образ: фиксированный блок памяти, отведённый при компоновке образа, из которого память выдаётся сдвигом указателя вперёд. Её размер задаёт -DKOLA_HEAP_BYTES (по умолчанию 16 МиБ), а регионы из главы Память: регионы и ссылки нарезают из неё свои блоки. -DKOLA_REGION_DEFAULT задаёт размер первого блока каждого региона (по умолчанию 1 МиБ), что важно на небольшой целевой платформе. Оба значения должны совпадать во всех единицах трансляции одного образа.

Читаем уровень заполнения

Программа на C компилируется по одной единице трансляции (файл .c вместе со всем, что он подключает), после чего единицы компонуются вместе. Среда выполнения экспортирует две функции, которые может вызвать единица трансляции хоста: k_heap_used_bytes() — учёт выделений из «голого» пула — и k_heap_total_bytes() — размер пула после компоновки. Возьмём модуль с одним постоянным выделением и одной функцией на запрос:

// pool.kl
// Постоянное состояние: `heap` никогда не закрывается, так что взятое им у арены не возвращается.
pub fn stash(n: u64) -> &heap mut Vec[u64] !{alloc(heap)} {
    let v: &heap mut Vec[u64] = alloc in heap mut Vec::new();
    for i in 0..n { v.push(i); }
    v
}

// Один запрос: всё временное живёт в регионе, который закрывается до
// возврата из функции, так что арена откатывается следом.
pub fn serve(n: u64) -> usize !{} {
    let mut used = 0usize;
    region q {
        let v: &q mut Vec[u64] = alloc in q mut Vec::new();
        for i in 0..n { v.push(i); }
        used = v.len;
    }
    used
}

В сгенерированном заголовке экспортируемые функции называются k_<module>__<fn> (см. Встраивание kola в C-программу):

/* host.c: обычная единица трансляции C рядом с модулем kola */
#define KOLA_FREESTANDING 1
#include "pool.kh"
#include <stdio.h>
#include <stdlib.h>

void k_panic(const char *m) { fprintf(stderr, "k_panic: %s\n", m); exit(7); }

int main(void) {
    printf("start:            used=%6zu of %zu\n",
           k_heap_used_bytes(), k_heap_total_bytes());
    (void)k_pool__stash(1000ull);                         /* постоянно, в heap    */
    printf("after stash:      used=%6zu\n", k_heap_used_bytes());
    for (int i = 0; i < 100; i++) k_pool__serve(500ull);  /* временно, регион q   */
    printf("after 100 serves: used=%6zu\n", k_heap_used_bytes());
    return 0;
}
$ kola build --freestanding pool.kl
$ cd build
$ cc -c -O2 -ffreestanding -DKOLA_HEAP_BYTES=262144u -DKOLA_REGION_DEFAULT=4096u pool.c -o pool_bare.o
$ cc -O2 -DKOLA_HEAP_BYTES=262144u -DKOLA_REGION_DEFAULT=4096u -I. ../host.c pool_bare.o -o host
$ ./host
start:            used=     0 of 262144
after stash:      used= 12480
after 100 serves: used= 12480

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

Возврат памяти при закрытии

Сто вызовов serve не стоят ни одного постоянного байта. Закрывающийся регион считает собственные выделения, и при закрытии арена откатывается тогда и только тогда, когда учёт продвинулся ровно на это число — это доказывает, что каждый байт выше отметки региона принадлежит ему.

Теперь по ошибке оставим состояние запроса в heap — одно слово в типе, — и тот же сервис погибнет:

/* leak.c: тот же сервис, но состояние запроса оставлено в heap */
int main(void) {
    for (int i = 0; ; i++) {
        if ((i % 20) == 0) {
            printf("request %4d: used=%7zu of %zu\n",
                   i, k_heap_used_bytes(), k_heap_total_bytes());
            fflush(stdout);
        }
        (void)k_pool__stash(100ull);
    }
}
$ ./leak
request    0: used=      0 of 262144
request   20: used=  28960 of 262144
request   40: used=  61824 of 262144
request   60: used= 127456 of 262144
...
request  120: used= 258624 of 262144
...
request  220: used= 258624 of 262144
k_panic: bare heap exhausted

Несколько следствий правила отката:

  • Размер арены определяется пиковым одновременным использованием, а не накопленным за всё время. Вложенные или последовательные регионы стоят столько, сколько живо в худший момент, плюс по одному блоку на каждое событие чересполосицы.

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

  • Регион с бюджетом (region r from m) при закрытии возвращает начисленные им кредиты Mem — на любом пути выхода. Байты арены и кредиты бюджета — отдельные учёты, отвечающие на разные вопросы.

Для сервиса, который должен пережить неограниченное число запросов, есть три приёма, по убыванию предпочтительности. Открывайте на каждый запрос region { }, закрываемый до возврата, а состояние, живущее всё время работы программы, держите в heap или во внешнем регионе. Пусть точки входа библиотеки принимают рабочий буфер от вызывающего — тогда прогретый Vec не выделяет ничего за вызов. Или, для резидентной машины состояний, которая умеет сохранять себя, закрывайте её долгоживущий регион и восстанавливайте её в новом. Последнее — решение политики, которое может принять только сама программа: среда выполнения не знает, какие состояния восстановимы.

Один пул на образ

Арена — один массив на скомпонованный образ, а не на единицу трансляции. Каждая единица трансляции, подключающая kola.h, выпускает его определение, помеченное как слабое (слабый символ компоновщик может отбросить в пользу другого определения с тем же именем), и это определение лежит в секции link-once (.gnu.linkonce.b.k_heap в ELF), так что компоновщик оставляет ровно одну копию и от вашей строки cc ничего не требуется. Исключение — написанный вручную скрипт компоновщика: правилу .bss, которое явно перечисляет входные секции, нужен *(.gnu.linkonce.b.*), иначе пул станет секцией-сиротой и окажется там, где решит компоновщик. Отбрасывает ли конкретный компоновщик проигравшие копии — вопрос к каждому компоновщику отдельно; это проверено на GNU ld и LLD, но не на gold и mold.

Скомпонованный образ можно проверить и без kola. В нём должен быть ровно один определённый k_heap, слабый; его st_size должен совпадать с задуманным размером пула; и значение k_heap_bytes после компоновки должно быть тем же числом. Проверка того, что все объекты собраны с одинаковым -DKOLA_HEAP_BYTES, полезна, но не видит, что оставил компоновщик.

Образ, который никогда не выделяет память, может так и заявить. -DKOLA_HEAP_BYTES=0 сам по себе отклоняется при компиляции, потому что определение нулевого размера может победить при компоновке и оставить без памяти модуль, который выделяет. В паре с -DKOLA_NO_HEAP он принимается и значит сразу две вещи: ничего не резервируется, и любое выделение срабатывает трапом с понятным именем:

$ cc -c -ffreestanding -DKOLA_NO_HEAP -DKOLA_HEAP_BYTES=0 ...
# at run time, on any allocation:
k_panic: bare allocation in an image built -DKOLA_NO_HEAP: this image declares that it never allocates from the bare pool, and something just did. Either the allocation is a defect, or the declaration is wrong — drop -DKOLA_NO_HEAP and pass the image's real pool size to EVERY TU.

Сообщение намеренно не «bare heap exhausted»: пул, который никогда не резервировался, не мог закончиться. -DKOLA_NO_HEAP с ненулевым размером — противоречие, и оно отклоняется при компиляции; так ловится сборочный скрипт, в котором завёлся настоящий пул, а старый флаг остался в командной строке.