- caps record parent (mint/delegate/ipc), CapRef w/ pid+slot gens
- Revoke = delete subtree, keep self; drop/death re-parents children
- CreateRegion/MapRegion; mapping lives only as long as its cap
- drop Permission::Revoke + object-wide revoke
- mint any cap (badge only ep/ntfn), process caps delegable
- kani: descendants == subtree; model-based fuzz vs spec
- RunList -> intrusive FIFO, no starvation, no silent drop
- cap table sized to CapSlot range (kani caught OOB panic)
- snake food color test uses const
- kani cfg lint, RUST_MIN_STACK for big kernel struct in tests
TimeSlice::DEFAULT and Priority::DEFAULT already exist with the
same values. Using them makes the intent clear and centralizes
the default values.
TimeSlice::new(2) in tick test is intentional — tests preemption
after 2 ticks specifically.
Page lifecycle:
- ProcessMemory now tracks (PhysicalAddress, count) pairs for each
allocation (up to 16). destroy_process iterates and frees all
pages back to the pool. No more permanent page leaks on exit/fault.
- RequestPages re-adds MemoryRegion entries so ReleasePages works.
Release test un-ignored, passes.
- RequestPages: VA allocation moved after pool allocation succeeds,
preventing VA leak on OOM.
IPC hardening:
- WaitQueue overflow (>16 waiters): returns WouldBlock error instead
of silently dropping the thread. Thread is not blocked if enqueue
fails.
- debug_assert on pending_messages[sender].take() — invariant that
a sender in wait queue must have a pending message.
Scheduler:
- remove() now clears current thread if the removed thread was
current on its core.
- add() asserts push succeeded; bitmap bit only set if thread was
actually added to RunList.
Cleanup:
- Priority::DEFAULT replaces Priority::new(16).unwrap() in
spawn_thread and spawn_thread_in.
36 kernel tests pass, 0 ignored.
Tests:
- IPC tests: spawn thread B explicitly (CreateProcess no longer
spawns threads since the boot logic fix)
- Memory tests: RequestPages now returns Value(va) not Slot(cap)
- MockPlatform: tracks VA→PA mappings for translate_va
- ReleasePages test: ignored (RequestPages no longer creates
regions — ReleasePages needs redesign)
CapSlot::const_new(value):
- const fn that panics at compile time for invalid values
- Replaces CapSlot::new(N).unwrap() in init, echo, snake
- Cap slot constants are now compile-time verified
Also fixes handle_release_pages to use translate_va instead of
treating VA as PA directly.
35 kernel tests pass, 1 ignored.
Complete microkernel boot pipeline: adapter loads only init + storage + display
from disk. Init bootstraps all other servers by reading binaries from the
storage server via IPC, parsing ELF, creating processes, mapping pages, and
spawning threads.
New syscalls:
- CreateEndpoint: userspace endpoint creation with full capability grant
- DebugPutchar: debug output to UART from userspace
- MapPage: cross-process page mapping (init loads binaries into children)
- SpawnThreadIn: spawn thread in another process via capability
Key fixes:
- Per-process L1 page tables for VPN[2]=0 (prevents cross-process corruption)
- Separate kernel_pt from page_tables[0] (init pid=0 overwrote kernel PT ref)
- Thread Running state set in switch_to_next (syscalls rejected without it)
- Pending IPC results applied during context switch
- SIE disabled during boot (timer can't preempt into unready processes)
- User heap VA starts at 0x40000 (avoids shared buffer at 0x30000)
- RequestPages maps at user VAs via per-process heap allocator
VirtIO GPU:
- Adapter probes for GPU device, initializes resource/scanout/backing
- Display server writes to mapped framebuffer, flushes via GPU virtqueue
- 640x480 BGRA framebuffer with transfer-to-host and resource-flush
Storage server:
- Userspace VirtIO block driver using pre-mapped MMIO and DMA pages
- FAT16 filesystem reader serving file-read requests via IPC
- Shared buffer protocol: init writes filename, storage writes file data
Echo app for IPC testing (adapter-loaded echo proved the pipeline end-to-end).
- Halt syscall: only pid 0 (init) can halt, adapter uses SBI SRST
- Fault notification: kernel delivers fault info to process fault handler endpoint before killing
- Supervisor: tracks restart counts, back-off up to 5 restarts
- Shutdown: notifies servers, waits with timeout, calls halt
- Trap handler: faults now call kernel.handle_fault instead of halting
