Машина: Cpu, упорядочивание памяти и атомарные операции

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

Как программа добирается до регистров устройств и общей памяти без указателей, включая seqlock и обслуживание кэша при DMA, рассказано в главе об аппаратных окнах. Узлы устройств и сборки без операционной системы описаны в главе Bare metal. Здесь окна считаются уже знакомыми.

Эффект hw

Эффекты описывают, какого рода действия совершает функция. hw отмечает привилегированную или чувствительную к порядку машинную операцию. Привилегированная — значит, процессор разрешает такую инструкцию только в режиме ядра; пример — выключение прерываний. Чувствительная к порядку — значит, весь смысл операции в том, когда её результат станет виден другим ядрам или устройствам; пример — барьер памяти.

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

fn mask(cpu: &Cpu) !{io} {
    cpu.irq_disable();
}

error[card §6]: `mask` performs `hw` (cpu irq_disable) but does not declare it
  --> row.kl:2:5
   = help: add `hw` to the effect clause, or hand the work to a caller that has it

Атомарная операция внутри ct fn отвергается так же, как любой другой вызов функции, не помеченной ct:

error[card §6b]: [ct fn `leaky`] ct fn calls non-ct fn `load32_relaxed` — a `ct` fn may only call other `ct` fns or the `widen`/`narrow`/`wrap` builtins

Капабилити Cpu

Окно выдаётся по имени: на вопрос «какое устройство?» бывает много ответов, и выбрать может только оператор, который запускает программу. На вопрос «можно ли этому коду выполнять привилегированные инструкции процессора?» ответ один, поэтому Cpu — единственный маркер полномочия в корневом наборе, как Clock или Rng. Ни флага, ни поиска, ни Option: sys.cpu есть всегда, а тест получает sim.cpu из своего набора Sim.

Каждая операция Cpu принимает разделяемую ссылку &Cpu. Симулированный процессор хранит настоящее состояние (флаг прерываний, файлы регистров) и меняет его через эту ссылку. Благодаря этому функции с параметром &Cpu остаются в верифицируемом подмножестве, и обязательства по границам и req вокруг них по-прежнему доказываются.

В интерпретаторе и в нативных сборках под операционной системой (обычные программы: kola run --native, kola test --native) операции выполняются на одном и том же симулированном процессоре, поэтому оба исполнителя дают одинаковый результат. Процессу под ОС некуда загружать таблицу прерываний, и оба исполнителя предлагают её модель. Поэтому cpuid отвечает то, что говорит модель, а не ваш компьютер. Сборка без операционной системы (kola build --freestanding, код, который работает прямо на железе) превращает каждую операцию в настоящую инструкцию целевой архитектуры.

Прерывания

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

Операций четыре: irq_disable(), irq_enable(), irq_save() -> u64 и irq_restore(flags: u64). irq_save выключает прерывания и возвращает состояние, которое было до этого (1 — были включены). Ради этого она и существует рядом с irq_disable. Критическая секция, которая заканчивается вызовом irq_enable(), ошибочна, если у вызывающего прерывания уже были выключены: она включит их за его спиной. Пара save и restore возвращает ровно то, что было, поэтому критические секции можно вкладывать друг в друга.

use std::log;

// Выключить прерывания, сделать работу, вернуть ровно то состояние, что было.
fn critical(cpu: &Cpu) !{hw, log} {
    let prior = cpu.irq_save();
    log::info(f"critical section entered, prior={prior}");
    cpu.irq_restore(prior);
}

fn main(mut sys: Sys) -> u8 !{hw, log} {
    critical(&sys.cpu);        // после сброса прерывания выключены: prior = 0
    sys.cpu.irq_enable();
    critical(&sys.cpu);        // теперь prior = 1, и restore оставляет их включёнными
    let after = sys.cpu.irq_save();
    log::info(f"after both sections, interrupts were on={after}");
    0
}

$ kola run --log stderr crit.kl
[info] critical section entered, prior=0
[info] critical section entered, prior=1
[info] after both sections, interrupts were on=1

Первое prior=0 — собственное состояние симулированного процессора: как и настоящий после сброса, он стартует с выключенными прерываниями.

Остановка, ожидание и активное ожидание

