From a2d4a7d085603c5fa969bed0b53cbffe1ddfd351 Mon Sep 17 00:00:00 2001 From: Gabriel Kaszewski Date: Wed, 28 Oct 2026 13:01:52 +0100 Subject: [PATCH] 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 --- Makefile | 6 + crates/adapter-riscv/src/boot/hardware.rs | 4 + crates/adapter-riscv/src/kernel_cell.rs | 4 - crates/adapter-riscv/src/main.rs | 13 +- crates/domain/src/endpoint/mod.rs | 12 +- crates/domain/src/generations.rs | 48 ++++++-- crates/domain/src/generations_tests.rs | 5 +- crates/domain/src/lib.rs | 1 + crates/domain/src/memory/frame/mod.rs | 55 ++++++--- crates/domain/src/memory/frame/proofs.rs | 38 +++--- crates/domain/src/memory/mod.rs | 8 +- crates/domain/src/notification/mod.rs | 12 +- crates/domain/src/process/mod.rs | 8 +- crates/domain/src/scheduler/multi_core.rs | 16 +-- crates/domain/src/scheduler/per_core.rs | 16 +-- crates/domain/src/scheduler/tests.rs | 8 +- crates/domain/src/slot.rs | 144 ++++++++++++++++++++++ crates/domain/src/thread/table.rs | 10 +- crates/kernel/src/lib.rs | 10 +- crates/kernel/src/syscall/ipc/endpoint.rs | 2 +- crates/kernel/src/syscall/ipc/mod.rs | 6 +- crates/kernel/src/teardown.rs | 2 +- crates/kernel/src/tests/ipc_invariants.rs | 4 +- crates/kernel/src/tests/storm.rs | 4 +- 24 files changed, 320 insertions(+), 116 deletions(-) create mode 100644 crates/domain/src/slot.rs diff --git a/Makefile b/Makefile index f4c47ee..e6e1b64 100644 --- a/Makefile +++ b/Makefile @@ -61,6 +61,12 @@ PROGRAMS = -p init -p echo -p sleep -p snake \ build: cargo build --target $(RISCV_TARGET) --release $(PROGRAMS) cargo build --target $(RISCV_TARGET) --release -p adapter-riscv + @# The kernel's tables are one static: if every empty entry is zero it + @# lives in .bss and costs nothing in the image (see domain::slot). + @data=$$(llvm-size -A $(KERNEL_BIN) | awk '$$1 == ".data" { print $$2 }'); \ + if [ "$${data:-0}" -gt 16384 ]; then \ + echo "kernel .data is $$data bytes: some table's empty value is not all zero bytes (use domain::slot::Slot)"; exit 1; \ + fi # The keystore holds the owner's sealed keys: made once, never rebuilt. KEYS_IMG ?= keys.img diff --git a/crates/adapter-riscv/src/boot/hardware.rs b/crates/adapter-riscv/src/boot/hardware.rs index e878099..17a1386 100644 --- a/crates/adapter-riscv/src/boot/hardware.rs +++ b/crates/adapter-riscv/src/boot/hardware.rs @@ -57,6 +57,10 @@ pub fn init(uart: &Uart, boot_hart: usize) -> &'static mut mmu::PageTable { let riscv_platform = platform::RiscVPlatform::new(kernel_pt as *const mmu::PageTable as usize, harts as u8); crate::kern_mut().install_platform(riscv_platform); + crate::kern_mut().install_pool( + types::address::PhysicalAddress::from_raw(board::USER_POOL_BASE), + board::USER_POOL_PAGES, + ); kernel_pt } diff --git a/crates/adapter-riscv/src/kernel_cell.rs b/crates/adapter-riscv/src/kernel_cell.rs index 074bc57..997f474 100644 --- a/crates/adapter-riscv/src/kernel_cell.rs +++ b/crates/adapter-riscv/src/kernel_cell.rs @@ -1,9 +1,7 @@ use core::cell::UnsafeCell; use core::mem::MaybeUninit; -use core::sync::atomic::{AtomicBool, Ordering}; pub struct KernelCell { - initialized: AtomicBool, inner: UnsafeCell>, } @@ -15,14 +13,12 @@ impl KernelCell { /// never lives on the stack. pub const fn new(value: T) -> Self { Self { - initialized: AtomicBool::new(true), inner: UnsafeCell::new(MaybeUninit::new(value)), } } /// Raw pointer to the kernel; callers must avoid aliasing `&mut`. pub fn as_ptr(&self) -> *mut T { - debug_assert!(self.initialized.load(Ordering::Acquire)); unsafe { (*self.inner.get()).as_mut_ptr() } } } diff --git a/crates/adapter-riscv/src/main.rs b/crates/adapter-riscv/src/main.rs index 2f9673e..f7e4396 100644 --- a/crates/adapter-riscv/src/main.rs +++ b/crates/adapter-riscv/src/main.rs @@ -15,14 +15,15 @@ mod trap; use hw::uart::Uart; use kernel_cell::KernelCell; -/// Built at compile time; boot installs the real platform before anything -/// runs. +/// Built at compile time with nothing in it (no platform, no cores, no +/// pool), so every byte is zero and it lives in `.bss`, not in the image; +/// boot installs the platform and the pool before anything runs. static KERNEL: KernelCell> = KernelCell::new(kernel::Kernel::with_cores( - platform::RiscVPlatform::new(0, 1), - 1, - types::address::PhysicalAddress::from_raw(board::USER_POOL_BASE), - board::USER_POOL_PAGES, + platform::RiscVPlatform::new(0, 0), + 0, + types::address::PhysicalAddress::from_raw(0), + 0, )); fn kern_mut() -> &'static mut kernel::Kernel { diff --git a/crates/domain/src/endpoint/mod.rs b/crates/domain/src/endpoint/mod.rs index f356317..b9500c0 100644 --- a/crates/domain/src/endpoint/mod.rs +++ b/crates/domain/src/endpoint/mod.rs @@ -93,14 +93,14 @@ impl Endpoint { pub const MAX_ENDPOINTS: usize = if cfg!(kani) { 2 } else { 256 }; pub struct EndpointTable { - endpoints: [Option; MAX_ENDPOINTS], + endpoints: [crate::slot::Slot; MAX_ENDPOINTS], generations: SlotGenerations, } impl EndpointTable { pub const fn new() -> Self { Self { - endpoints: [const { None }; MAX_ENDPOINTS], + endpoints: [const { crate::slot::Slot::Empty }; MAX_ENDPOINTS], generations: SlotGenerations::new(), } } @@ -111,9 +111,9 @@ impl EndpointTable { .endpoints .iter_mut() .enumerate() - .find(|(i, s)| s.is_none() && generations.is_usable(*i))?; + .find(|(i, s)| !s.is_full() && generations.is_usable(*i))?; let id = EndpointId::from_raw(idx as u16); - *slot = Some(Endpoint::new(id, owner)); + slot.set(Endpoint::new(id, owner)); Some(id) } @@ -124,13 +124,13 @@ impl EndpointTable { } pub fn iter(&self) -> impl Iterator { - self.endpoints.iter().flatten() + self.endpoints.iter().filter_map(crate::slot::Slot::as_ref) } pub fn ids_owned_by(&self, owner: ProcessId) -> impl Iterator + '_ { self.endpoints .iter() - .flatten() + .filter_map(crate::slot::Slot::as_ref) .filter(move |ep| ep.owner == owner) .map(|ep| ep.id) } diff --git a/crates/domain/src/generations.rs b/crates/domain/src/generations.rs index 3f79196..a3b5aed 100644 --- a/crates/domain/src/generations.rs +++ b/crates/domain/src/generations.rs @@ -6,21 +6,44 @@ use types::generation::Generation; #[path = "generations_tests.rs"] mod tests; +/// One slot's counter. A fresh one is all zero bytes (not retired, +/// generation 0), so tables of them cost nothing in the kernel image. +#[derive(Clone, Copy)] +struct Counter { + retired: bool, + generation: Generation, +} + +impl Counter { + const FRESH: Self = Self { + retired: false, + generation: Generation::initial(), + }; + const RETIRED: Self = Self { + retired: true, + generation: Generation::initial(), + }; + + fn get(self) -> Option { + (!self.retired).then_some(self.generation) + } +} + /// Bumped on every destroy or revoke so older capabilities stop matching; a slot whose counter runs out is retired. pub struct SlotGenerations { - gens: [Option; N], + gens: [Counter; N], } impl SlotGenerations { pub const fn new() -> Self { Self { - gens: [Some(Generation::initial()); N], + gens: [Counter::FRESH; N], } } /// Current generation of `idx`, `None` if retired or out of range. pub fn current(&self, idx: usize) -> Option { - *self.gens.get(idx)? + self.gens.get(idx)?.get() } pub fn is_usable(&self, idx: usize) -> bool { @@ -30,7 +53,13 @@ impl SlotGenerations { /// Invalidates every capability minted for the current generation. pub fn advance(&mut self, idx: usize) { if let Some(g) = self.gens.get_mut(idx) { - *g = g.and_then(|g| g.next()); + *g = match g.get().and_then(|g| g.next()) { + Some(generation) => Counter { + retired: false, + generation, + }, + None => Counter::RETIRED, + }; } } } @@ -43,7 +72,7 @@ impl Default for SlotGenerations { #[cfg(kani)] mod proofs { - use super::SlotGenerations; + use super::{Counter, SlotGenerations}; use types::generation::Generation; /// However many times a slot is advanced, a generation observed earlier @@ -53,9 +82,12 @@ mod proofs { fn an_observed_generation_never_returns() { let mut g: SlotGenerations<1> = SlotGenerations::new(); g.gens[0] = if kani::any() { - Some(Generation::from_raw(kani::any())) + Counter { + retired: false, + generation: Generation::from_raw(kani::any()), + } } else { - None + Counter::RETIRED }; let observed = g.current(0); let steps: u8 = kani::any(); @@ -73,7 +105,7 @@ mod proofs { #[kani::unwind(5)] fn retired_slots_stay_retired() { let mut g: SlotGenerations<1> = SlotGenerations::new(); - g.gens[0] = None; + g.gens[0] = Counter::RETIRED; let steps: u8 = kani::any(); kani::assume(steps <= 4); for _ in 0..steps { diff --git a/crates/domain/src/generations_tests.rs b/crates/domain/src/generations_tests.rs index b735e08..2695d90 100644 --- a/crates/domain/src/generations_tests.rs +++ b/crates/domain/src/generations_tests.rs @@ -27,7 +27,10 @@ fn out_of_range_slots_are_never_usable() { #[test] fn exhausted_counter_retires_the_slot() { let mut g: SlotGenerations<1> = SlotGenerations::new(); - g.gens[0] = Some(Generation::from_raw(u32::MAX)); + g.gens[0] = super::Counter { + retired: false, + generation: Generation::from_raw(u32::MAX), + }; g.advance(0); assert_eq!(g.current(0), None); assert!(!g.is_usable(0)); diff --git a/crates/domain/src/lib.rs b/crates/domain/src/lib.rs index 525f434..9e9c676 100644 --- a/crates/domain/src/lib.rs +++ b/crates/domain/src/lib.rs @@ -31,6 +31,7 @@ pub mod notification; pub mod process; pub mod resource; pub mod scheduler; +pub mod slot; pub mod syscall; pub mod thread; pub mod timer; diff --git a/crates/domain/src/memory/frame/mod.rs b/crates/domain/src/memory/frame/mod.rs index 60c136f..488b289 100644 --- a/crates/domain/src/memory/frame/mod.rs +++ b/crates/domain/src/memory/frame/mod.rs @@ -1,6 +1,7 @@ //! Physical frame ownership. The kernel's single source of truth for what //! every frame of the user pool is used for and who is charged for it. +use crate::slot::Slot; use types::{ address::{PhysicalAddress, VirtualAddress}, id::{ProcessId, RegionId}, @@ -48,7 +49,7 @@ impl FrameUse { pub struct FrameTable { base: PhysicalAddress, total: usize, - frames: [Option; N], + frames: [Slot; N], free: usize, /// Where the next allocation starts looking: just past the last one. cursor: usize, @@ -60,12 +61,23 @@ impl FrameTable { Self { base, total, - frames: [None; N], + frames: [Slot::Empty; N], free: total, cursor: 0, } } + /// The pool, given at boot to a table made (in the kernel's static) + /// without one; only while nothing is allocated. + pub fn set_pool(&mut self, base: PhysicalAddress, total: usize) { + if self.free == self.total && self.live().iter().all(|f| !f.is_full()) { + self.base = base; + self.total = total.min(N); + self.free = self.total; + self.cursor = 0; + } + } + pub fn base(&self) -> PhysicalAddress { self.base } @@ -92,11 +104,11 @@ impl FrameTable { } /// The frames that exist (`total` is clamped to `N` at construction). - fn live(&self) -> &[Option] { + fn live(&self) -> &[Slot] { self.frames.get(..self.total).unwrap_or(&[]) } - fn live_mut(&mut self) -> &mut [Option] { + fn live_mut(&mut self) -> &mut [Slot] { self.frames.get_mut(..self.total).unwrap_or(&mut []) } @@ -113,8 +125,8 @@ impl FrameTable { let start = self.cursor.min(total); let idx = (start..total) .chain(0..start) - .find(|&i| self.frames.get(i).is_some_and(Option::is_none))?; - *self.frames.get_mut(idx)? = Some(usage); + .find(|&i| self.frames.get(i).is_some_and(|f| !f.is_full()))?; + self.frames.get_mut(idx)?.set(usage); self.free -= 1; self.cursor = idx + 1; Some(self.address_of(idx)) @@ -132,7 +144,7 @@ impl FrameTable { let mut run = 0; let mut start = None; for (idx, f) in self.live().iter().enumerate() { - if f.is_some() { + if f.is_full() { run = 0; continue; } @@ -145,7 +157,7 @@ impl FrameTable { let start = start?; let run = self.live_mut().get_mut(start..start + count)?; for (i, f) in run.iter_mut().enumerate() { - *f = Some(usage(i)); + f.set(usage(i)); } self.free -= count; Some(self.address_of(start)) @@ -165,7 +177,7 @@ impl FrameTable { match self .index_of(pa) .and_then(|i| self.frames.get_mut(i)) - .and_then(Option::as_mut) + .and_then(Slot::as_mut) { Some(slot) => { *slot = usage; @@ -205,14 +217,17 @@ impl FrameTable { return None; } let page = u32::try_from(va.raw() / PAGE_SIZE).ok()?; - self.live().iter().enumerate().find_map(|(idx, f)| match f { - Some(FrameUse::User { - owner: o, - page: p, - perms, - }) if *o == owner && *p == page => Some((self.address_of(idx), *perms)), - _ => None, - }) + self.live() + .iter() + .enumerate() + .find_map(|(idx, f)| match f.as_ref() { + Some(FrameUse::User { + owner: o, + page: p, + perms, + }) if *o == owner && *p == page => Some((self.address_of(idx), *perms)), + _ => None, + }) } /// Every allocated frame and its use. @@ -231,7 +246,7 @@ impl FrameTable { self.live() .iter() .enumerate() - .filter_map(move |(idx, f)| match f { + .filter_map(move |(idx, f)| match f.as_ref() { Some(FrameUse::User { owner: o, page, .. }) if *o == owner => Some(( self.address_of(idx), VirtualAddress::from_raw(*page as usize * PAGE_SIZE), @@ -246,11 +261,11 @@ impl FrameTable { let mut freed = 0; for slot in self.live_mut().iter_mut() { let owned = matches!( - slot, + slot.as_ref(), Some(FrameUse::User { owner: o, .. } | FrameUse::PageTable { owner: o }) if *o == owner ); if owned { - *slot = None; + *slot = Slot::Empty; freed += 1; } } diff --git a/crates/domain/src/memory/frame/proofs.rs b/crates/domain/src/memory/frame/proofs.rs index c48cbaf..b8a95d2 100644 --- a/crates/domain/src/memory/frame/proofs.rs +++ b/crates/domain/src/memory/frame/proofs.rs @@ -35,13 +35,17 @@ fn any_use() -> FrameUse { } } -fn any_slot() -> Option { - if kani::any() { Some(any_use()) } else { None } +fn any_slot() -> Slot { + if kani::any() { + Slot::Full(any_use()) + } else { + Slot::Empty + } } fn any_table() -> FrameTable { let frames = [any_slot(), any_slot(), any_slot(), any_slot()]; - let free = frames.iter().filter(|f| f.is_none()).count(); + let free = frames.iter().filter(|f| !f.is_full()).count(); FrameTable { base: PhysicalAddress::from_raw(BASE), total: N, @@ -53,7 +57,7 @@ fn any_table() -> FrameTable { } fn well_formed(t: &FrameTable) -> bool { - t.free == t.frames[..t.total].iter().filter(|f| f.is_none()).count() + t.free == t.frames[..t.total].iter().filter(|f| !f.is_full()).count() } fn any_pa() -> PhysicalAddress { @@ -71,8 +75,8 @@ fn alloc_only_hands_out_free_frames() { Some(pa) => { let idx = (pa.raw() - BASE) / PAGE_SIZE; assert!(idx < N); - assert!(before[idx].is_none()); - assert!(t.frames[idx] == Some(usage)); + assert!(!before[idx].is_full()); + assert!(t.frames[idx] == Slot::Full(usage)); for i in 0..N { if i != idx { assert!(t.frames[i] == before[i]); @@ -80,7 +84,7 @@ fn alloc_only_hands_out_free_frames() { } } None => { - assert!(before.iter().all(Option::is_some)); + assert!(before.iter().all(Slot::is_full)); assert!(t.frames == before); } } @@ -97,8 +101,8 @@ fn free_releases_exactly_one_allocated_frame_or_nothing() { Some(usage) => { let idx = (pa.raw() - BASE) / PAGE_SIZE; assert!(pa.raw() % PAGE_SIZE == 0); - assert!(before[idx] == Some(usage)); - assert!(t.frames[idx].is_none()); + assert!(before[idx] == Slot::Full(usage)); + assert!(!t.frames[idx].is_full()); for i in 0..N { if i != idx { assert!(t.frames[i] == before[i]); @@ -119,8 +123,8 @@ fn retag_never_allocates() { let usage = any_use(); let changed = t.retag(pa, usage); for i in 0..N { - if before[i].is_none() { - assert!(t.frames[i].is_none()); + if !before[i].is_full() { + assert!(!t.frames[i].is_full()); } } if !changed { @@ -138,11 +142,11 @@ fn free_owned_by_spares_everyone_else() { t.free_owned_by(owner); for i in 0..N { let was_owned = matches!( - before[i], - Some(FrameUse::User { owner: o, .. } | FrameUse::PageTable { owner: o }) if o == owner + before[i].as_ref(), + Some(FrameUse::User { owner: o, .. } | FrameUse::PageTable { owner: o }) if *o == owner ); if was_owned { - assert!(t.frames[i].is_none()); + assert!(!t.frames[i].is_full()); } else { assert!(t.frames[i] == before[i]); } @@ -162,7 +166,7 @@ fn find_user_only_reports_the_owners_mapping() { assert!(va.raw() % PAGE_SIZE == 0); assert!( t.frames[idx] - == Some(FrameUse::User { + == Slot::Full(FrameUse::User { owner, page: (va.raw() / PAGE_SIZE) as u32, perms, @@ -184,8 +188,8 @@ fn alloc_contiguous_only_claims_a_free_run() { assert!(count > 0 && start + count <= N); for i in 0..N { if i >= start && i < start + count { - assert!(before[i].is_none()); - assert!(t.frames[i] == Some(FrameUse::Region { region })); + assert!(!before[i].is_full()); + assert!(t.frames[i] == Slot::Full(FrameUse::Region { region })); } else { assert!(t.frames[i] == before[i]); } diff --git a/crates/domain/src/memory/mod.rs b/crates/domain/src/memory/mod.rs index 5fc4543..eb8fa69 100644 --- a/crates/domain/src/memory/mod.rs +++ b/crates/domain/src/memory/mod.rs @@ -117,14 +117,14 @@ impl Region { } pub struct RegionTable { - regions: [Option; MAX_REGIONS], + regions: [crate::slot::Slot; MAX_REGIONS], generations: SlotGenerations, } impl RegionTable { pub const fn new() -> Self { Self { - regions: [const { None }; MAX_REGIONS], + regions: [const { crate::slot::Slot::Empty }; MAX_REGIONS], generations: SlotGenerations::new(), } } @@ -139,7 +139,7 @@ impl RegionTable { self.regions .iter() .enumerate() - .position(|(i, r)| r.is_none() && self.generations.is_usable(i)) + .position(|(i, r)| !r.is_full() && self.generations.is_usable(i)) } /// The id the next `insert` will return. @@ -150,7 +150,7 @@ impl RegionTable { pub fn insert(&mut self, region: Region) -> Option { let idx = self.free_slot()?; - *self.regions.get_mut(idx)? = Some(region); + self.regions.get_mut(idx)?.set(region); Some(RegionId::from_raw(idx as u16)) } diff --git a/crates/domain/src/notification/mod.rs b/crates/domain/src/notification/mod.rs index d230c5c..c5169f2 100644 --- a/crates/domain/src/notification/mod.rs +++ b/crates/domain/src/notification/mod.rs @@ -128,14 +128,14 @@ impl Notification { } pub struct NotificationTable { - slots: [Option; MAX_NOTIFICATIONS], + slots: [crate::slot::Slot; MAX_NOTIFICATIONS], generations: SlotGenerations, } impl NotificationTable { pub const fn new() -> Self { Self { - slots: [const { None }; MAX_NOTIFICATIONS], + slots: [const { crate::slot::Slot::Empty }; MAX_NOTIFICATIONS], generations: SlotGenerations::new(), } } @@ -146,9 +146,9 @@ impl NotificationTable { .slots .iter_mut() .enumerate() - .find(|(i, s)| s.is_none() && generations.is_usable(*i))?; + .find(|(i, s)| !s.is_full() && generations.is_usable(*i))?; let id = NotificationId::from_raw(idx as u16); - *slot = Some(Notification::new(id, owner)); + slot.set(Notification::new(id, owner)); Some(id) } @@ -172,13 +172,13 @@ impl NotificationTable { } pub fn iter(&self) -> impl Iterator { - self.slots.iter().flatten() + self.slots.iter().filter_map(crate::slot::Slot::as_ref) } pub fn ids_owned_by(&self, owner: ProcessId) -> impl Iterator + '_ { self.slots .iter() - .flatten() + .filter_map(crate::slot::Slot::as_ref) .filter(move |n| n.owner == owner) .map(|n| n.id) } diff --git a/crates/domain/src/process/mod.rs b/crates/domain/src/process/mod.rs index e62a895..937483d 100644 --- a/crates/domain/src/process/mod.rs +++ b/crates/domain/src/process/mod.rs @@ -75,14 +75,14 @@ impl Process { } pub struct ProcessTable { - processes: [Option; MAX_PROCESSES], + processes: [crate::slot::Slot; MAX_PROCESSES], generations: SlotGenerations, } impl ProcessTable { pub const fn new() -> Self { Self { - processes: [const { None }; MAX_PROCESSES], + processes: [const { crate::slot::Slot::Empty }; MAX_PROCESSES], generations: SlotGenerations::new(), } } @@ -103,11 +103,11 @@ impl ProcessTable { .processes .iter_mut() .enumerate() - .find(|(i, s)| s.is_none() && generations.is_usable(*i)) + .find(|(i, s)| !s.is_full() && generations.is_usable(*i)) .ok_or(KernelError::TooManyProcesses)?; let id = ProcessId::from_raw(idx as u16); - *slot = Some(Process::new(id, capabilities, fault_handler)); + *slot = crate::slot::Slot::Full(Process::new(id, capabilities, fault_handler)); Ok(id) } diff --git a/crates/domain/src/scheduler/multi_core.rs b/crates/domain/src/scheduler/multi_core.rs index b8fff28..2abc4a9 100644 --- a/crates/domain/src/scheduler/multi_core.rs +++ b/crates/domain/src/scheduler/multi_core.rs @@ -22,17 +22,9 @@ pub struct MultiCoreScheduler { impl MultiCoreScheduler { pub const fn new(num_cores: u8) -> Self { - let mut cores = [const { PerCoreScheduler::new(CoreId::from_raw(0)) }; MAX_CORES]; - // Each core numbered by its place (a const fn cannot index or map). - let mut rest: &mut [PerCoreScheduler] = &mut cores; - let mut id = 0u8; - while let Some((core, tail)) = rest.split_first_mut() { - *core = PerCoreScheduler::new(CoreId::from_raw(id)); - rest = tail; - id += 1; - } + // A core is numbered by its place in `cores`. Self { - cores, + cores: [const { PerCoreScheduler::new() }; MAX_CORES], num_cores: if num_cores < MAX_CORES as u8 { num_cores } else { @@ -78,8 +70,8 @@ impl MultiCoreScheduler { pub fn queued_on(&self, thread: ThreadId) -> Option { self.active() .iter() - .find(|c| c.is_queued(thread)) - .map(|c| c.core()) + .position(|c| c.is_queued(thread)) + .map(|i| CoreId::from_raw(i as u8)) } /// Whether `thread` waits in some core's run queue. diff --git a/crates/domain/src/scheduler/per_core.rs b/crates/domain/src/scheduler/per_core.rs index 258ac95..1ddef09 100644 --- a/crates/domain/src/scheduler/per_core.rs +++ b/crates/domain/src/scheduler/per_core.rs @@ -1,26 +1,26 @@ use super::priority_queue::PriorityQueue; use types::bounded::Priority; -use types::id::{CoreId, ThreadId}; +use types::id::ThreadId; pub struct PerCoreScheduler { - core: CoreId, queue: PriorityQueue, current: Option, } +impl Default for PerCoreScheduler { + fn default() -> Self { + Self::new() + } +} + impl PerCoreScheduler { - pub const fn new(core: CoreId) -> Self { + pub const fn new() -> Self { Self { - core, queue: PriorityQueue::new(), current: None, } } - pub fn core(&self) -> CoreId { - self.core - } - pub fn current(&self) -> Option { self.current } diff --git a/crates/domain/src/scheduler/tests.rs b/crates/domain/src/scheduler/tests.rs index a200a44..e8ec4a9 100644 --- a/crates/domain/src/scheduler/tests.rs +++ b/crates/domain/src/scheduler/tests.rs @@ -99,13 +99,13 @@ fn drain_all_priorities() { #[test] fn new_core_has_no_current() { - let core = PerCoreScheduler::new(CoreId::from_raw(0)); + let core = PerCoreScheduler::new(); assert!(core.current().is_none()); } #[test] fn pick_next_sets_current() { - let mut core = PerCoreScheduler::new(CoreId::from_raw(0)); + let mut core = PerCoreScheduler::new(); core.add(thread(1), prio(10)); let picked = core.pick_next().unwrap(); @@ -115,13 +115,13 @@ fn pick_next_sets_current() { #[test] fn pick_next_on_empty_returns_none() { - let mut core = PerCoreScheduler::new(CoreId::from_raw(0)); + let mut core = PerCoreScheduler::new(); assert!(core.pick_next().is_none()); } #[test] fn clear_current() { - let mut core = PerCoreScheduler::new(CoreId::from_raw(0)); + let mut core = PerCoreScheduler::new(); core.add(thread(1), prio(10)); core.pick_next(); diff --git a/crates/domain/src/slot.rs b/crates/domain/src/slot.rs new file mode 100644 index 0000000..b801854 --- /dev/null +++ b/crates/domain/src/slot.rs @@ -0,0 +1,144 @@ +//! A table entry that is empty or holds a value, like `Option`, but whose +//! empty state is guaranteed to be all zero bytes. The kernel's tables are +//! one static; if every empty entry is zero, the whole static starts zero +//! and costs nothing in the kernel image (`.bss`). `Option` makes no such +//! promise (its `None` is whatever the compiler picks). + +/// `#[repr(u8)]` fixes the layout: a tag byte, `Empty` being 0, then the +/// value (left uninitialised when empty). +#[cfg(not(kani))] +#[repr(u8)] +#[derive(Debug, Clone, Copy, PartialEq, Eq, Default)] +pub enum Slot { + #[default] + Empty = 0, + Full(T) = 1, +} + +/// For the proofs, the same behaviour over `Option`: only the byte layout +/// differs, which no proof depends on, and CBMC is far faster on `Option` +/// than on an enum with an uninitialised payload. +#[cfg(kani)] +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub struct Slot(Option); + +#[cfg(kani)] +impl Default for Slot { + fn default() -> Self { + Self(None) + } +} + +#[cfg(kani)] +#[allow(non_upper_case_globals, non_snake_case)] +impl Slot { + pub const Empty: Self = Self(None); + + pub const fn Full(value: T) -> Self { + Self(Some(value)) + } + + pub const fn is_full(&self) -> bool { + self.0.is_some() + } + + pub const fn as_ref(&self) -> Option<&T> { + self.0.as_ref() + } + + pub fn as_mut(&mut self) -> Option<&mut T> { + self.0.as_mut() + } + + pub fn take(&mut self) -> Option { + self.0.take() + } + + pub fn set(&mut self, value: T) { + self.0 = Some(value); + } +} + +#[cfg(kani)] +impl Slot { + pub const fn get(&self) -> Option { + self.0 + } +} + +#[cfg(kani)] +impl From> for Slot { + fn from(o: Option) -> Self { + Self(o) + } +} + +#[cfg(not(kani))] +impl Slot { + pub const fn is_full(&self) -> bool { + matches!(self, Slot::Full(_)) + } + + pub const fn as_ref(&self) -> Option<&T> { + match self { + Slot::Full(v) => Some(v), + Slot::Empty => None, + } + } + + pub fn as_mut(&mut self) -> Option<&mut T> { + match self { + Slot::Full(v) => Some(v), + Slot::Empty => None, + } + } + + /// The value, leaving the slot empty. + pub fn take(&mut self) -> Option { + match core::mem::replace(self, Slot::Empty) { + Slot::Full(v) => Some(v), + Slot::Empty => None, + } + } + + pub fn set(&mut self, value: T) { + *self = Slot::Full(value); + } +} + +#[cfg(not(kani))] +impl Slot { + pub const fn get(&self) -> Option { + match self { + Slot::Full(v) => Some(*v), + Slot::Empty => None, + } + } +} + +#[cfg(not(kani))] +impl From> for Slot { + fn from(o: Option) -> Self { + match o { + Some(v) => Slot::Full(v), + None => Slot::Empty, + } + } +} + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn a_slot_behaves_like_an_option() { + let mut s: Slot = Slot::Empty; + assert!(!s.is_full() && s.get().is_none()); + s.set(5); + *s.as_mut().unwrap() += 1; + assert_eq!(s.get(), Some(6)); + assert_eq!(s.take(), Some(6)); + assert_eq!(s, Slot::Empty); + assert_eq!(Slot::from(Some(1)), Slot::Full(1)); + } +} diff --git a/crates/domain/src/thread/table.rs b/crates/domain/src/thread/table.rs index 4f12ca3..76a5045 100644 --- a/crates/domain/src/thread/table.rs +++ b/crates/domain/src/thread/table.rs @@ -13,14 +13,14 @@ use crate::{error::KernelError, generations::SlotGenerations}; pub const MAX_THREADS: usize = if cfg!(kani) { 3 } else { 256 }; pub struct ThreadTable { - threads: [Option; MAX_THREADS], + threads: [crate::slot::Slot; MAX_THREADS], generations: SlotGenerations, } impl ThreadTable { pub const fn new() -> Self { Self { - threads: [const { None }; MAX_THREADS], + threads: [const { crate::slot::Slot::Empty }; MAX_THREADS], generations: SlotGenerations::new(), } } @@ -36,7 +36,7 @@ impl ThreadTable { self.threads .iter() .enumerate() - .position(|(i, t)| t.is_none() && self.generations.is_usable(i)) + .position(|(i, t)| !t.is_full() && self.generations.is_usable(i)) } pub fn spawn( @@ -52,7 +52,7 @@ impl ThreadTable { *self .threads .get_mut(idx) - .ok_or(KernelError::TooManyThreads)? = Some(Thread::new( + .ok_or(KernelError::TooManyThreads)? = crate::slot::Slot::Full(Thread::new( id, process, priority, @@ -76,7 +76,7 @@ impl ThreadTable { *self .threads .get_mut(idx) - .ok_or(KernelError::TooManyThreads)? = Some(Thread::with_context( + .ok_or(KernelError::TooManyThreads)? = crate::slot::Slot::Full(Thread::with_context( id, process, priority, diff --git a/crates/kernel/src/lib.rs b/crates/kernel/src/lib.rs index 4be9f53..f2c981d 100644 --- a/crates/kernel/src/lib.rs +++ b/crates/kernel/src/lib.rs @@ -71,7 +71,7 @@ pub struct Kernel { irqs: IrqRoutingTable, notifications: NotificationTable, ipc: [syscall::IpcState; MAX_THREADS], - pending_results: [Option; MAX_THREADS], + pending_results: [domain::slot::Slot; MAX_THREADS], /// The core each thread runs on (see smp.rs). homes: [types::id::CoreId; MAX_THREADS], /// The capability derivation tree as links (see captree.rs). @@ -111,7 +111,7 @@ impl Kernel

