Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Memory Management

Memory management gives the kernel controlled ownership of physical frames, separates user processes, enforces page permissions, and exposes memory authority only through explicit capabilities.

Status: Partially implemented. Physical frame allocation, heap initialization, kernel page-table remapping, per-process address spaces, ELF/user stack/TLS mappings, user-buffer validation, FrameAllocator, MemoryObject, and VirtualMemory caps are implemented. SMP-safe validation, mapped shared buffers, huge pages, and hardware I/O memory isolation remain open.

Current Behavior

The frame allocator builds a bitmap from the Limine memory map, marks all non-usable frames as used, reserves frame zero, and reserves its own bitmap frames. The heap is initialized separately for kernel allocation.

Paging initialization builds a new kernel PML4, remaps kernel sections with section-specific permissions, copies upper-half mappings with NX applied and user access stripped, switches CR3, then enables page-global support. SMEP/SMAP are enabled after those mappings are active.

Each user AddressSpace owns its lower-half page tables and clones the kernel’s upper-half mappings. Dropping an address space walks the user half and frees mapped frames and page-table frames. VirtualMemory lets a process map, unmap, and protect anonymous user pages. Anonymous VM pages charge the process ResourceLedger::frame_grant_pages counter, while AddressSpace keeps owned-range tracking at the same shared process limit.

FrameAllocator allocation methods return a MemoryObject result capability, not a physical address. The normal result payload carries the result-cap index, and the CQE transfer-result record carries the local cap id plus MemoryObject interface id. MemoryObject.info exposes page count and size; held MemoryObject caps charge the holder’s frame_grant_pages ledger, and final CAP_OP_RELEASE or process exit frees the owned frames. Mapping a MemoryObject into an address space remains future work.

Design

The kernel keeps physical allocation host-testable by placing bitmap logic in capos-lib and wrapping it with kernel HHDM access in kernel/src/mem/frame.rs. Page-table manipulation stays in the kernel because it is architecture-specific.

ELF loading and VirtualMemory both use page-table flags to preserve W^X: non-executable data gets NX, writable mappings are explicit, and userspace pages must be USER_ACCESSIBLE. The CapSet and ring bootstrap pages occupy reserved virtual pages; VirtualMemory rejects ranges that overlap either one.

User-buffer validation checks that user pointers stay below the user address limit and that page-table permissions match the requested access. SMAP UserAccessGuard brackets kernel copy operations into or out of user pages.

VirtualMemory mappings and held MemoryObject caps use the same per-process frame-grant ledger, with quota checks before frame allocation or mapping side effects. Future shared-buffer and DMA resources should reuse that authority ledger instead of adding one-off counters per cap.

Invariants

  • Frame addresses are 4 KiB aligned.
  • The frame bitmap’s own frames are never returned as free frames.
  • Upper-half kernel mappings are not user-accessible.
  • Kernel text is RX, rodata is read-only NX, and data/bss are RW NX.
  • User address spaces own only lower-half page-table frames.
  • Process frame-grant usage covers live anonymous VM pages and held MemoryObject caps.
  • VirtualMemory caps are bound to one address space and are not valid cross-process service exports.
  • CapSet is read-only/no-execute; ring is writable/no-execute.
  • VirtualMemory cannot map, unmap, or protect the ring or CapSet pages.
  • VirtualMemory protect/unmap only succeeds for pages tracked as owned by the cap’s address space.

Code Map

  • capos-lib/src/frame_bitmap.rs - host-testable physical frame bitmap core.
  • capos-lib/src/cap_table.rs - capability holds and per-process ResourceLedger frame-grant accounting.
  • capos-lib/src/frame_ledger.rs - bounded frame-grant helper retained for host tests.
  • kernel/src/mem/frame.rs - Limine memory-map integration and global frame allocator wrapper.
  • kernel/src/mem/heap.rs - kernel heap setup.
  • kernel/src/mem/paging.rs - kernel remap, AddressSpace, page mapping, VM-cap page tracking, user copy helpers.
  • kernel/src/mem/validate.rs - user-buffer validation.
  • kernel/src/cap/frame_alloc.rs - FrameAllocator capability and cleanup.
  • kernel/src/cap/virtual_memory.rs - VirtualMemory capability.
  • kernel/src/spawn.rs - ELF, stack, and TLS user mappings.
  • kernel/src/arch/x86_64/smap.rs - SMEP/SMAP setup and user access guard.

Validation

  • cargo test-lib covers frame bitmap, frame ledger, ELF parser, and cap-table pure logic.
  • cargo miri-lib runs host-testable capos-lib tests under Miri when installed.
  • make kani-lib proves bounded frame bitmap, cap ID, and ELF parser invariants when Kani is installed.
  • make run validates ELF mapping, process teardown, MemoryObject-backed FrameAllocator cleanup, TLS, VirtualMemory map/protect/unmap/quota/release smoke, and clean halt.
  • make run-spawn validates ELF load failure rollback and frame exhaustion handling through ProcessSpawner.

Open Work

  • Extend frame-grant accounting to future shared-memory and DMA resources.
  • Harden user-buffer validation for SMP-era page-table races.
  • Add MemoryObject map/unmap and shared-buffer operations for zero-copy data paths.
  • Add DMA isolation and device memory capability boundaries before userspace drivers.
  • Add huge-page handling only with explicit ownership and teardown rules.