Процессору, которому нечего делать, лучше остановиться и подождать события, чем жечь энергию. Для этого в kola есть три операции: hlt(), wfi() (ждать прерывания) и wfe() (ждать события). Четвёртая, spin_hint(), — для обратного случая: она сообщает процессору, что код крутится в цикле, ожидая другое ядро. В интерпретаторе все четыре ничего не делают, потому что симулятор не моделирует приход прерываний. В сборке без ОС они превращаются в такие инструкции:

В x86 нет инструкции ожидания события. Очевидная замена, pause, процессор не останавливает, так что цикл простоя ядра loop { cpu.wfe(); } крутился бы на x86 на полной мощности, а на других архитектурах спал бы. Чтобы одна операция не означала разное в зависимости от цели, kola отвергает wfe на x86. Генератор кода выдаёт каждую операцию Cpu как выражение, а туда _Static_assert языка C не поставить, поэтому отказ оформлен как необъявленный идентификатор, имя которого и есть диагностика:

pub fn park(cpu: &Cpu) !{hw} { cpu.wfe(); }

fn main(mut sys: Sys) -> u8 !{hw} { park(&sys.cpu); 0 }

$ kola build --freestanding wait.kl -o out        # on an x86-64 host
out/kola.h:9800:5: error: ‘k_cpu_wfe_UNAVAILABLE_ON_x86_64__use_wfi_to_park_or_spin_hint_to_spin’ undeclared (first use in this function)
error[build]: cc failed: exit status: 1

Идентификатор называет оба исправления: wfi, чтобы остановиться, и spin_hint, чтобы крутиться. Тот же C-код собирается для aarch64 и mips, где настоящее ожидание события есть.

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

// Ограниченный захват через compare-and-swap: так устроен любой SMP-спинлок.
pub fn try_acquire(cpu: &Cpu, cells: &[u32], i: usize, budget: u32) -> bool !{hw}
    req i < cells.len
{
    let mut tries = 0u32;
    while tries < budget {
        if Atomic::cas32_acquire(cells, i, 0u32, 1u32) == 0u32 {
            return true;
        }
        cpu.spin_hint();
        tries = tries + 1;
    }
    false
}

pub fn release(cells: &[u32], i: usize) !{hw}
    req i < cells.len
{
    Atomic::store32_release(cells, i, 0u32);
}

test the_lock_is_taken_then_released(mut sim: Sim) {
    let cells: [u32; 1] = [0u32];
    assert try_acquire(&sim.cpu, &cells, 0, 64);
    // блокировка занята: второй претендент исчерпывает бюджет и сдаётся
    assert !try_acquire(&sim.cpu, &cells, 0, 8);
    release(&cells, 0);
    assert try_acquire(&sim.cpu, &cells, 0, 64);
}

$ kola test spin.kl
spin.kl: test the_lock_is_taken_then_released ... ok
1 passed, 0 failed (interpreted, JIT backend)
native tests: 1 ran, 0 fail(s)

$ kola report checks spin.kl
  proven   Atomic::cas32_acquire(cells, i)  [proved i < cells.len from req+guards]
  proven   tries + 1u32  [sum bounded by width]
  proven   Atomic::store32_release(cells, i)  [proved i < cells.len from req+guards]

В сборке без ОС подсказка превращается в pause на x86-64 и в yield на aarch64. На mips это вообще ничего: подсказки для активного ожидания там нет, а если выдать вместо неё wait, остановится ядро, которое должно следить за блокировкой.

Привилегированные регистры

Свою конфигурацию процессор хранит в особых регистрах, недоступных обычному коду: включена ли страничная адресация, где лежит таблица прерываний, какие возможности включены. В каждой архитектуре они устроены по-своему, и kola сохраняет эту форму:

• aarch64: sysreg_read(enc) -> u64 и sysreg_write(enc, v). enc — кодировка системного регистра, и она обязана быть константой времени компиляции, потому что инструкция (mrs/msr) несёт номер регистра внутри своего машинного слова.

• MSR на x86 (model-specific registers, модельно-специфичные регистры): rdmsr(id) -> u64 и wrmsr(id, v). Здесь id может вычисляться во время выполнения, потому что rdmsr берёт номер из регистра.

• Управляющие регистры x86: cr_read(n) -> u64 и cr_write(n, v). n — константа, одно из чисел 0, 2, 3, 4 или 8. Зарезервированный номер вызывает трап, а не читается как 0: управляющий регистр, который молча читается нулём, выглядит для загрузочного кода как «страничная адресация выключена».

