Commit Graph

27 Commits

Author SHA1 Message Date
38f20cc3c4 feat: proper IPC-based boot — init loads servers from storage via IPC, VirtIO GPU driver
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).
2026-10-18 13:02:30 +02:00
ffde4065ba fix: full init boot logic works — CreateProcess no longer spawns threads, boot uses out-param to avoid sret bug
- CreateProcess only creates process + grants cap, no thread spawning
- boot::boot takes &mut BootResult instead of returning it (fixes -> ! sret convention issue)
- Init creates 6 server processes, sets up supervisor, enters receive loop
- No faults on QEMU with full boot sequence
2026-10-18 04:57:20 +02:00
b7bc223a79 feat: add Halt syscall, fault notification to fault handler, supervisor with back-off, shutdown with timeout
- 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
2026-10-18 03:29:05 +02:00
896c78088a feat: implement configure_protection and map_shared with real page mapping, remove dead context_switch from Platform trait 2026-10-18 02:39:36 +02:00
7724a5bd0a feat: implement context switching, SavedContext with pc/status fields, wire all syscall outcomes and timer preemption 2026-10-18 02:34:36 +02:00
66a730b2fe feat(adapter-riscv): IPC demo — two processes exchange a message on QEMU virt 2026-10-18 01:58:18 +02:00
dcadb83088 feat: add Platform::map_shared and wire memory delegation to page mapping 2026-10-18 01:30:23 +02:00
142505d8a4 feat: add SavedContext::with_entry_and_stack, wire SpawnThread to preserve entry point and stack 2026-10-18 01:24:56 +02:00
4833f2e2bb feat(kernel): add Revoke syscall for generation-based capability revocation 2026-10-18 01:23:24 +02:00
241fefe2d4 refactor(kernel): extract MockPlatform and test helpers into separate modules 2026-10-18 01:16:24 +02:00
192631d506 feat(kernel): implement generation-based capability revocation with proofs and tests 2026-10-18 01:11:24 +02:00
71518a93a4 refactor(proofs): split into per-topic modules with shared helpers across types, domain, and kernel 2026-10-18 01:08:05 +02:00
e5fd6372b3 feat(proofs): add complete mediation, message integrity, and revocation proofs 2026-10-18 01:03:54 +02:00
74bdd1fd08 fix(proofs): replace tautological delegate guard proof with check_cap path verification 2026-10-18 01:01:20 +02:00
acc59830ff feat: add Kani proofs for delegation non-escalation across types, domain, and kernel 2026-10-18 00:55:52 +02:00
2c4a9dbadc refactor(kernel): move SyscallOutcome/Result to syscall module, move test helpers to tests module 2026-10-18 00:39:28 +02:00
38ebb6002b refactor(kernel): split syscall.rs into per-tier modules (simple, memory, lifecycle, capability, ipc) 2026-10-18 00:36:34 +02:00
b8c5090fe5 fix(kernel): fix kill wait-queue cleanup, RegionId tracking, ReleasePages ownership, and SwitchTo scheduler state 2026-10-18 00:31:05 +02:00
8912a944b8 feat(kernel): add WaitForInterrupt, AcknowledgeInterrupt, and WaitAny syscalls 2026-10-18 00:26:11 +02:00
e7835c0435 feat(kernel): add Send and Receive IPC syscalls with rendezvous 2026-10-18 00:24:09 +02:00
ae6023081a feat(kernel): add Delegate syscall for capability delegation 2026-10-18 00:22:37 +02:00
07534e52d9 feat(kernel): add SpawnThread, CreateProcess, and Kill syscalls 2026-10-18 00:21:01 +02:00
471d96b9a4 feat(kernel): add RequestPages and ReleasePages syscalls 2026-10-18 00:19:24 +02:00
95c023f286 feat(kernel): add handle_tick and handle_interrupt entry points 2026-10-18 00:17:55 +02:00
74b296a2bf feat(kernel): add Exit and ExitThread syscalls with process cleanup 2026-10-18 00:16:38 +02:00
d0a0ba788f feat(kernel): add Kernel struct, MockPlatform, and simple syscalls (GetTime, GetProcessId, Yield) 2026-10-18 00:15:40 +02:00
bb99c3001d init 2026-10-16 02:32:24 +02:00