kernel demo

A small freestanding “kernel” – a UEFI application that badc compiles for x86_64 and AArch64 and that boots under QEMU through UEFI firmware (OVMF on x86_64, ArmVirtQemu/AAVMF on AArch64). It runs before any OS, talks only to the firmware console (which the firmware mirrors to the serial line), and is a live end-to-end test of badc’s inline assembly: a correct boot means the inline asm assembled to the right bytes and executed on real hardware paths.

What each target exercises:

Run

cargo build --release --features full      # build badc
python3 demos/kernel/smoke.py               # build + boot both targets
python3 demos/kernel/smoke.py --arch native # boot this host's arch only
python3 demos/kernel/smoke.py --self-test   # check the arch filter, no boot

The smoke compiles kernel.c for windows-x64 and windows-arm64 (PE32+ EFI applications) and, when QEMU and UEFI firmware are present, boots each and checks the serial output for the per-target markers and the final BADC-KERNEL-OK. If QEMU or the firmware is missing the boot is skipped, the demo is build-only for that target, and the closing summary says how many boots ran. Override the badc binary with $BADC.

The emulator is stopped as soon as the expected markers reach the serial line, so a boot costs what the firmware and the kernel take to print them. Neither kernel exits on its own – preempt.c ends in a halt loop and kernel.c returns to the firmware – so a boot spends the whole 60 s budget only when its markers do not appear.

--arch <x64|aarch64|native> narrows the run to one architecture’s boots; every kernel is still built for both, each build costing a fraction of a second. The local gate runs both architectures on each Linux lane and does not use the filter.

Booting inside badc-built QEMU

By default the smoke uses the system qemu-system-<arch>. To run the kernel inside the badc-built emulator from the qemu demo, point the per-arch override at its output:

QEMU_SYSTEM_X64=demos/qemu/qbuild-x86_64/qemu-system-x86_64 \
QEMU_SYSTEM_AARCH64=demos/qemu/qbuild-aarch64/qemu-system-aarch64 \
    python3 demos/kernel/smoke.py

so the whole stack – the kernel, and the emulator it runs in – is badc-built.

Preemptive multitasking (preempt.c)

preempt.c is a second, larger kernel: it installs its own timer interrupt, runs three hardcoded threads, and context-switches between them on every tick, with each thread printing to the serial port under a spin lock. It goes beyond the inline-asm smoke by taking over the interrupt vector table and the timer, so it is a live test of badc emitting a real interrupt service routine – a __attribute__((naked)) function whose body is the context switch.

Both targets are complete and the smoke boots them: the serial output shows the three threads round-robin under the timer, then efi_main resumes after the scheduler stops and prints BADC-PREEMPT-OK.

On x86_64 every vector the demo does not install gets a diagnostic gate: a 16-byte stub pushes its vector number and jumps to a common handler that prints the vector, the error code where the CPU pushed one, and the faulting RIP, then halts. Without them an unexpected exception escalates to a triple fault, which resets the guest with nothing on the serial line. Building with -DPREEMPT_FAULT_INJECT raises #GP right after the IDT is installed, which is how the smoke checks the diagnostic.

Both arch_start_scheduler implementations mask interrupts before they touch the vector table. UEFI enters an application with interrupts enabled and the firmware’s own timer running – on x86_64 that is IRQ0 through the 8259, whose initialization sequence clears the master’s vector base and mask until ICW2 arrives, so an IRQ0 taken in that six-instruction window arrives at vector 0 and lands on the demo’s unhandled-fault gate. Building with -DPREEMPT_PIC_WINDOW_STRESS holds the window open past a firmware timer period, which turns that race into a certainty; the smoke boots it and requires the normal markers.

All addresses and saved stack pointers use the pointer-width UINTN (unsigned long long), not unsigned long, because the EFI targets are LLP64 (long is 32-bit); a 32-bit IDT base or saved SP would fault on the first tick.

^ To the top