• CP0 на mips: cp0_read(reg, sel) -> u64 и cp0_write(reg, sel, v), где reg и sel — константы.

Требование константы происходит из генерации кода, поэтому kola check принимает селектор, вычисляемый во время выполнения, а сборка без ОС его отвергает:

pub fn read_dynamic(cpu: &Cpu, enc: u64) -> u64 !{hw} {
    cpu.sysreg_read(enc)
}

$ kola build --freestanding sysreg.kl -o out
codegen: native codegen: `sysreg_read(...)` in `read_dynamic`: the register selector must be a compile-time constant (it is baked into the instruction encoding) — pass a literal or a `const`, not a runtime value (design-kernel-lowlevel.md §2.1b)

Кроме того, в x86 есть таблицы дескрипторов — таблицы в памяти, описывающие сегменты и обработчики прерываний. Их загружают lgdt(base, limit), lidt(base, limit) и ltr(sel); sgdt() и sidt() возвращают (base, limit), а str() — регистр задачи. Чтение возвращает кортеж, потому что каждое из них — одна инструкция, заполняющая несколько регистров, и две отдельные операции выполнили бы её дважды. cpuid(leaf, sub) возвращает четыре регистра с результатом. lgdt_win(w), lidt_win(w) и cr3_write_win(w) принимают вместо голого адреса RamWindow: среда выполнения сама берёт базу из окна, так что адрес в исходном коде kola вообще не появляется, а предел вычисляется как len - 1.

В симуляторе все эти регистры хранятся в одном файле регистров с доступом по ключу. Регистр, в который никто не писал, читается как 0:

// Один файл регистров по ключу обслуживает все три семейства; незаписанный читается как 0.
test the_register_files_round_trip(mut sim: Sim) {
    // aarch64: у SCTLR_EL1 (S3_0_C1_C0_0) кодировка 0xc080, это константа
    assert sim.cpu.sysreg_read(0xc080) == 0;
    sim.cpu.sysreg_write(0xc080, 0x1234);
    assert sim.cpu.sysreg_read(0xc080) == 0x1234;

    // x86: IA32_EFER — это MSR 0xC0000080; номер может вычисляться во время выполнения
    sim.cpu.wrmsr(0xC0000080, 0x500);
    assert sim.cpu.rdmsr(0xC0000080) == 0x500;

    // управляющие регистры x86: номер — константа, одно из 0/2/3/4/8
    sim.cpu.cr_write(4, 0x20);
    assert sim.cpu.cr_read(4) == 0x20;

    // mips: CP0 адресуется парой (reg, sel); другой sel — независимый регистр
    sim.cpu.cp0_write(10, 0, 0xABCD);
    assert sim.cpu.cp0_read(10, 0) == 0xABCD;
    assert sim.cpu.cp0_read(10, 1) == 0;
}

test descriptor_tables_and_cpuid(mut sim: Sim) {
    sim.cpu.lgdt(0x8000, 0x37);
    let (base, limit) = sim.cpu.sgdt();
    assert base == 0x8000;
    assert limit == 0x37;
    let (a, b, c, d) = sim.cpu.cpuid(0x4000_0000, 0);
    assert a == 0 && b == 0 && c == 0 && d == 0;   // незапрошенный лист отвечает одними нулями
}

На чужой архитектуре сборка без ОС отвергает операцию с регистром по имени и никогда не превращает её в молчаливое «ничего».

Виртуализация

Гипервизор запускает целые операционные системы как гостевые. На процессорах Intel аппаратная поддержка называется VMX: гипервизор входит в особый режим (vmxon) и описывает каждый виртуальный процессор в структуре в памяти, которая называется VMCS (virtual machine control structure). В ней лежат регистры гостя, причины, по которым он может выйти обратно в гипервизор, и так далее. У AMD аналог называется SVM, а структура — VMCB.

К полям VMCS kola обращается через одну пару операций, vmread(enc) -> u64 и vmwrite(enc, v), а не через полторы сотни именованных. Кодировки полей — константы в std::machine::vmcs (GUEST_RIP, VM_EXIT_REASON, HOST_RIP, ...). Если кодировка — константа, её корректность проверяется при компиляции:

pub fn bad(cpu: &Cpu) -> u64 !{hw} {
    cpu.vmread(0x7000)
}

