Architecture Overview

Daxo OS is a microkernel – only the most essential services run in privileged mode (Ring 0). Drivers, file systems, and user applications reside in user space (Ring 3) and communicate via system calls.

Memory Management

Paging

Uses the x86_64 4-level page table hierarchy. The kernel maps its own code and data at high virtual addresses (offset by physical_memory_offset).

Heap Allocators

Three allocators are implemented:

  • Bump – simple, used for early init.
  • Linked List – manages freed blocks.
  • Fixed‑Size Block – the default global allocator, with fallback to linked list.

Physical Frame Allocator

BootInfoFrameAllocator scans the memory map provided by the bootloader and returns usable frames. It is formally verified in Lean 4 (see verification/).

User Memory Isolation

User pages are mapped with USER_ACCESSIBLE flag. Attempts to access kernel memory from Ring 3 trigger a page fault.

let user_flags = PageTableFlags::PRESENT | PageTableFlags::WRITABLE | PageTableFlags::USER_ACCESSIBLE;

Task Scheduler (Async Executor)

Cooperative multitasking based on Rust futures. Each task is a Future that yields when waiting for I/O. The executor maintains a queue of ready tasks and wakes them via Waker.

Idle state: when the queue is empty, the CPU executes hlt until the next interrupt.

Key files: src/task/executor.rs, src/task/keyboard.rs.

Interrupts and Exceptions

IDT – handlers for:

  • Breakpoint (int 3)
  • Double Fault (with separate IST stack)
  • Page Fault (logs address and error code)
  • Timer (IRQ0) – currently no‑op
  • Keyboard (IRQ1) – pushes scancodes into queue

GDT – defines kernel and user code/data segments, and a TSS for stack switching.

PIC – remapped to offsets 0x20 and 0x28.

Drivers

ATA PIO

Uses ports 0x1F0‑0x1F7. Implements polling (wait_ready, wait_data) before interrupt setup to avoid early IRQs. Reads a sector into a 512‑byte buffer.

pub fn read_sector(&mut self, lba: u32, buffer: &mut [u8; 512]);

PS/2 Keyboard

IRQ1 handler reads scancode from port 0x60 and pushes it to a lock‑free queue. An async stream (ScancodeStream) decodes keys using the pc-keyboard crate.

Serial (COM1)

Used for logging and test output. Implements serial_print! and serial_println!.

System Calls

Currently only a stub for syscall (number 1) that prints a dot. The infrastructure is set up in src/syscall.rs and called from user code via syscall instruction.

Future plans: memory allocation, process creation, file I/O.

User Mode (Ring 3)

Transition is performed with iretq. The kernel prepares a stack frame containing SS, RSP, RFLAGS, CS, and RIP. The jump_to_user_space function in gdt.rs executes this instruction.

User code runs on a dedicated page (e.g., at 0x0000_1000_0000_0000) with the USER_ACCESSIBLE flag. The example user program is a simple infinite loop that makes a syscall to print dots.

Formal Verification

The physical frame allocator is modelled in Lean 4. The property allocate_marks_as_allocated ensures that after allocation, a frame is marked as used. This proof increases trust in the memory management subsystem.

Files: verification/FrameVerify.lean, verification/lakefile.lean.