{ irqs: IrqRoutingTable::new(), notifications: NotificationTable::new(), ipc: [syscall::IpcState::EMPTY; MAX_THREADS], - pending_results: [const { None }; MAX_THREADS], + pending_results: [const { domain::slot::Slot::Empty }; MAX_THREADS], homes: [types::id::CoreId::from_raw(0); MAX_THREADS], tree: domain::capability::tree::CapTree::new(), heap_cursors: [0; MAX_PROCESSES], @@ -127,6 +127,12 @@ impl Kernel

{ self.platform = platform; } + /// Hands over the user pool, for a kernel placed without one (so its + /// static is all zero, see the adapter); before anything is allocated. + pub fn install_pool(&mut self, pool_base: PhysicalAddress, pool_pages: usize) { + self.frames.set_pool(pool_base, pool_pages); + } + pub fn boot( &mut self, priority: Priority, diff --git a/crates/kernel/src/syscall/ipc/endpoint.rs b/crates/kernel/src/syscall/ipc/endpoint.rs index 7bee6ba..ff0da08 100644 --- a/crates/kernel/src/syscall/ipc/endpoint.rs +++ b/crates/kernel/src/syscall/ipc/endpoint.rs @@ -148,7 +148,7 @@ impl Kernel

{ return SyscallOutcome::Complete(SyscallResult::Error(KernelError::EndpointFull)); } if let Some(s) = self.ipc_mut(tid) { - s.outgoing = Some(out); + s.outgoing.set(out); } let reason = if is_call { BlockReason::Calling(ep) diff --git a/crates/kernel/src/syscall/ipc/mod.rs b/crates/kernel/src/syscall/ipc/mod.rs index e77bb5c..5e746e2 100644 --- a/crates/kernel/src/syscall/ipc/mod.rs +++ b/crates/kernel/src/syscall/ipc/mod.rs @@ -42,7 +42,7 @@ pub(crate) struct Outgoing { /// Per-thread IPC bookkeeping. #[derive(Debug, Clone, Copy, Default)] pub struct IpcState { - pub(crate) outgoing: Option, + pub(crate) outgoing: domain::slot::Slot, /// The caller this thread owes a reply to. pub(crate) reply_to: Option, /// Callers it kept to answer later (`SaveReply`). @@ -55,7 +55,7 @@ pub(crate) const SAVED: usize = types::bounded::SavedReply::MAX as usize + 1; impl IpcState { pub const EMPTY: Self = Self { - outgoing: None, + outgoing: domain::slot::Slot::Empty, reply_to: None, saved: [None; SAVED], bound: None, @@ -73,7 +73,7 @@ impl Kernel

{ pub(crate) fn set_pending_result(&mut self, tid: ThreadId, result: Option) { if let Some(r) = self.pending_results.get_mut(tid.raw() as usize) { - *r = result; + *r = result.into(); } } diff --git a/crates/kernel/src/teardown.rs b/crates/kernel/src/teardown.rs index a655521..773a2a3 100644 --- a/crates/kernel/src/teardown.rs +++ b/crates/kernel/src/teardown.rs @@ -126,7 +126,7 @@ impl Kernel

{ /// dropping whatever it was about to send. fn wake_with_error(&mut self, tid: ThreadId, error: KernelError) { if let Some(s) = self.ipc_mut(tid) { - s.outgoing = None; + s.outgoing = domain::slot::Slot::Empty; } self.wake(tid, SyscallResult::Error(error)); } diff --git a/crates/kernel/src/tests/ipc_invariants.rs b/crates/kernel/src/tests/ipc_invariants.rs index 667ece6..e312ffd 100644 --- a/crates/kernel/src/tests/ipc_invariants.rs +++ b/crates/kernel/src/tests/ipc_invariants.rs @@ -256,7 +256,7 @@ impl World { "{t:?} blocked sending but not queued" ); assert!( - ipc.outgoing.is_some(), + ipc.outgoing.is_full(), "{t:?} queued sender without a message" ); } @@ -287,7 +287,7 @@ impl World { } ThreadState::Ready | ThreadState::Running(_) | ThreadState::Dead => { assert!(!in_any_queue, "{t:?} runnable but queued on an IPC object"); - assert!(ipc.outgoing.is_none()); + assert!(!ipc.outgoing.is_full()); } } let blocked = matches!(state, ThreadState::Blocked(_)); diff --git a/crates/kernel/src/tests/storm.rs b/crates/kernel/src/tests/storm.rs index 6bf9993..73ba9d3 100644 --- a/crates/kernel/src/tests/storm.rs +++ b/crates/kernel/src/tests/storm.rs @@ -194,7 +194,7 @@ impl Kernel { }; match state { ThreadState::Blocked(BlockReason::Sending(e) | BlockReason::Calling(e)) => { - if in_endpoint(e) != Some((true, false)) || ipc.outgoing.is_none() { + if in_endpoint(e) != Some((true, false)) || !ipc.outgoing.is_full() { return Err(format!("{t:?} blocked sending but not queued")); } } @@ -225,7 +225,7 @@ impl Kernel { } } _ => { - if ipc.outgoing.is_some() { + if ipc.outgoing.is_full() { return Err(format!("{t:?} runnable with a queued message")); } }