error[card §7]: `vmread`: 0x7000 is not a valid Intel VMCS field encoding — a well-formed encoding sets no bit outside 0x6FFF (bit 12 and bits 15-31 are reserved MBZ)
   = help: use a field from the std::machine::vmcs table (GUEST_RIP, VM_EXIT_REASON, …), or a real Intel SDM Vol 3 App-B encoding — this constant could only ever fault the instruction

Кодировка, вычисленная во время выполнения (скажем, в цикле, который сохраняет список полей), проверяется во время выполнения.

Вокруг этой пары — остальной жизненный цикл: для VMX это vmxon, vmxoff, vmclear, vmptrld, vmptrst, invept и invvpid, для SVM — vmsave, vmload, stgi, clgi, vmmcall и invlpga. Все они есть только на x86, требуют !{hw} и принимают &Cpu. Набор инструкций замкнут, поэтому kola даёт всё семейство целиком, а не то подмножество, которое понадобилось одной программе. invept и invvpid сбрасывают закэшированные трансляции адресов гостя. EPT — это второй уровень таблиц страниц гостя, VPID — метка его записей в TLB, процессорном кэше трансляций адресов.

use std::machine::vmcs;

// Запуск Intel VMX на одном процессоре: войти в корневой режим VMX, загрузить VMCS,
// задать стартовый адрес гостя, сбросить записи EPT и VPID, выйти.
fn vmx_bringup(cpu: &Cpu, vmxon_pa: u64, vmcs_pa: u64, eptp: u64) !{hw} {
    cpu.vmxon(vmxon_pa);
    cpu.vmclear(vmcs_pa);
    cpu.vmptrld(vmcs_pa);
    cpu.vmwrite(vmcs::GUEST_RIP, 0xffff_0000);
    cpu.invept(1, eptp);           // тип 1: сброс EPT для одного контекста
    cpu.invvpid(2, 1, 0);          // тип 2: сброс VPID для одного контекста
    cpu.vmxoff();
}

test the_lifecycle_leaves_the_vmcs_fields_alone(mut sim: Sim) {
    vmx_bringup(&sim.cpu, 0x1000, 0x2000, 0x3000);
    assert sim.cpu.vmread(vmcs::GUEST_RIP) == 0xffff_0000;
    assert sim.cpu.invept_single(0x3000);
    assert sim.cpu.invept_count() == 1;
}

В симуляторе операции жизненного цикла либо ничего не делают, либо меняют пару флагов (корневой режим VMX, указатель на текущую VMCS, глобальный флаг прерываний). Интересное состояние здесь — файл полей VMCS, и тест проверяет, что жизненный цикл его не трогает. invept_single(eptp) -> bool — удобная обёртка рядом с голым invept: сброс для одного контекста, при этом бит отказа инструкции возвращается как значение. invept_count() считает сбросы, чтобы тест мог утверждать «N изменений таблиц страниц дали N сбросов». Она работает в обоих симулирующих исполнителях и отвергается в сборке без ОС, где нулевой счётчик позволил бы такому утверждению пройти, ничего не доказав.

Инструкций, которые действительно входят в гостя (vmrun, vmlaunch, vmresume), в kola нет. Вход в гостя требует, чтобы вокруг инструкции гипервизор сам сохранял и восстанавливал регистры, а этого никакая обобщённая операция дать не может. Поэтому этот шаг живёт в коде вне kola. Всё, что подготавливает и сворачивает виртуализацию, написано на kola.

Кэши, TLB и барьеры

Недавно использованную память процессор держит в кэшах, а недавние трансляции адресов — в TLB (translation lookaside buffer, буфер ассоциативной трансляции). Обычно это незаметно. Заметно становится, когда память читает кто-то кроме процессора (DMA-контроллер), когда меняются таблицы страниц или когда процессор записывает инструкции, которые потом будет выполнять. Для этих случаев у Cpu есть операции обслуживания: tlb_flush_all(), tlb_flush_page(va), dcache_clean(va), dcache_flush(va), icache_invalidate(va).

Барьер памяти (fence) — инструкция, которая не даёт процессору переставлять операции с памятью через неё. Современные процессоры ради скорости меняют порядок чтений и записей, и барьер — способ сказать: «всё, что было до него, должно стать видимым раньше всего, что после». fence() упорядочивает память между ядрами, fence_sys() — общесистемный барьер, который охватывает и устройства. В симуляторе все эти операции ничего не делают; это операции сборки без ОС.

