Commit Graph

26 Commits

Author SHA1 Message Date
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