Gabriel Kaszewski a2d4a7d085 perf(kernel): kernel static all-zero -> .bss (image 812K -> 173K): domain::Slot (repr(u8) Empty=0) for tables, zero generation counters, core ids by position, pool/platform installed at boot; Option-backed Slot under kani (cbmc speed); build fails if .data > 16K

2026-10-28 13:01:52 +01:00

..

capability

refactor: unsafe only in adapter + libkos; forbid(unsafe_code) everywhere else; libkos Window (volatile, bounds-checked MMIO/DMA/shared mem), entry!, thread::spawn; MapRegion returns pages; kernel const-built (with_cores/install_platform); newtype addrs

2026-10-27 21:43:24 +01:00

endpoint

perf(kernel): kernel static all-zero -> .bss (image 812K -> 173K): domain::Slot (repr(u8) Empty=0) for tables, zero generation counters, core ids by position, pool/platform installed at boot; Option-backed Slot under kani (cbmc speed); build fails if .data > 16K

2026-10-28 13:01:52 +01:00

irq

refactor: unsafe only in adapter + libkos; forbid(unsafe_code) everywhere else; libkos Window (volatile, bounds-checked MMIO/DMA/shared mem), entry!, thread::spawn; MapRegion returns pages; kernel const-built (with_cores/install_platform); newtype addrs

2026-10-27 21:43:24 +01:00

memory

perf(kernel): kernel static all-zero -> .bss (image 812K -> 173K): domain::Slot (repr(u8) Empty=0) for tables, zero generation counters, core ids by position, pool/platform installed at boot; Option-backed Slot under kani (cbmc speed); build fails if .data > 16K

2026-10-28 13:01:52 +01:00

message

feat(storage): scoped grants (subtree, ro/rw), narrow-only, release revokes all holders; IPC KEEP_DELEGATE opt-in; shell cd/pwd, programs get ro cwd

2026-10-27 20:20:34 +01:00

notification

perf(kernel): kernel static all-zero -> .bss (image 812K -> 173K): domain::Slot (repr(u8) Empty=0) for tables, zero generation counters, core ids by position, pool/platform installed at boot; Option-backed Slot under kani (cbmc speed); build fails if .data > 16K

2026-10-28 13:01:52 +01:00

process

perf(kernel): kernel static all-zero -> .bss (image 812K -> 173K): domain::Slot (repr(u8) Empty=0) for tables, zero generation counters, core ids by position, pool/platform installed at boot; Option-backed Slot under kani (cbmc speed); build fails if .data > 16K

2026-10-28 13:01:52 +01:00

proofs

feat(kernel): per-process budgets (pages, endpoints, notifs, regions) carved from creator, returned on death; init owns pool

2026-10-27 15:08:58 +01:00

scheduler

perf(kernel): kernel static all-zero -> .bss (image 812K -> 173K): domain::Slot (repr(u8) Empty=0) for tables, zero generation counters, core ids by position, pool/platform installed at boot; Option-backed Slot under kani (cbmc speed); build fails if .data > 16K

2026-10-28 13:01:52 +01:00

thread

perf(kernel): kernel static all-zero -> .bss (image 812K -> 173K): domain::Slot (repr(u8) Empty=0) for tables, zero generation counters, core ids by position, pool/platform installed at boot; Option-backed Slot under kani (cbmc speed); build fails if .data > 16K

2026-10-28 13:01:52 +01:00

budget_tests.rs

feat(kernel): per-process budgets (pages, endpoints, notifs, regions) carved from creator, returned on death; init owns pool

2026-10-27 15:08:58 +01:00

budget.rs

feat(kernel): per-process budgets (pages, endpoints, notifs, regions) carved from creator, returned on death; init owns pool

2026-10-27 15:08:58 +01:00

error.rs

feat: kernel W^X (per-section perms, firmware unmapped, stack guard, boot check), halt on kernel faults, region W^X across processes

2026-10-27 00:13:00 +01:00

fault.rs

feat: add Halt syscall, fault notification to fault handler, supervisor with back-off, shutdown with timeout

2026-10-18 03:29:05 +02:00

generations_tests.rs

perf(kernel): kernel static all-zero -> .bss (image 812K -> 173K): domain::Slot (repr(u8) Empty=0) for tables, zero generation counters, core ids by position, pool/platform installed at boot; Option-backed Slot under kani (cbmc speed); build fails if .data > 16K

2026-10-28 13:01:52 +01:00

generations.rs

perf(kernel): kernel static all-zero -> .bss (image 812K -> 173K): domain::Slot (repr(u8) Empty=0) for tables, zero generation counters, core ids by position, pool/platform installed at boot; Option-backed Slot under kani (cbmc speed); build fails if .data > 16K

2026-10-28 13:01:52 +01:00

lib.rs

perf(kernel): kernel static all-zero -> .bss (image 812K -> 173K): domain::Slot (repr(u8) Empty=0) for tables, zero generation counters, core ids by position, pool/platform installed at boot; Option-backed Slot under kani (cbmc speed); build fails if .data > 16K

2026-10-28 13:01:52 +01:00

resource.rs

feat(kernel): console cap gates DebugPutchar, no uart fast path; spawn start arg in a0; delegate returns slot

2026-10-27 14:54:36 +01:00

slot.rs

perf(kernel): kernel static all-zero -> .bss (image 812K -> 173K): domain::Slot (repr(u8) Empty=0) for tables, zero generation counters, core ids by position, pool/platform installed at boot; Option-backed Slot under kani (cbmc speed); build fails if .data > 16K

2026-10-28 13:01:52 +01:00

syscall.rs

feat(ipc): saved replies: SaveReply/ReplySaved (8 per thread, released on thread death, unforgeable); terminal READ saved until Enter (line.rs editor, reader queue), now pinged

2026-10-28 02:09:34 +01:00

timer_tests.rs

feat(kernel): WatchDeath + SetTimer events as notification signals; adapter wakes at earliest deadline

2026-10-27 16:06:04 +01:00

timer.rs

feat(init): spawn service over IPC with per-client allowance refunded on child death; up to 4 death watchers; spawntest on test image

2026-10-27 16:21:08 +01:00