Явных барьеров нужно меньше, чем можно подумать. Обращения через MmioWindow уже упорядочены так, как их видит устройство, поэтому между «записать дескриптор в RamWindow» и «записать регистр-звонок» барьер не нужен. Операции с кэшем для DMA над диапазоном памяти, dma_writeback и dma_invalidate, принадлежат RamWindow, потому что относятся к диапазону, а не к процессору; см. главу об аппаратных окнах.

Атомарные операции

Когда два ядра делят память, обычное «прочитать, изменить, записать» вроде x = x + 1 небезопасно: оба ядра могут прочитать одно и то же старое значение, и одно приращение потеряется. Атомарная операция выполняет всё «прочитать, изменить, записать» одним неделимым шагом, который другое ядро прервать не может. Из атомарных операций строятся блокировки, счётчики и неблокирующие очереди.

В kola 18 атомарных операций, все с эффектом !{hw}, и записываются они как Atomic::<op>(cells, i, ...). Первый аргумент — разделяемый срез (&[u32] или &[u64]), второй — индекс в нём. Ссылки на отдельную ячейку не бывает:

• Срез разделяемый, а не &mut, потому что атомарная операция — это как раз та запись, которую безопасно делать через разделяемую ссылку. Этим она и отличается от обычной записи.

• Читать через ссылку на одно целое число kola не умеет, поэтому ячейка задаётся срезом и индексом. Полезное следствие: невыровненную атомарную операцию просто невозможно написать, ведь индекс в срезе u32 всегда попадает на границу 4 байт.

И разрядность, и упорядочивание входят в имя операции. Упорядочивание говорит, какие другие операции с памятью гарантированно видны вокруг атомарной. Relaxed гарантирует только атомарность самой операции. Acquire (у чтения) означает, что ничто после операции нельзя перенести раньше неё; это нужно при захвате блокировки. Release (у записи) означает, что ничто до операции нельзя перенести после неё; это нужно при освобождении блокировки, чтобы другое ядро увидело ваши записи раньше, чем увидит блокировку свободной.

• чтение: load32_relaxed, load32_acquire, load64_relaxed, load64_acquire

• запись: store32_relaxed, store32_release, store64_relaxed, store64_release

• «прочитать, изменить, записать», каждая возвращает прежнее значение: add32_relaxed, add64_relaxed, or32_relaxed, or64_relaxed, and32_relaxed, and64_relaxed, swap32_relaxed, swap64_relaxed

• сравнение с обменом: cas32_acquire, cas64_acquire, аргументы (cells, i, expected, new)

Сравнение с обменом (compare-and-swap, CAS) записывает new, только если в ячейке сейчас лежит expected. CAS в kola возвращает увиденное значение, а не bool. Если оно равно expected, вы выиграли. Если нет, текущее значение уже у вас в руках, и второе чтение не нужно: к моменту выполнения оно могло бы устареть.

pub fn bump(cells: &[u64], i: usize) -> u64 !{hw}
    req i < cells.len
{
    Atomic::add64_relaxed(cells, i, 1u64)   // возвращает прежнее значение
}

pub fn try_latch(cells: &[u32], i: usize) -> bool !{hw}
    req i < cells.len
{
    Atomic::cas32_acquire(cells, i, 0u32, 1u32) == 0u32
}

test the_latch_wins_exactly_once {
    let cells: [u32; 1] = [0u32];
    assert try_latch(&cells, 0);
    assert !try_latch(&cells, 0);
}

test cas_reports_what_was_really_there {
    let cells: [u32; 1] = [0u32];
    let won = Atomic::cas32_acquire(&cells, 0, 0u32, 7u32);
    assert won == 0u32;
    let lost = Atomic::cas32_acquire(&cells, 0, 0u32, 9u32);
    assert lost == 7u32;               // то, что лежало в ячейке, а не наша догадка
    assert Atomic::load32_relaxed(&cells, 0) == 7u32;
}

test add_returns_the_previous_value {
    let cells: [u64; 1] = [0u64];
    assert bump(&cells, 0) == 0u64;
    assert bump(&cells, 0) == 1u64;
    assert Atomic::load64_relaxed(&cells, 0) == 2u64;
}

$ kola test lock.kl
lock.kl: test the_latch_wins_exactly_once ... ok
lock.kl: test cas_reports_what_was_really_there ... ok
lock.kl: test add_returns_the_previous_value ... ok
3 passed, 0 failed (interpreted, JIT backend)
native tests: 3 ran, 0 fail(s)

Набор намеренно мал. Последовательно согласованного упорядочивания (самого строгого и самого медленного) нет, как нет и «слабого» CAS, который может ложно не сработать: такой повтор операция делает сама.

Атомарные операции над окном

Аргументом cells может быть и RamWindow или его ослабленная версия только для атомарных операций, AtomicWindow (w.atomic()). Так те же операции достают до памяти, общей с другим ядром или устройством. И для окна индекс остаётся номером ячейки, а не смещением в байтах, чтобы Atomic::add32(x, i, v) означало одно и то же, что бы ни было x. Для 32-битных ячеек граница — w.len / 4.

test atomics_over_a_window(mut sim: Sim) {
    match sim.mmio.ram(b"roster") {
        Some(w) => {
            let a = w.atomic();
            let prev = Atomic::add32_relaxed(&a, 1, 5u32);   // ячейка 1 = байты 4..8
            assert prev == 0u32;
            assert w.read32(4) == 5u32;
        }
        None => { assert false; }
    }
}

Этому тесту нужна выдача окна: kola test aw.kl --ram-window roster=0x0:0x40.

Что выдаёт компилятор

Ассемблер для атомарных операций kola не пишет. Она выдаёт встроенные функции __atomic компилятора C: им не нужен заголовочный файл (значит, они работают и в сборке без ОС), и они сами выбирают подходящую инструкцию для каждой архитектуры. <stdatomic.h> из C11 не используется: в сборке без ОС его может не быть, а тип _Atomic мог бы изменить раскладку памяти, которую другое ядро читает как обычные байты.

На mips, например, 32-битный CAS компилируется в пару load-linked/store-conditional. ll загружает значение и начинает следить за адресом; sc записывает, только если никто другой за это время по этому адресу не писал, и сообщает, удалось ли:

	ll	$1, 0($4)
	...
	sc	$2, 0($4)
	...
	sync

На 32-битной цели, например 32-битном mips, одной инструкции для 64-битной атомарной операции нет. Компилятор вызвал бы вспомогательную библиотеку, а образ без ОС её прилинковать не может. Поэтому там 64-битные операции отвергаются при компиляции, и исправление записано в самом идентификаторе:

pub fn bump(cells: &[u64], i: usize) -> u64 !{hw}
    req i < cells.len
{
    Atomic::add64_relaxed(cells, i, 1u64)
}

$ kola build --freestanding w64.kl -o out
$ clang --target=mipsel-linux-gnu -ffreestanding -DKOLA_FREESTANDING -Iout -c out/w64.c
out/w64.c:799:12: error: use of undeclared identifier 'k_atomic64_UNAVAILABLE_ON_ILP32__use_the_32_bit_ops'
  799 |     return K_ATOMIC64(__atomic_fetch_add(((uint64_t*)((cells).ptr) + (/*IR:discharged*/(i))), ...

32-битные операции для этой цели по-прежнему компилируются. Та же строка с ошибкой показывает, что дало req i < cells.len: индекс попадает в C-код с пометкой /*IR:discharged*/ и без проверки границ, потому что граница доказана.

Чего не скажет симулятор

Интерпретатор выполняет потоки по одному, поэтому он — эталон для значений и ни для чего, что касается порядка или когерентности. Release-запись выполняется там как обычная запись, барьер ничего не делает, а compare-and-swap — это чтение и следом запись, между которыми ничто не может вмешаться. Каждое совпадение между kola run и kola run --native в этой главе говорит лишь о том, какие числа получились.

Пробел закрывают три вещи:

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

• Запускать на целевом железе, причём на нескольких ядрах, если важен порядок. Свидетельство правильности атомарных операций — многоядерный тест спинлока на настоящем чипе, а не пройденные тесты под ОС.

• Помнить, что сравнение двух исполнителей не находит общую для них ошибку. Если оба одинаково ошибаются в какой-то проверке, они согласятся друг с другом, и упадёт только утверждение об ожидаемом значении.

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