From 95dbe7b9d5daab23a93f3c618e5f5bcef161e371 Mon Sep 17 00:00:00 2001 From: Gabriel Kaszewski Date: Tue, 27 Oct 2026 13:21:53 +0100 Subject: [PATCH] refactor(kernel): split ipc/memory/lib/thread by concern; trim comments --- crates/domain/src/capability/derivation.rs | 9 +- crates/domain/src/capability/mod.rs | 4 +- crates/domain/src/capability/tree.rs | 14 +- crates/domain/src/endpoint/wait_queue.rs | 4 +- crates/domain/src/generations.rs | 4 +- crates/domain/src/memory/frame/mod.rs | 9 +- crates/domain/src/scheduler/priority_queue.rs | 4 +- crates/domain/src/thread/context.rs | 51 ++ crates/domain/src/thread/mod.rs | 185 +------ crates/domain/src/thread/table.rs | 137 +++++ crates/kernel/src/abi.rs | 4 +- crates/kernel/src/board.rs | 16 +- crates/kernel/src/captree.rs | 13 +- crates/kernel/src/lib.rs | 126 +---- crates/kernel/src/memory.rs | 521 ------------------ crates/kernel/src/memory/mod.rs | 214 +++++++ crates/kernel/src/memory/pages.rs | 138 +++++ crates/kernel/src/memory/region.rs | 201 +++++++ crates/kernel/src/proofs/authority.rs | 15 +- crates/kernel/src/smp.rs | 14 +- .../src/syscall/{ipc.rs => ipc/endpoint.rs} | 282 +--------- crates/kernel/src/syscall/ipc/irq.rs | 67 +++ crates/kernel/src/syscall/ipc/mod.rs | 109 ++++ crates/kernel/src/syscall/ipc/notification.rs | 133 +++++ crates/kernel/src/syscall/memory.rs | 12 +- crates/kernel/src/teardown.rs | 126 +++++ crates/kernel/src/tests/bench.rs | 4 +- crates/kernel/src/tests/captree_model.rs | 6 +- crates/kernel/src/tests/ipc_invariants.rs | 7 +- crates/kernel/src/tests/storm.rs | 16 +- crates/platform/src/lib.rs | 8 +- crates/types/src/badge.rs | 4 +- crates/types/src/bootinfo.rs | 9 +- crates/types/src/proofs/generation.rs | 4 +- 34 files changed, 1239 insertions(+), 1231 deletions(-) create mode 100644 crates/domain/src/thread/context.rs create mode 100644 crates/domain/src/thread/table.rs delete mode 100644 crates/kernel/src/memory.rs create mode 100644 crates/kernel/src/memory/mod.rs create mode 100644 crates/kernel/src/memory/pages.rs create mode 100644 crates/kernel/src/memory/region.rs rename crates/kernel/src/syscall/{ipc.rs => ipc/endpoint.rs} (51%) create mode 100644 crates/kernel/src/syscall/ipc/irq.rs create mode 100644 crates/kernel/src/syscall/ipc/mod.rs create mode 100644 crates/kernel/src/syscall/ipc/notification.rs create mode 100644 crates/kernel/src/teardown.rs diff --git a/crates/domain/src/capability/derivation.rs b/crates/domain/src/capability/derivation.rs index a4d53b6..49c7c86 100644 --- a/crates/domain/src/capability/derivation.rs +++ b/crates/domain/src/capability/derivation.rs @@ -2,10 +2,7 @@ //! capability is a node with at most one parent. Kept free of kernel //! types so the revocation rule can be checked on its own. -/// `result[i]` is true iff `root` is `i` or an ancestor of `i`. -/// -/// `parents` must be acyclic, which holds because a capability's parent -/// always exists before it does. +/// `result[i]` is true iff `root` is `i` or an ancestor of `i`. `parents` must be acyclic. pub fn descendants(parents: &[Option; N], root: usize) -> [bool; N] { let mut marked = [false; N]; let Some(r) = marked.get_mut(root) else { @@ -57,9 +54,7 @@ mod proofs { false } - /// On every acyclic forest of `N` capabilities, `descendants` marks - /// exactly the nodes `root` is an ancestor of: revocation removes the - /// whole subtree and nothing else. + /// On every acyclic forest, `descendants` marks exactly the subtree under `root`. #[kani::proof] #[kani::unwind(6)] fn marks_exactly_the_subtree() { diff --git a/crates/domain/src/capability/mod.rs b/crates/domain/src/capability/mod.rs index b6c656b..5e46968 100644 --- a/crates/domain/src/capability/mod.rs +++ b/crates/domain/src/capability/mod.rs @@ -24,9 +24,7 @@ mod tests; // Sized so that every representable `CapSlot` indexes a real slot. pub const MAX_CAPS_PER_PROCESS: usize = CapSlot::MAX as usize + 1; -/// Names one capability slot at one point in time. Both generations must -/// still match for the reference to resolve, so a reused pid or slot is -/// never mistaken for the capability that used to live there. +/// One capability slot at one point in time; both generations must match to resolve. #[derive(Debug, Clone, Copy, PartialEq, Eq)] pub struct CapRef { pub process: ProcessId, diff --git a/crates/domain/src/capability/tree.rs b/crates/domain/src/capability/tree.rs index 952c5f5..66ea570 100644 --- a/crates/domain/src/capability/tree.rs +++ b/crates/domain/src/capability/tree.rs @@ -1,11 +1,5 @@ -//! The capability derivation tree with explicit links, so deleting a -//! capability costs its number of children and revoking costs the size of -//! the subtree, instead of a scan of every capability in the system. -//! -//! Nodes are numbered `0..N` (the kernel flattens process and slot). Each -//! live node knows its parent, its first child and its siblings. The -//! fixpoint in `derivation::descendants` stays as the reference this tree -//! is checked against. +//! Derivation tree with explicit links: delete costs its children, revoke its subtree. +//! Nodes are `0..N`; `derivation::descendants` is the reference model it is checked against. /// Longest walk any operation may take: every node visited once, plus the /// climb back up. Corrupted links can therefore never hang the kernel. @@ -59,9 +53,7 @@ impl CapTree { self.node(i)?.parent.map(usize::from) } - /// Adds `i` as a child of `parent` (or as a root). Fails, changing - /// nothing, if `i` is already live or out of range, or `parent` is not - /// live. + /// Adds `i` under `parent` (or as a root); fails without change if `i` is live or out of range, or `parent` is not live. pub fn attach(&mut self, i: usize, parent: Option) -> bool { let (Some(me), Some(node)) = (id(i), self.nodes.get(i)) else { return false; diff --git a/crates/domain/src/endpoint/wait_queue.rs b/crates/domain/src/endpoint/wait_queue.rs index 7861ad5..2f34057 100644 --- a/crates/domain/src/endpoint/wait_queue.rs +++ b/crates/domain/src/endpoint/wait_queue.rs @@ -85,9 +85,7 @@ impl Default for WaitQueue { mod proofs { use super::*; - /// Against a simple reference model (a plain array kept in arrival - /// order), any sequence of pushes, pops and removals behaves the same: - /// FIFO order, no duplicates, nothing lost. + /// Matches a plain arrival-ordered array model: FIFO, no duplicates, nothing lost. #[kani::proof] #[kani::unwind(7)] fn behaves_like_a_fifo_without_duplicates() { diff --git a/crates/domain/src/generations.rs b/crates/domain/src/generations.rs index cd8e26e..de36ef4 100644 --- a/crates/domain/src/generations.rs +++ b/crates/domain/src/generations.rs @@ -6,9 +6,7 @@ use types::generation::Generation; #[path = "generations_tests.rs"] mod tests; -/// A slot's generation changes every time the object in it is destroyed -/// or revoked, so capabilities minted earlier stop matching. A slot whose -/// counter runs out is retired for good rather than reused. +/// 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], } diff --git a/crates/domain/src/memory/frame/mod.rs b/crates/domain/src/memory/frame/mod.rs index 77f44e5..48e1b20 100644 --- a/crates/domain/src/memory/frame/mod.rs +++ b/crates/domain/src/memory/frame/mod.rs @@ -104,9 +104,7 @@ impl FrameTable { self.frames.get(self.index_of(pa)?)?.as_ref() } - /// Next-fit: searches from just past the previous allocation and wraps - /// once, so a run of allocations costs O(1) each instead of rescanning - /// the allocated prefix every time. + /// Next-fit: searches from just past the previous allocation, wrapping once. pub fn alloc(&mut self, usage: FrameUse) -> Option { if self.free == 0 { return None; @@ -177,10 +175,7 @@ impl FrameTable { } } - /// The frame mapped at `va` in `owner`, if `owner` holds it as a user page. - /// The perms of the frame at `pa` if it is `owner`'s user page at - /// `va`; `None` for any other frame. O(1): the caller supplies the - /// frame, this only confirms it. + /// The perms of the frame at `pa` if it is `owner`'s user page at `va`; O(1), the caller supplies the frame. pub fn user_at( &self, pa: PhysicalAddress, diff --git a/crates/domain/src/scheduler/priority_queue.rs b/crates/domain/src/scheduler/priority_queue.rs index d9370f3..40a1b32 100644 --- a/crates/domain/src/scheduler/priority_queue.rs +++ b/crates/domain/src/scheduler/priority_queue.rs @@ -17,9 +17,7 @@ struct ListEnds { tail: Option, } -/// Ready queue: one FIFO per priority level, threaded through an -/// intrusive doubly linked list indexed by thread id. A thread is in at -/// most one list, so capacity never runs out and every op is O(1). +/// Ready queue: one FIFO per priority in an intrusive list indexed by thread id; O(1) ops. pub struct PriorityQueue { lists: [ListEnds; NUM_PRIORITIES], links: [Links; MAX_THREADS], diff --git a/crates/domain/src/thread/context.rs b/crates/domain/src/thread/context.rs new file mode 100644 index 0000000..980c15a --- /dev/null +++ b/crates/domain/src/thread/context.rs @@ -0,0 +1,51 @@ +//! Saved register state of a thread. + +pub struct SavedContext { + registers: [usize; 32], + pc: usize, + status: usize, +} + +impl SavedContext { + pub fn empty() -> Self { + Self { + registers: [0; 32], + pc: 0, + status: 0, + } + } + + pub fn with_entry_and_stack( + entry: types::address::EntryPoint, + stack: types::address::StackPointer, + ) -> Self { + let mut ctx = Self::empty(); + ctx.pc = entry.raw(); + ctx.registers[2] = stack.raw(); + ctx + } + + pub fn program_counter(&self) -> usize { + self.pc + } + + pub fn set_pc(&mut self, pc: usize) { + self.pc = pc; + } + + pub fn status(&self) -> usize { + self.status + } + + pub fn set_status(&mut self, status: usize) { + self.status = status; + } + + pub fn registers(&self) -> &[usize; 32] { + &self.registers + } + + pub fn registers_mut(&mut self) -> &mut [usize; 32] { + &mut self.registers + } +} diff --git a/crates/domain/src/thread/mod.rs b/crates/domain/src/thread/mod.rs index 79676ba..b7ff270 100644 --- a/crates/domain/src/thread/mod.rs +++ b/crates/domain/src/thread/mod.rs @@ -1,11 +1,16 @@ use types::{ bounded::Priority, - generation::Generation, id::{CoreId, EndpointId, NotificationId, ProcessId, ThreadId}, time::TimeSlice, }; -use crate::{error::KernelError, generations::SlotGenerations}; +use crate::error::KernelError; + +mod context; +mod table; + +pub use context::SavedContext; +pub use table::{MAX_THREADS, ThreadTable}; #[cfg(test)] #[path = "tests.rs"] @@ -29,56 +34,6 @@ pub enum ThreadState { Dead, } -pub struct SavedContext { - registers: [usize; 32], - pc: usize, - status: usize, -} - -impl SavedContext { - pub fn empty() -> Self { - Self { - registers: [0; 32], - pc: 0, - status: 0, - } - } - - pub fn with_entry_and_stack( - entry: types::address::EntryPoint, - stack: types::address::StackPointer, - ) -> Self { - let mut ctx = Self::empty(); - ctx.pc = entry.raw(); - ctx.registers[2] = stack.raw(); - ctx - } - - pub fn program_counter(&self) -> usize { - self.pc - } - - pub fn set_pc(&mut self, pc: usize) { - self.pc = pc; - } - - pub fn status(&self) -> usize { - self.status - } - - pub fn set_status(&mut self, status: usize) { - self.status = status; - } - - pub fn registers(&self) -> &[usize; 32] { - &self.registers - } - - pub fn registers_mut(&mut self) -> &mut [usize; 32] { - &mut self.registers - } -} - #[derive(Debug, Clone, Copy, PartialEq, Eq)] pub enum BlockReason { /// Queued as a sender on the endpoint. @@ -228,129 +183,3 @@ impl Thread { } } } - -pub const MAX_THREADS: usize = if cfg!(kani) { 3 } else { 256 }; - -pub struct ThreadTable { - threads: [Option; MAX_THREADS], - generations: SlotGenerations, -} - -impl ThreadTable { - pub fn new() -> Self { - Self { - threads: [const { None }; MAX_THREADS], - generations: SlotGenerations::new(), - } - } - - /// Current generation of a live thread, so references to it (reply - /// slots) can detect that the id was reused. - pub fn generation(&self, id: ThreadId) -> Option { - self.get(id).ok()?; - self.generations.current(id.raw() as usize) - } - - fn free_slot(&self) -> Option { - self.threads - .iter() - .enumerate() - .position(|(i, t)| t.is_none() && self.generations.is_usable(i)) - } - - pub fn spawn( - &mut self, - process: ProcessId, - priority: Priority, - time_slice: TimeSlice, - core_affinity: Option, - ) -> Result { - let idx = self.free_slot().ok_or(KernelError::TooManyThreads)?; - - let id = ThreadId::from_raw(idx as u16); - *self - .threads - .get_mut(idx) - .ok_or(KernelError::TooManyThreads)? = Some(Thread::new( - id, - process, - priority, - time_slice, - core_affinity, - )); - Ok(id) - } - - pub fn spawn_with_context( - &mut self, - process: ProcessId, - priority: Priority, - time_slice: TimeSlice, - core_affinity: Option, - context: SavedContext, - ) -> Result { - let idx = self.free_slot().ok_or(KernelError::TooManyThreads)?; - - let id = ThreadId::from_raw(idx as u16); - *self - .threads - .get_mut(idx) - .ok_or(KernelError::TooManyThreads)? = Some(Thread::with_context( - id, - process, - priority, - time_slice, - core_affinity, - context, - )); - Ok(id) - } - - /// Every live thread with its id. - pub fn iter(&self) -> impl Iterator { - self.threads - .iter() - .enumerate() - .filter_map(|(i, t)| Some((ThreadId::from_raw(i as u16), t.as_ref()?))) - } - - pub fn get(&self, id: ThreadId) -> Result<&Thread, KernelError> { - let idx = id.raw() as usize; - self.threads - .get(idx) - .and_then(|s| s.as_ref()) - .ok_or(KernelError::InvalidThread(id)) - } - - pub fn get_mut(&mut self, id: ThreadId) -> Result<&mut Thread, KernelError> { - let idx = id.raw() as usize; - self.threads - .get_mut(idx) - .and_then(|s| s.as_mut()) - .ok_or(KernelError::InvalidThread(id)) - } - - pub fn destroy(&mut self, id: ThreadId) -> Result { - let idx = id.raw() as usize; - let thread = self - .threads - .get_mut(idx) - .and_then(|s| s.take()) - .ok_or(KernelError::InvalidThread(id))?; - self.generations.advance(idx); - Ok(thread) - } - - pub fn threads_for_process(&self, process: ProcessId) -> impl Iterator { - self.threads - .iter() - .filter_map(|s| s.as_ref()) - .filter(move |t| t.process() == process) - } -} - -impl Default for ThreadTable { - fn default() -> Self { - Self::new() - } -} diff --git a/crates/domain/src/thread/table.rs b/crates/domain/src/thread/table.rs new file mode 100644 index 0000000..569e36f --- /dev/null +++ b/crates/domain/src/thread/table.rs @@ -0,0 +1,137 @@ +//! Fixed-capacity table of threads. + +use types::{ + bounded::Priority, + generation::Generation, + id::{CoreId, ProcessId, ThreadId}, + time::TimeSlice, +}; + +use super::{SavedContext, Thread}; +use crate::{error::KernelError, generations::SlotGenerations}; + +pub const MAX_THREADS: usize = if cfg!(kani) { 3 } else { 256 }; + +pub struct ThreadTable { + threads: [Option; MAX_THREADS], + generations: SlotGenerations, +} + +impl ThreadTable { + pub fn new() -> Self { + Self { + threads: [const { None }; MAX_THREADS], + generations: SlotGenerations::new(), + } + } + + /// Current generation of a live thread, so references to it (reply + /// slots) can detect that the id was reused. + pub fn generation(&self, id: ThreadId) -> Option { + self.get(id).ok()?; + self.generations.current(id.raw() as usize) + } + + fn free_slot(&self) -> Option { + self.threads + .iter() + .enumerate() + .position(|(i, t)| t.is_none() && self.generations.is_usable(i)) + } + + pub fn spawn( + &mut self, + process: ProcessId, + priority: Priority, + time_slice: TimeSlice, + core_affinity: Option, + ) -> Result { + let idx = self.free_slot().ok_or(KernelError::TooManyThreads)?; + + let id = ThreadId::from_raw(idx as u16); + *self + .threads + .get_mut(idx) + .ok_or(KernelError::TooManyThreads)? = Some(Thread::new( + id, + process, + priority, + time_slice, + core_affinity, + )); + Ok(id) + } + + pub fn spawn_with_context( + &mut self, + process: ProcessId, + priority: Priority, + time_slice: TimeSlice, + core_affinity: Option, + context: SavedContext, + ) -> Result { + let idx = self.free_slot().ok_or(KernelError::TooManyThreads)?; + + let id = ThreadId::from_raw(idx as u16); + *self + .threads + .get_mut(idx) + .ok_or(KernelError::TooManyThreads)? = Some(Thread::with_context( + id, + process, + priority, + time_slice, + core_affinity, + context, + )); + Ok(id) + } + + /// Every live thread with its id. + pub fn iter(&self) -> impl Iterator { + self.threads + .iter() + .enumerate() + .filter_map(|(i, t)| Some((ThreadId::from_raw(i as u16), t.as_ref()?))) + } + + pub fn get(&self, id: ThreadId) -> Result<&Thread, KernelError> { + let idx = id.raw() as usize; + self.threads + .get(idx) + .and_then(|s| s.as_ref()) + .ok_or(KernelError::InvalidThread(id)) + } + + pub fn get_mut(&mut self, id: ThreadId) -> Result<&mut Thread, KernelError> { + let idx = id.raw() as usize; + self.threads + .get_mut(idx) + .and_then(|s| s.as_mut()) + .ok_or(KernelError::InvalidThread(id)) + } + + pub fn destroy(&mut self, id: ThreadId) -> Result { + let idx = id.raw() as usize; + let thread = self + .threads + .get_mut(idx) + .and_then(|s| s.take()) + .ok_or(KernelError::InvalidThread(id))?; + self.generations.advance(idx); + Ok(thread) + } + + pub fn threads_for_process(&self, process: ProcessId) -> impl Iterator { + self.threads + .iter() + .filter_map(|s| s.as_ref()) + .filter(move |t| t.process() == process) + } +} + +impl Default for ThreadTable { + fn default() -> Self { + Self::new() + } +} diff --git a/crates/kernel/src/abi.rs b/crates/kernel/src/abi.rs index 1b293dc..1a83b5e 100644 --- a/crates/kernel/src/abi.rs +++ b/crates/kernel/src/abi.rs @@ -34,9 +34,7 @@ fn message(a: &[usize; 6]) -> Option { }) } -/// Decodes syscall `nr` with arguments `a0..a5`. `None` for an unknown -/// number or an argument with no meaning (e.g. a slot out of range); the -/// caller then gets `UnknownSyscall` and nothing else happens. +/// Decodes syscall `nr` with args `a0..a5`; `None` for an unknown number or meaningless argument. pub fn decode(nr: usize, a: &[usize; 6]) -> Option { Some(match nr { SYS_EXIT => Syscall::Exit, diff --git a/crates/kernel/src/board.rs b/crates/kernel/src/board.rs index 6768ebd..5699c2c 100644 --- a/crates/kernel/src/board.rs +++ b/crates/kernel/src/board.rs @@ -1,7 +1,4 @@ -//! The authority init starts with. The board describes its devices; the -//! kernel turns each into capabilities (an MMIO region and an IRQ line) -//! and adds one SystemControl capability. Init then decides who gets what; -//! nothing else is privileged by its process id. +//! The authority init starts with: per-device MMIO and IRQ capabilities plus one SystemControl. use domain::{error::KernelError, resource::Resource}; use platform::Platform; @@ -31,9 +28,7 @@ pub struct BoardCaps { } impl Kernel

{ - /// Creates one device region per board device, owned by `init`. Fails - /// on the first device that is misaligned, overlaps the frame pool or - /// another device, or names an IRQ the kernel cannot route. + /// Creates one device region per board device, owned by `init`; fails on the first invalid one. pub fn register_board( &mut self, init: ProcessId, @@ -50,11 +45,8 @@ impl Kernel

{ Ok(()) } - /// Gives `init` a capability to every registered device's region and - /// IRQ line, then one SystemControl capability. All carry Delegate so - /// init can hand them on. Writes where each device's caps went into - /// `placed` (one entry per device, in order) and returns the - /// SystemControl slot, so boot can tell init. + /// Gives `init` (with Delegate) caps to every device region and IRQ, then SystemControl. + /// Writes each device's slots into `placed` in order; returns the SystemControl slot. pub fn grant_boot_authority( &mut self, init: ProcessId, diff --git a/crates/kernel/src/captree.rs b/crates/kernel/src/captree.rs index f7e773c..ea86ef5 100644 --- a/crates/kernel/src/captree.rs +++ b/crates/kernel/src/captree.rs @@ -1,13 +1,6 @@ -//! The capability derivation tree. Every derived capability (Mint, -//! Delegate, IPC transfer) records its parent; `Revoke` deletes a subtree -//! and deleting a capability re-parents its children, so the tree can only -//! shrink by explicit deletion, never by a middleman stepping out. -//! -//! Each capability records its parent (`Capability::parent`), and -//! `Kernel::tree` holds the same relation as explicit links, so deletion -//! and revocation cost the subtree, not a scan of every capability. Every -//! insertion and removal of a capability goes through this module, which -//! keeps the two in step. +//! Derivation tree: every derived capability records its parent; `Revoke` deletes a subtree, +//! deleting re-parents children. All capability insertion/removal goes through here so +//! `Capability::parent` and `Kernel::tree` stay in step. use domain::{ capability::{CapRef, Capability, MAX_CAPS_PER_PROCESS}, diff --git a/crates/kernel/src/lib.rs b/crates/kernel/src/lib.rs index 0e8ae8d..bf23e29 100644 --- a/crates/kernel/src/lib.rs +++ b/crates/kernel/src/lib.rs @@ -23,6 +23,7 @@ mod memory; pub mod proofs; mod smp; pub mod syscall; +mod teardown; pub use board::{BoardCaps, BoardDevice}; pub use syscall::{SyscallOutcome, SyscallResult}; @@ -37,7 +38,7 @@ use domain::{ error::KernelError, irq::IrqRoutingTable, memory::{RegionTable, frame::FrameTable, quota::Quota}, - notification::{MAX_NOTIFICATIONS, NotificationTable}, + notification::NotificationTable, process::{MAX_PROCESSES, ProcessTable}, resource::Resource, scheduler::{Scheduler, multi_core::MultiCoreScheduler}, @@ -96,12 +97,10 @@ impl Kernel

{ } } - /// Builds the kernel directly in `slot`, one table at a time, so the - /// whole structure never has to fit on the (small) boot stack. + /// Builds the kernel in place, one table at a time, to stay off the boot stack. /// /// # Safety - /// `slot` must be valid for writes and properly aligned. Any previous - /// value is overwritten without being dropped. + /// `slot` must be valid for writes and aligned; the old value is overwritten without drop. pub unsafe fn init_in_place( slot: *mut Self, platform: P, @@ -263,123 +262,6 @@ impl Kernel

{ } } - pub(crate) fn destroy_process(&mut self, pid: ProcessId) { - use domain::process::MAX_THREADS_PER_PROCESS; - - let thread_ids: [Option; MAX_THREADS_PER_PROCESS] = match self.processes.get(pid) - { - Ok(p) => { - let mut ids = [None; MAX_THREADS_PER_PROCESS]; - for (slot, tid) in ids.iter_mut().zip(p.thread_ids()) { - *slot = Some(tid); - } - ids - } - Err(_) => return, - }; - - self.cleanup_threads(&thread_ids); - self.delete_all_caps(pid); - self.destroy_endpoints_owned_by(pid); - self.destroy_notifications_owned_by(pid); - self.teardown_memory(pid); - - let _ = self.processes.destroy(pid); - } - - pub(crate) fn cleanup_threads(&mut self, thread_ids: &[Option]) { - use domain::scheduler::Scheduler; - for tid in thread_ids.iter().flatten() { - self.leave_queue(*tid); - if let Some(n) = self - .ipc(*tid) - .and_then(|s| s.bound) - .and_then(|n| self.notifications.get_mut(n)) - { - n.remove_thread(*tid); - } - let ipc = self.ipc_mut(*tid).map(core::mem::take).unwrap_or_default(); - if let Some(caller) = ipc.reply_to { - self.release_caller(caller); - } - self.evict(*tid); - self.scheduler.remove(*tid); - self.set_pending_result(*tid, None); - let _ = self.threads.destroy(*tid); - } - } - - /// Takes a blocked thread off the one queue its block reason names, so - /// nothing needs to scan every endpoint and notification. - pub(crate) fn leave_queue(&mut self, tid: ThreadId) { - use domain::thread::BlockReason::*; - let Ok(ThreadState::Blocked(reason)) = self.threads.get(tid).map(|t| *t.state()) else { - return; - }; - match reason { - Sending(ep) | Calling(ep) => { - self.endpoints.get_mut(ep).map(|e| e.remove_sender(tid)); - } - Receiving(ep) => { - self.endpoints.get_mut(ep).map(|e| e.remove_receiver(tid)); - } - WaitingNotification(n) => { - if let Some(n) = self.notifications.get_mut(n) { - n.remove_waiter(tid); - } - } - AwaitingReply => {} - } - } - - /// Destroys every endpoint `owner` created, waking anyone blocked on - /// them with an error instead of leaving them blocked forever. - pub(crate) fn destroy_endpoints_owned_by(&mut self, owner: ProcessId) { - let mut owned = [None; domain::endpoint::MAX_ENDPOINTS]; - for (slot, id) in owned.iter_mut().zip(self.endpoints.ids_owned_by(owner)) { - *slot = Some(id); - } - for id in owned.into_iter().flatten() { - let Some(mut ep) = self.endpoints.destroy(id) else { - continue; - }; - while let Some(tid) = ep.dequeue_sender().or_else(|| ep.dequeue_receiver()) { - self.wake_with_error(tid, KernelError::InvalidEndpoint(id)); - } - } - } - - /// Destroys every notification `owner` created, waking its waiters - /// with an error and unbinding its bound thread. - pub(crate) fn destroy_notifications_owned_by(&mut self, owner: ProcessId) { - let mut owned = [None; MAX_NOTIFICATIONS]; - for (slot, id) in owned.iter_mut().zip(self.notifications.ids_owned_by(owner)) { - *slot = Some(id); - } - for id in owned.into_iter().flatten() { - let Some(mut n) = self.notifications.destroy(id) else { - continue; - }; - if let Some(bound) = n.bound() - && let Some(s) = self.ipc_mut(bound) - { - s.bound = None; - } - while let Some(tid) = n.pop_waiter() { - self.wake_with_error(tid, KernelError::NoSuchObject); - } - } - } - - /// Makes a blocked thread runnable with `error` as its syscall result, - /// 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; - } - self.wake(tid, SyscallResult::Error(error)); - } - fn check_cap( &self, owner: ProcessId, diff --git a/crates/kernel/src/memory.rs b/crates/kernel/src/memory.rs deleted file mode 100644 index 80b9056..0000000 --- a/crates/kernel/src/memory.rs +++ /dev/null @@ -1,521 +0,0 @@ -//! Address-space bookkeeping. The kernel decides every user mapping from -//! its own records (`FrameTable`, `RegionTable`, quotas) and only then tells -//! the platform to apply it; it never asks the hardware what is mapped. - -use domain::{ - error::KernelError, - memory::{ - Region, RegionBacking, RegionMapping, - frame::{FrameTable, FrameUse, PAGE_SIZE}, - quota::Quota, - }, -}; -use platform::{FrameSource, MapError, Platform}; -use types::{ - address::{PhysicalAddress, VirtualAddress}, - bounded::PageCount, - id::{ProcessId, RegionId}, - mapping::PagePerms, -}; - -use crate::Kernel; - -/// First VA the kernel considers when picking a spot for `RequestPages`. -/// Below it sit the program image and boot-time device windows. -pub(crate) const USER_HEAP_START: usize = 0x40000; - -/// Page-table frames for one address space, charged to its owner. -struct ChargedFrames<'a> { - frames: &'a mut FrameTable, - quota: &'a mut Quota, - owner: ProcessId, -} - -impl FrameSource for ChargedFrames<'_> { - fn alloc_table_frame(&mut self) -> Option { - if !self.quota.charge(1) { - return None; - } - match self.frames.alloc(FrameUse::PageTable { owner: self.owner }) { - Some(pa) => Some(pa), - None => { - self.quota.uncharge(1); - None - } - } - } -} - -fn map_error(e: MapError) -> KernelError { - match e { - MapError::OutOfFrames => KernelError::OutOfMemory, - MapError::InvalidAddress => KernelError::InvalidAddress, - MapError::NoAddressSpace => KernelError::OutOfMemory, - } -} - -impl Kernel

{ - /// Whether `[va, va + pages)` is page aligned and inside the user window. - pub(crate) fn in_user_window(va: VirtualAddress, pages: usize) -> bool { - let start = va.raw(); - let Some(len) = pages.checked_mul(PAGE_SIZE) else { - return false; - }; - let Some(end) = start.checked_add(len) else { - return false; - }; - pages > 0 - && start.is_multiple_of(PAGE_SIZE) - && start >= P::USER_VA_START - && end <= P::USER_VA_END - } - - /// `pid`'s user page at `va`: the platform's page table says where it - /// points, the frame table confirms the frame really is that page. - fn user_frame( - &self, - pid: ProcessId, - va: VirtualAddress, - ) -> Option<(PhysicalAddress, PagePerms)> { - let pa = self.platform.translate(pid, va)?; - self.frames.user_at(pa, pid, va).map(|perms| (pa, perms)) - } - - fn is_mapped(&self, pid: ProcessId, va: VirtualAddress) -> bool { - self.user_frame(pid, va).is_some() || self.regions.covering(pid, va).is_some() - } - - fn range_is_free(&self, pid: ProcessId, va: VirtualAddress, pages: usize) -> bool { - (0..pages).all(|i| !self.is_mapped(pid, page_at(va, i))) - } - - fn quota_mut(&mut self, pid: ProcessId) -> Result<&mut Quota, KernelError> { - self.quotas - .get_mut(pid.raw() as usize) - .ok_or(KernelError::InvalidProcess(pid)) - } - - pub fn page_usage(&self, pid: ProcessId) -> usize { - self.quotas.get(pid.raw() as usize).map_or(0, Quota::used) - } - - pub fn set_page_limit(&mut self, pid: ProcessId, limit: usize) -> Result<(), KernelError> { - self.processes.get(pid)?; - if self.quota_mut(pid)?.set_limit(limit) { - Ok(()) - } else { - Err(KernelError::OutOfMemory) - } - } - - pub fn free_page_count(&self) -> usize { - self.frames.free_count() - } - - /// Maps `pa` at `va` in `pid`, building page tables on `pid`'s quota. - fn platform_map( - &mut self, - pid: ProcessId, - va: VirtualAddress, - pa: PhysicalAddress, - perms: PagePerms, - ) -> Result<(), KernelError> { - let quota = self - .quotas - .get_mut(pid.raw() as usize) - .ok_or(KernelError::InvalidProcess(pid))?; - let mut source = ChargedFrames { - frames: &mut self.frames, - quota, - owner: pid, - }; - self.platform - .map_page(pid, va, pa, perms, &mut source) - .map_err(map_error) - } - - pub(crate) fn create_address_space(&mut self, pid: ProcessId) -> Result<(), KernelError> { - let quota = self - .quotas - .get_mut(pid.raw() as usize) - .ok_or(KernelError::InvalidProcess(pid))?; - *quota = Quota::default(); - let mut source = ChargedFrames { - frames: &mut self.frames, - quota, - owner: pid, - }; - let created = self - .platform - .create_address_space(pid, &mut source) - .map_err(map_error); - if created.is_err() { - self.frames.free_owned_by(pid); - if let Some(q) = self.quotas.get_mut(pid.raw() as usize) { - *q = Quota::default(); - } - } - created - } - - /// Allocates, zeroes and maps one fresh page for `pid` at `va`. - fn map_fresh_page( - &mut self, - pid: ProcessId, - va: VirtualAddress, - perms: PagePerms, - ) -> Result { - let usage = FrameUse::user(pid, va, perms).ok_or(KernelError::InvalidAddress)?; - if !self.quota_mut(pid)?.charge(1) { - return Err(KernelError::OutOfMemory); - } - let Some(pa) = self.frames.alloc(usage) else { - self.quota_mut(pid)?.uncharge(1); - return Err(KernelError::OutOfMemory); - }; - self.platform.zero_frame(pa); - if let Err(e) = self.platform_map(pid, va, pa, perms) { - self.frames.free(pa); - self.quota_mut(pid)?.uncharge(1); - return Err(e); - } - Ok(pa) - } - - /// Removes one user page of `pid` and returns its frame to the pool. - fn unmap_and_free(&mut self, pid: ProcessId, va: VirtualAddress) { - if let Some((pa, _)) = self.user_frame(pid, va) { - self.platform.unmap_page(pid, va); - self.frames.free(pa); - if let Some(q) = self.quotas.get_mut(pid.raw() as usize) { - q.uncharge(1); - } - } - } - - /// Frame backing the user page at `va` in `pid`. Lets boot code fill - /// pages it has just mapped for a process. - pub fn user_page_frame(&self, pid: ProcessId, va: VirtualAddress) -> Option { - self.user_frame(pid, va).map(|(pa, _)| pa) - } - - /// Maps `pages` fresh zeroed pages at `va`, all or nothing. - pub fn map_fresh_range( - &mut self, - pid: ProcessId, - va: VirtualAddress, - pages: usize, - perms: PagePerms, - ) -> Result<(), KernelError> { - if !Self::in_user_window(va, pages) { - return Err(KernelError::InvalidAddress); - } - if !self.range_is_free(pid, va, pages) { - return Err(KernelError::AddressInUse); - } - for i in 0..pages { - if let Err(e) = self.map_fresh_page(pid, page_at(va, i), perms) { - for j in 0..i { - self.unmap_and_free(pid, page_at(va, j)); - } - return Err(e); - } - } - Ok(()) - } - - /// Next-fit search for `pages` free pages in the heap part of the - /// window: from just past `pid`'s previous request, then once more from - /// the bottom. Requests in a row cost O(pages) each instead of - /// rescanning everything allocated before. - pub(crate) fn find_free_heap_range( - &self, - pid: ProcessId, - pages: usize, - ) -> Option { - let bottom = USER_HEAP_START.max(P::USER_VA_START); - let cursor = self - .heap_cursors - .get(pid.raw() as usize) - .copied() - .unwrap_or(0) - .max(bottom); - self.first_fit_from(pid, cursor, pages) - .or_else(|| self.first_fit_from(pid, bottom, pages)) - } - - /// Records where `pid`'s next heap search starts. - pub(crate) fn advance_heap_cursor(&mut self, pid: ProcessId, past: VirtualAddress) { - if let Some(c) = self.heap_cursors.get_mut(pid.raw() as usize) { - *c = past.raw(); - } - } - - fn first_fit_from(&self, pid: ProcessId, from: usize, pages: usize) -> Option { - let mut candidate = from; - while Self::in_user_window(VirtualAddress::from_raw(candidate), pages) { - let va = VirtualAddress::from_raw(candidate); - match (0..pages).find(|&i| self.is_mapped(pid, page_at(va, i))) { - None => return Some(va), - Some(busy) => candidate += (busy + 1) * PAGE_SIZE, - } - } - None - } - - /// Validates that every page of the range is a user page `pid` owns, - /// then releases them all. - pub(crate) fn release_range( - &mut self, - pid: ProcessId, - va: VirtualAddress, - pages: usize, - ) -> Result<(), KernelError> { - if !Self::in_user_window(va, pages) { - return Err(KernelError::InvalidAddress); - } - if !(0..pages).all(|i| self.user_frame(pid, page_at(va, i)).is_some()) { - return Err(KernelError::InvalidAddress); - } - for i in 0..pages { - self.unmap_and_free(pid, page_at(va, i)); - } - Ok(()) - } - - /// Moves the page at `src` in `from` to `dst` in `to`. The frame and its - /// quota charge change hands; `from` loses access. - pub(crate) fn move_page( - &mut self, - from: ProcessId, - src: VirtualAddress, - to: ProcessId, - dst: VirtualAddress, - perms: PagePerms, - ) -> Result<(), KernelError> { - if !Self::in_user_window(src, 1) || !Self::in_user_window(dst, 1) { - return Err(KernelError::InvalidAddress); - } - let (pa, _) = self - .user_frame(from, src) - .ok_or(KernelError::InvalidAddress)?; - self.processes.get(to)?; - if !self.range_is_free(to, dst, 1) { - return Err(KernelError::AddressInUse); - } - let usage = FrameUse::user(to, dst, perms).ok_or(KernelError::InvalidAddress)?; - if !self.quota_mut(to)?.charge(1) { - return Err(KernelError::OutOfMemory); - } - if let Err(e) = self.platform_map(to, dst, pa, perms) { - self.quota_mut(to)?.uncharge(1); - return Err(e); - } - self.platform.unmap_page(from, src); - self.frames.retag(pa, usage); - self.quota_mut(from)?.uncharge(1); - Ok(()) - } - - /// Allocates a physically contiguous, zeroed region charged to `owner`. - pub fn create_pool_region( - &mut self, - owner: ProcessId, - pages: PageCount, - ) -> Result { - self.processes.get(owner)?; - let id = self.regions.next_free_id().ok_or(KernelError::NoFreeSlot)?; - let count = pages.value() as usize; - if !self.quota_mut(owner)?.charge(count) { - return Err(KernelError::OutOfMemory); - } - let Some(base) = self - .frames - .alloc_contiguous(count, |_| FrameUse::Region { region: id }) - else { - self.quota_mut(owner)?.uncharge(count); - return Err(KernelError::OutOfMemory); - }; - for i in 0..count { - self.platform.zero_frame(base.offset(i)); - } - self.regions - .insert(Region::new(owner, RegionBacking::Pool, base, pages)) - .ok_or(KernelError::NoFreeSlot) - } - - /// Describes device memory at `base` so it can be mapped like a region. - pub fn create_device_region( - &mut self, - owner: ProcessId, - base: PhysicalAddress, - pages: PageCount, - ) -> Result { - self.processes.get(owner)?; - if !base.raw().is_multiple_of(PAGE_SIZE) { - return Err(KernelError::InvalidAddress); - } - // Device memory must never alias frames the kernel hands out. - let len = pages.value() as usize * PAGE_SIZE; - let start = base.raw(); - let end = start.checked_add(len).ok_or(KernelError::InvalidAddress)?; - let pool_start = self.frames.base().raw(); - let pool_end = pool_start + self.frames.capacity() * PAGE_SIZE; - if start < pool_end && end > pool_start { - return Err(KernelError::InvalidAddress); - } - // Nor another device's window: each device has one region, so - // revoking or delegating it means the same thing everywhere. - let overlaps = self.regions.iter().any(|(_, r)| { - let r_start = r.base().raw(); - let r_end = r_start.saturating_add(r.pages().value() as usize * PAGE_SIZE); - r.backing() == RegionBacking::Device && start < r_end && end > r_start - }); - if overlaps { - return Err(KernelError::AddressInUse); - } - self.regions - .insert(Region::new(owner, RegionBacking::Device, base, pages)) - .ok_or(KernelError::NoFreeSlot) - } - - pub fn region_base(&self, id: RegionId) -> Option { - self.regions.get(id).map(Region::base) - } - - pub fn region_pages(&self, id: RegionId) -> Option { - self.regions.get(id).map(Region::pages) - } - - /// Maps all of region `id` at `va` in `pid`, all or nothing. - /// Maps region `id` for boot code; the mapping is not tied to any - /// capability and lasts until the region or the process dies. - pub fn map_region( - &mut self, - id: RegionId, - pid: ProcessId, - va: VirtualAddress, - perms: PagePerms, - ) -> Result<(), KernelError> { - self.map_region_via(id, pid, va, perms, None) - } - - /// Maps all of region `id` at `va` in `pid`, all or nothing. A mapping - /// made through a capability (`via`) is removed when that capability - /// is deleted. - pub(crate) fn map_region_via( - &mut self, - id: RegionId, - pid: ProcessId, - va: VirtualAddress, - perms: PagePerms, - via: Option, - ) -> Result<(), KernelError> { - self.processes.get(pid)?; - let region = self.regions.get(id).ok_or(KernelError::InvalidRegion)?; - let (base, pages) = (region.base(), region.pages().value() as usize); - if region.mappings().any(|m| m.process == pid) { - return Err(KernelError::AddressInUse); - } - // W^X holds across processes too: nobody may write what someone - // else can execute. - let clashes = |other: PagePerms| { - matches!( - (perms, other), - (PagePerms::ReadWrite, PagePerms::ReadExecute) - | (PagePerms::ReadExecute, PagePerms::ReadWrite) - ) - }; - if region.mappings().any(|m| clashes(m.perms)) { - return Err(KernelError::WritableAndExecutable); - } - if !Self::in_user_window(va, pages) { - return Err(KernelError::InvalidAddress); - } - if !self.range_is_free(pid, va, pages) { - return Err(KernelError::AddressInUse); - } - for i in 0..pages { - if let Err(e) = self.platform_map(pid, page_at(va, i), base.offset(i), perms) { - for j in 0..i { - self.platform.unmap_page(pid, page_at(va, j)); - } - return Err(e); - } - } - let recorded = self.regions.get_mut(id).is_some_and(|r| { - r.add_mapping(RegionMapping { - process: pid, - va, - perms, - via, - }) - }); - if !recorded { - for i in 0..pages { - self.platform.unmap_page(pid, page_at(va, i)); - } - return Err(KernelError::NoFreeSlot); - } - Ok(()) - } - - /// Removes `pid`'s mapping of region `id`, if it has one. - pub(crate) fn unmap_region_from(&mut self, id: RegionId, pid: ProcessId) { - let Some(region) = self.regions.get_mut(id) else { - return; - }; - let pages = region.pages().value() as usize; - if let Some(m) = region.remove_mapping(pid) { - for i in 0..pages { - self.platform.unmap_page(pid, page_at(m.va, i)); - } - } - } - - /// Frees regions owned by `pid` (unmapping them from every other - /// process) and forgets `pid`'s mappings of other regions. - fn teardown_regions(&mut self, pid: ProcessId) { - let mut owned = [None; domain::memory::MAX_REGIONS]; - for (slot, id) in owned.iter_mut().zip(self.regions.ids_owned_by(pid)) { - *slot = Some(id); - } - for id in owned.into_iter().flatten() { - let Some(region) = self.regions.remove(id) else { - continue; - }; - let pages = region.pages().value() as usize; - for m in region.mappings().filter(|m| m.process != pid) { - for i in 0..pages { - self.platform.unmap_page(m.process, page_at(m.va, i)); - } - } - if region.backing() == RegionBacking::Pool { - for i in 0..pages { - self.frames.free(region.base().offset(i)); - } - } - } - for (_, region) in self.regions.iter_mut() { - region.remove_mapping(pid); - } - } - - /// Releases everything `pid` holds in memory: its address space, page - /// tables, user pages and owned regions. - pub(crate) fn teardown_memory(&mut self, pid: ProcessId) { - self.teardown_regions(pid); - self.platform.destroy_address_space(pid); - self.frames.free_owned_by(pid); - if let Some(q) = self.quotas.get_mut(pid.raw() as usize) { - *q = Quota::default(); - } - if let Some(c) = self.heap_cursors.get_mut(pid.raw() as usize) { - *c = 0; - } - } -} - -fn page_at(base: VirtualAddress, i: usize) -> VirtualAddress { - VirtualAddress::from_raw(base.raw() + i * PAGE_SIZE) -} diff --git a/crates/kernel/src/memory/mod.rs b/crates/kernel/src/memory/mod.rs new file mode 100644 index 0000000..05dd6f5 --- /dev/null +++ b/crates/kernel/src/memory/mod.rs @@ -0,0 +1,214 @@ +//! Address-space bookkeeping. The kernel decides every user mapping from +//! its own records (`FrameTable`, `RegionTable`, quotas) and only then tells +//! the platform to apply it; it never asks the hardware what is mapped. + +mod pages; +mod region; + +use domain::{ + error::KernelError, + memory::{ + frame::{FrameTable, FrameUse, PAGE_SIZE}, + quota::Quota, + }, +}; +use platform::{FrameSource, MapError, Platform}; +use types::{ + address::{PhysicalAddress, VirtualAddress}, + id::ProcessId, + mapping::PagePerms, +}; + +use crate::Kernel; + +/// First VA the kernel considers when picking a spot for `RequestPages`. +/// Below it sit the program image and boot-time device windows. +pub(crate) const USER_HEAP_START: usize = 0x40000; + +/// Page-table frames for one address space, charged to its owner. +struct ChargedFrames<'a> { + frames: &'a mut FrameTable, + quota: &'a mut Quota, + owner: ProcessId, +} + +impl FrameSource for ChargedFrames<'_> { + fn alloc_table_frame(&mut self) -> Option { + if !self.quota.charge(1) { + return None; + } + match self.frames.alloc(FrameUse::PageTable { owner: self.owner }) { + Some(pa) => Some(pa), + None => { + self.quota.uncharge(1); + None + } + } + } +} + +fn map_error(e: MapError) -> KernelError { + match e { + MapError::OutOfFrames => KernelError::OutOfMemory, + MapError::InvalidAddress => KernelError::InvalidAddress, + MapError::NoAddressSpace => KernelError::OutOfMemory, + } +} + +impl Kernel

{ + /// Whether `[va, va + pages)` is page aligned and inside the user window. + pub(crate) fn in_user_window(va: VirtualAddress, pages: usize) -> bool { + let start = va.raw(); + let Some(len) = pages.checked_mul(PAGE_SIZE) else { + return false; + }; + let Some(end) = start.checked_add(len) else { + return false; + }; + pages > 0 + && start.is_multiple_of(PAGE_SIZE) + && start >= P::USER_VA_START + && end <= P::USER_VA_END + } + + /// `pid`'s user page at `va`: the platform's page table says where it + /// points, the frame table confirms the frame really is that page. + fn user_frame( + &self, + pid: ProcessId, + va: VirtualAddress, + ) -> Option<(PhysicalAddress, PagePerms)> { + let pa = self.platform.translate(pid, va)?; + self.frames.user_at(pa, pid, va).map(|perms| (pa, perms)) + } + + fn is_mapped(&self, pid: ProcessId, va: VirtualAddress) -> bool { + self.user_frame(pid, va).is_some() || self.regions.covering(pid, va).is_some() + } + + fn range_is_free(&self, pid: ProcessId, va: VirtualAddress, pages: usize) -> bool { + (0..pages).all(|i| !self.is_mapped(pid, page_at(va, i))) + } + + fn quota_mut(&mut self, pid: ProcessId) -> Result<&mut Quota, KernelError> { + self.quotas + .get_mut(pid.raw() as usize) + .ok_or(KernelError::InvalidProcess(pid)) + } + + pub fn page_usage(&self, pid: ProcessId) -> usize { + self.quotas.get(pid.raw() as usize).map_or(0, Quota::used) + } + + pub fn set_page_limit(&mut self, pid: ProcessId, limit: usize) -> Result<(), KernelError> { + self.processes.get(pid)?; + if self.quota_mut(pid)?.set_limit(limit) { + Ok(()) + } else { + Err(KernelError::OutOfMemory) + } + } + + pub fn free_page_count(&self) -> usize { + self.frames.free_count() + } + + /// Maps `pa` at `va` in `pid`, building page tables on `pid`'s quota. + fn platform_map( + &mut self, + pid: ProcessId, + va: VirtualAddress, + pa: PhysicalAddress, + perms: PagePerms, + ) -> Result<(), KernelError> { + let quota = self + .quotas + .get_mut(pid.raw() as usize) + .ok_or(KernelError::InvalidProcess(pid))?; + let mut source = ChargedFrames { + frames: &mut self.frames, + quota, + owner: pid, + }; + self.platform + .map_page(pid, va, pa, perms, &mut source) + .map_err(map_error) + } + + pub(crate) fn create_address_space(&mut self, pid: ProcessId) -> Result<(), KernelError> { + let quota = self + .quotas + .get_mut(pid.raw() as usize) + .ok_or(KernelError::InvalidProcess(pid))?; + *quota = Quota::default(); + let mut source = ChargedFrames { + frames: &mut self.frames, + quota, + owner: pid, + }; + let created = self + .platform + .create_address_space(pid, &mut source) + .map_err(map_error); + if created.is_err() { + self.frames.free_owned_by(pid); + if let Some(q) = self.quotas.get_mut(pid.raw() as usize) { + *q = Quota::default(); + } + } + created + } + + /// Allocates, zeroes and maps one fresh page for `pid` at `va`. + fn map_fresh_page( + &mut self, + pid: ProcessId, + va: VirtualAddress, + perms: PagePerms, + ) -> Result { + let usage = FrameUse::user(pid, va, perms).ok_or(KernelError::InvalidAddress)?; + if !self.quota_mut(pid)?.charge(1) { + return Err(KernelError::OutOfMemory); + } + let Some(pa) = self.frames.alloc(usage) else { + self.quota_mut(pid)?.uncharge(1); + return Err(KernelError::OutOfMemory); + }; + self.platform.zero_frame(pa); + if let Err(e) = self.platform_map(pid, va, pa, perms) { + self.frames.free(pa); + self.quota_mut(pid)?.uncharge(1); + return Err(e); + } + Ok(pa) + } + + /// Removes one user page of `pid` and returns its frame to the pool. + fn unmap_and_free(&mut self, pid: ProcessId, va: VirtualAddress) { + if let Some((pa, _)) = self.user_frame(pid, va) { + self.platform.unmap_page(pid, va); + self.frames.free(pa); + if let Some(q) = self.quotas.get_mut(pid.raw() as usize) { + q.uncharge(1); + } + } + } + + /// Releases everything `pid` holds in memory: its address space, page + /// tables, user pages and owned regions. + pub(crate) fn teardown_memory(&mut self, pid: ProcessId) { + self.teardown_regions(pid); + self.platform.destroy_address_space(pid); + self.frames.free_owned_by(pid); + if let Some(q) = self.quotas.get_mut(pid.raw() as usize) { + *q = Quota::default(); + } + if let Some(c) = self.heap_cursors.get_mut(pid.raw() as usize) { + *c = 0; + } + } +} + +fn page_at(base: VirtualAddress, i: usize) -> VirtualAddress { + VirtualAddress::from_raw(base.raw() + i * PAGE_SIZE) +} diff --git a/crates/kernel/src/memory/pages.rs b/crates/kernel/src/memory/pages.rs new file mode 100644 index 0000000..53c7676 --- /dev/null +++ b/crates/kernel/src/memory/pages.rs @@ -0,0 +1,138 @@ +//! Page moves, release and heap placement. + +use domain::{ + error::KernelError, + memory::frame::{FrameUse, PAGE_SIZE}, +}; +use platform::Platform; +use types::{ + address::{PhysicalAddress, VirtualAddress}, + id::ProcessId, + mapping::PagePerms, +}; + +use super::{USER_HEAP_START, page_at}; +use crate::Kernel; + +impl Kernel

{ + /// Frame backing the user page at `va` in `pid`. Lets boot code fill + /// pages it has just mapped for a process. + pub fn user_page_frame(&self, pid: ProcessId, va: VirtualAddress) -> Option { + self.user_frame(pid, va).map(|(pa, _)| pa) + } + + /// Maps `pages` fresh zeroed pages at `va`, all or nothing. + pub fn map_fresh_range( + &mut self, + pid: ProcessId, + va: VirtualAddress, + pages: usize, + perms: PagePerms, + ) -> Result<(), KernelError> { + if !Self::in_user_window(va, pages) { + return Err(KernelError::InvalidAddress); + } + if !self.range_is_free(pid, va, pages) { + return Err(KernelError::AddressInUse); + } + for i in 0..pages { + if let Err(e) = self.map_fresh_page(pid, page_at(va, i), perms) { + for j in 0..i { + self.unmap_and_free(pid, page_at(va, j)); + } + return Err(e); + } + } + Ok(()) + } + + /// Next-fit search for `pages` free heap pages from `pid`'s last request, then from the bottom. + pub(crate) fn find_free_heap_range( + &self, + pid: ProcessId, + pages: usize, + ) -> Option { + let bottom = USER_HEAP_START.max(P::USER_VA_START); + let cursor = self + .heap_cursors + .get(pid.raw() as usize) + .copied() + .unwrap_or(0) + .max(bottom); + self.first_fit_from(pid, cursor, pages) + .or_else(|| self.first_fit_from(pid, bottom, pages)) + } + + /// Records where `pid`'s next heap search starts. + pub(crate) fn advance_heap_cursor(&mut self, pid: ProcessId, past: VirtualAddress) { + if let Some(c) = self.heap_cursors.get_mut(pid.raw() as usize) { + *c = past.raw(); + } + } + + fn first_fit_from(&self, pid: ProcessId, from: usize, pages: usize) -> Option { + let mut candidate = from; + while Self::in_user_window(VirtualAddress::from_raw(candidate), pages) { + let va = VirtualAddress::from_raw(candidate); + match (0..pages).find(|&i| self.is_mapped(pid, page_at(va, i))) { + None => return Some(va), + Some(busy) => candidate += (busy + 1) * PAGE_SIZE, + } + } + None + } + + /// Validates that every page of the range is a user page `pid` owns, + /// then releases them all. + pub(crate) fn release_range( + &mut self, + pid: ProcessId, + va: VirtualAddress, + pages: usize, + ) -> Result<(), KernelError> { + if !Self::in_user_window(va, pages) { + return Err(KernelError::InvalidAddress); + } + if !(0..pages).all(|i| self.user_frame(pid, page_at(va, i)).is_some()) { + return Err(KernelError::InvalidAddress); + } + for i in 0..pages { + self.unmap_and_free(pid, page_at(va, i)); + } + Ok(()) + } + + /// Moves the page at `src` in `from` to `dst` in `to`. The frame and its + /// quota charge change hands; `from` loses access. + pub(crate) fn move_page( + &mut self, + from: ProcessId, + src: VirtualAddress, + to: ProcessId, + dst: VirtualAddress, + perms: PagePerms, + ) -> Result<(), KernelError> { + if !Self::in_user_window(src, 1) || !Self::in_user_window(dst, 1) { + return Err(KernelError::InvalidAddress); + } + let (pa, _) = self + .user_frame(from, src) + .ok_or(KernelError::InvalidAddress)?; + self.processes.get(to)?; + if !self.range_is_free(to, dst, 1) { + return Err(KernelError::AddressInUse); + } + let usage = FrameUse::user(to, dst, perms).ok_or(KernelError::InvalidAddress)?; + if !self.quota_mut(to)?.charge(1) { + return Err(KernelError::OutOfMemory); + } + if let Err(e) = self.platform_map(to, dst, pa, perms) { + self.quota_mut(to)?.uncharge(1); + return Err(e); + } + self.platform.unmap_page(from, src); + self.frames.retag(pa, usage); + self.quota_mut(from)?.uncharge(1); + Ok(()) + } +} diff --git a/crates/kernel/src/memory/region.rs b/crates/kernel/src/memory/region.rs new file mode 100644 index 0000000..16eb483 --- /dev/null +++ b/crates/kernel/src/memory/region.rs @@ -0,0 +1,201 @@ +//! Shared and device regions and their mappings. + +use domain::{ + error::KernelError, + memory::{ + Region, RegionBacking, RegionMapping, + frame::{FrameUse, PAGE_SIZE}, + }, +}; +use platform::Platform; +use types::{ + address::{PhysicalAddress, VirtualAddress}, + bounded::PageCount, + id::{ProcessId, RegionId}, + mapping::PagePerms, +}; + +use super::page_at; +use crate::Kernel; + +impl Kernel

{ + /// Allocates a physically contiguous, zeroed region charged to `owner`. + pub fn create_pool_region( + &mut self, + owner: ProcessId, + pages: PageCount, + ) -> Result { + self.processes.get(owner)?; + let id = self.regions.next_free_id().ok_or(KernelError::NoFreeSlot)?; + let count = pages.value() as usize; + if !self.quota_mut(owner)?.charge(count) { + return Err(KernelError::OutOfMemory); + } + let Some(base) = self + .frames + .alloc_contiguous(count, |_| FrameUse::Region { region: id }) + else { + self.quota_mut(owner)?.uncharge(count); + return Err(KernelError::OutOfMemory); + }; + for i in 0..count { + self.platform.zero_frame(base.offset(i)); + } + self.regions + .insert(Region::new(owner, RegionBacking::Pool, base, pages)) + .ok_or(KernelError::NoFreeSlot) + } + + /// Describes device memory at `base` so it can be mapped like a region. + pub fn create_device_region( + &mut self, + owner: ProcessId, + base: PhysicalAddress, + pages: PageCount, + ) -> Result { + self.processes.get(owner)?; + if !base.raw().is_multiple_of(PAGE_SIZE) { + return Err(KernelError::InvalidAddress); + } + // Device memory must never alias frames the kernel hands out. + let len = pages.value() as usize * PAGE_SIZE; + let start = base.raw(); + let end = start.checked_add(len).ok_or(KernelError::InvalidAddress)?; + let pool_start = self.frames.base().raw(); + let pool_end = pool_start + self.frames.capacity() * PAGE_SIZE; + if start < pool_end && end > pool_start { + return Err(KernelError::InvalidAddress); + } + // Nor another device's window: each device has one region, so + // revoking or delegating it means the same thing everywhere. + let overlaps = self.regions.iter().any(|(_, r)| { + let r_start = r.base().raw(); + let r_end = r_start.saturating_add(r.pages().value() as usize * PAGE_SIZE); + r.backing() == RegionBacking::Device && start < r_end && end > r_start + }); + if overlaps { + return Err(KernelError::AddressInUse); + } + self.regions + .insert(Region::new(owner, RegionBacking::Device, base, pages)) + .ok_or(KernelError::NoFreeSlot) + } + + pub fn region_base(&self, id: RegionId) -> Option { + self.regions.get(id).map(Region::base) + } + + pub fn region_pages(&self, id: RegionId) -> Option { + self.regions.get(id).map(Region::pages) + } + + /// Maps region `id` for boot code, all or nothing; not tied to any capability. + pub fn map_region( + &mut self, + id: RegionId, + pid: ProcessId, + va: VirtualAddress, + perms: PagePerms, + ) -> Result<(), KernelError> { + self.map_region_via(id, pid, va, perms, None) + } + + /// Maps region `id`, all or nothing; a mapping made `via` a capability dies with it. + pub(crate) fn map_region_via( + &mut self, + id: RegionId, + pid: ProcessId, + va: VirtualAddress, + perms: PagePerms, + via: Option, + ) -> Result<(), KernelError> { + self.processes.get(pid)?; + let region = self.regions.get(id).ok_or(KernelError::InvalidRegion)?; + let (base, pages) = (region.base(), region.pages().value() as usize); + if region.mappings().any(|m| m.process == pid) { + return Err(KernelError::AddressInUse); + } + // W^X holds across processes too: nobody may write what someone + // else can execute. + let clashes = |other: PagePerms| { + matches!( + (perms, other), + (PagePerms::ReadWrite, PagePerms::ReadExecute) + | (PagePerms::ReadExecute, PagePerms::ReadWrite) + ) + }; + if region.mappings().any(|m| clashes(m.perms)) { + return Err(KernelError::WritableAndExecutable); + } + if !Self::in_user_window(va, pages) { + return Err(KernelError::InvalidAddress); + } + if !self.range_is_free(pid, va, pages) { + return Err(KernelError::AddressInUse); + } + for i in 0..pages { + if let Err(e) = self.platform_map(pid, page_at(va, i), base.offset(i), perms) { + for j in 0..i { + self.platform.unmap_page(pid, page_at(va, j)); + } + return Err(e); + } + } + let recorded = self.regions.get_mut(id).is_some_and(|r| { + r.add_mapping(RegionMapping { + process: pid, + va, + perms, + via, + }) + }); + if !recorded { + for i in 0..pages { + self.platform.unmap_page(pid, page_at(va, i)); + } + return Err(KernelError::NoFreeSlot); + } + Ok(()) + } + + /// Removes `pid`'s mapping of region `id`, if it has one. + pub(crate) fn unmap_region_from(&mut self, id: RegionId, pid: ProcessId) { + let Some(region) = self.regions.get_mut(id) else { + return; + }; + let pages = region.pages().value() as usize; + if let Some(m) = region.remove_mapping(pid) { + for i in 0..pages { + self.platform.unmap_page(pid, page_at(m.va, i)); + } + } + } + + /// Frees regions owned by `pid` (unmapping them from every other + /// process) and forgets `pid`'s mappings of other regions. + pub(super) fn teardown_regions(&mut self, pid: ProcessId) { + let mut owned = [None; domain::memory::MAX_REGIONS]; + for (slot, id) in owned.iter_mut().zip(self.regions.ids_owned_by(pid)) { + *slot = Some(id); + } + for id in owned.into_iter().flatten() { + let Some(region) = self.regions.remove(id) else { + continue; + }; + let pages = region.pages().value() as usize; + for m in region.mappings().filter(|m| m.process != pid) { + for i in 0..pages { + self.platform.unmap_page(m.process, page_at(m.va, i)); + } + } + if region.backing() == RegionBacking::Pool { + for i in 0..pages { + self.frames.free(region.base().offset(i)); + } + } + } + for (_, region) in self.regions.iter_mut() { + region.remove_mapping(pid); + } + } +} diff --git a/crates/kernel/src/proofs/authority.rs b/crates/kernel/src/proofs/authority.rs index 79c744c..55b702e 100644 --- a/crates/kernel/src/proofs/authority.rs +++ b/crates/kernel/src/proofs/authority.rs @@ -1,15 +1,6 @@ -//! Mint creates no authority. The real kernel, with tables shrunk under -//! `cfg(kani)`, runs `mint` with arbitrary arguments in a small state -//! whose capabilities carry arbitrary rights. Afterwards every capability -//! to an object that already existed carries no more rights than some -//! capability to that object carried before. -//! -//! Only this harness is kept. The same check over delegate, delete, -//! revoke, create and kill either exceeded 12 GB in CBMC or tripped -//! modelling artifacts ("unreachable code" on safe `Option` matches that -//! an exhaustive host replay never reaches). Those operations are covered -//! by the syscall storm's global invariants (tests/storm.rs) and the -//! capability-tree model test (tests/captree_model.rs) instead. +//! Mint creates no authority: after `mint` with arbitrary arguments, no capability to a +//! pre-existing object carries rights beyond some earlier one. Other operations exceeded +//! 12 GB in CBMC; tests/storm.rs and tests/captree_model.rs cover them. use super::platform::KaniPlatform; use crate::Kernel; diff --git a/crates/kernel/src/smp.rs b/crates/kernel/src/smp.rs index 19c9245..7c832cd 100644 --- a/crates/kernel/src/smp.rs +++ b/crates/kernel/src/smp.rs @@ -1,9 +1,5 @@ -//! Cores. Every thread has a home core, chosen when it is created, and -//! only ever runs there: it waits in that core's run queue and is never -//! migrated. Making a thread ready from another core sends that core an -//! IPI when it has to look at its queue again (it is idle, or the thread -//! outranks what it is running), and so does taking away the thread a -//! core is running. +//! Cores: each thread has a home core and never migrates; waking or removing a thread on +//! another core sends that core an IPI when it must re-check its queue. use domain::{ scheduler::{Scheduler, SchedulerDecision}, @@ -88,10 +84,8 @@ impl Kernel

{ self.threads.get(tid).ok().map(|t| t.priority()) } - /// What `core` should do after an IPI: keep running its thread, or - /// switch to a higher-priority one now waiting. When it has no thread - /// (it was idle, or its thread was destroyed) the caller picks the - /// next one itself. + /// What `core` does after an IPI: keep its thread or switch to a higher-priority one; + /// with no thread the caller picks. pub fn reschedule(&mut self, core: CoreId) -> SchedulerDecision { let Some(current) = self.scheduler.current(core) else { return SchedulerDecision::Continue; diff --git a/crates/kernel/src/syscall/ipc.rs b/crates/kernel/src/syscall/ipc/endpoint.rs similarity index 51% rename from crates/kernel/src/syscall/ipc.rs rename to crates/kernel/src/syscall/ipc/endpoint.rs index 3c333f0..9cab477 100644 --- a/crates/kernel/src/syscall/ipc.rs +++ b/crates/kernel/src/syscall/ipc/endpoint.rs @@ -1,121 +1,22 @@ -//! Endpoint IPC, notifications and interrupt delivery. docs/ipc.md is the -//! specification; the comments below only point at the non-obvious rules. +//! Endpoint send/receive, call/reply, capability transfer and minting. use domain::{ - capability::Capability, - error::KernelError, - message::Message, - notification::SignalEffect, - resource::Resource, - scheduler::Scheduler, - thread::{BlockReason, ThreadState}, + capability::Capability, error::KernelError, message::Message, resource::Resource, + thread::BlockReason, }; use platform::Platform; use types::{ badge::Badge, bounded::CapSlot, - generation::Generation, - id::{EndpointId, IrqId, NotificationId, ProcessId, ThreadId}, + id::{EndpointId, ProcessId, ThreadId}, permission::{Permission, PermissionSet}, }; -use super::{Delivery, DeliveryKind, SyscallOutcome, SyscallResult}; +use super::super::{Delivery, DeliveryKind, SyscallOutcome, SyscallResult}; +use super::Outgoing; use crate::Kernel; -/// A thread named by id and generation, so a stale reference can be told -/// apart from a new thread that reused the id. -#[derive(Debug, Clone, Copy, PartialEq, Eq)] -pub struct ThreadRef { - pub tid: ThreadId, - pub generation: Generation, -} - -/// A message a blocked sender is waiting to hand over. -#[derive(Debug, Clone, Copy)] -pub(crate) struct Outgoing { - message: Message, - badge: Badge, - /// The sender's endpoint cap had `Delegate`, so a capability may travel. - grant: bool, -} - -/// Per-thread IPC bookkeeping. -#[derive(Debug, Clone, Copy, Default)] -pub struct IpcState { - pub(crate) outgoing: Option, - /// The caller this thread owes a reply to. - pub(crate) reply_to: Option, - pub(crate) bound: Option, -} - -fn rw_delegate() -> PermissionSet { - PermissionSet::empty() - .with(Permission::Read) - .with(Permission::Write) - .with(Permission::Delegate) -} - impl Kernel

{ - pub(crate) fn ipc(&self, tid: ThreadId) -> Option<&IpcState> { - self.ipc.get(tid.raw() as usize) - } - - pub(crate) fn ipc_mut(&mut self, tid: ThreadId) -> Option<&mut IpcState> { - self.ipc.get_mut(tid.raw() as usize) - } - - 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; - } - } - - fn thread_ref(&self, tid: ThreadId) -> Option { - Some(ThreadRef { - tid, - generation: self.threads.generation(tid)?, - }) - } - - fn is_live(&self, r: ThreadRef) -> bool { - self.threads.generation(r.tid) == Some(r.generation) - } - - fn is_blocked_as(&self, tid: ThreadId, f: impl Fn(&BlockReason) -> bool) -> bool { - matches!(self.threads.get(tid).map(|t| *t.state()), Ok(ThreadState::Blocked(r)) if f(&r)) - } - - /// Blocks the running caller. - pub(crate) fn block_caller(&mut self, tid: ThreadId, reason: BlockReason) -> SyscallOutcome { - if let Ok(t) = self.threads.get_mut(tid) { - let _ = t.block(reason); - } - self.scheduler.remove(tid); - SyscallOutcome::BlockCaller(reason) - } - - /// Makes a blocked thread runnable with `result` as its syscall result. - pub(crate) fn wake(&mut self, tid: ThreadId, result: SyscallResult) { - let Ok(thread) = self.threads.get_mut(tid) else { - return; - }; - let priority = thread.priority(); - if thread.unblock().is_ok() { - self.set_pending_result(tid, Some(result)); - self.make_ready(tid, priority); - } - } - - /// Releases a caller waiting on `reply` with `NoReply`, if it is still - /// that caller and still waiting. - pub(crate) fn release_caller(&mut self, reply: ThreadRef) { - if self.is_live(reply) - && self.is_blocked_as(reply.tid, |r| *r == BlockReason::AwaitingReply) - { - self.wake(reply.tid, SyscallResult::Error(KernelError::NoReply)); - } - } - fn endpoint_cap( &self, pid: ProcessId, @@ -133,22 +34,8 @@ impl Kernel

{ } } - fn notification_cap( - &self, - pid: ProcessId, - slot: CapSlot, - needed: Permission, - ) -> Result<(NotificationId, Badge, Generation), KernelError> { - let cap = self.check_cap(pid, slot, needed)?; - match cap.resource() { - Resource::Notification(id) => Ok((*id, cap.badge(), *cap.generation())), - _ => Err(KernelError::WrongObject), - } - } - - /// Copies the capability in `slot` of `from` into `to`'s table, if the /// transfer is allowed and still valid. Returns where it landed. - fn transfer_cap( + pub(super) fn transfer_cap( &mut self, from: ProcessId, slot: Option, @@ -169,7 +56,7 @@ impl Kernel

{ /// Hands `out` from `sender` to `receiver`. For a call, the receiver's /// reply slot now names the sender. - fn deliver( + pub(super) fn deliver( &mut self, sender: ThreadId, out: Outgoing, @@ -413,157 +300,4 @@ impl Kernel

{ } } } - - // ---- notifications ---- - - pub fn create_notification(&mut self, owner: ProcessId) -> Result { - self.processes.get(owner)?; - self.notifications - .create(owner) - .ok_or(KernelError::NoFreeSlot) - } - - pub(crate) fn create_notification_cap( - &mut self, - pid: ProcessId, - ) -> Result { - let id = self.create_notification(pid)?; - self.grant_cap(pid, Resource::Notification(id), rw_delegate()) - .inspect_err(|_| { - self.notifications.destroy(id); - }) - } - - /// Signals `id` with `badge`; shared by `Signal` and interrupts. - fn signal_notification(&mut self, id: NotificationId, badge: Badge) { - let bound_receiving = self - .notifications - .get(id) - .and_then(|n| n.bound()) - .is_some_and(|t| self.is_blocked_as(t, |r| matches!(r, BlockReason::Receiving(_)))); - let Some(ntfn) = self.notifications.get_mut(id) else { - return; - }; - match ntfn.signal(badge, bound_receiving) { - SignalEffect::WakeWaiter(t, bits) => { - self.wake(t, SyscallResult::Received(Delivery::signal(bits))); - } - SignalEffect::WakeBound(t, bits) => { - self.leave_queue(t); - self.wake(t, SyscallResult::Received(Delivery::signal(bits))); - } - SignalEffect::Stored => {} - } - } - - pub(crate) fn signal(&mut self, pid: ProcessId, slot: CapSlot) -> Result<(), KernelError> { - let (id, badge, _) = self.notification_cap(pid, slot, Permission::Write)?; - self.signal_notification(id, badge); - Ok(()) - } - - pub(crate) fn wait(&mut self, tid: ThreadId, pid: ProcessId, slot: CapSlot) -> SyscallOutcome { - let id = match self.notification_cap(pid, slot, Permission::Read) { - Ok((id, _, _)) => id, - Err(e) => return SyscallOutcome::Complete(SyscallResult::Error(e)), - }; - let Some(ntfn) = self.notifications.get_mut(id) else { - return SyscallOutcome::Complete(SyscallResult::Error(KernelError::NoSuchObject)); - }; - if ntfn.has_bits() { - let bits = ntfn.take_bits(); - return SyscallOutcome::Complete(SyscallResult::Received(Delivery::signal(bits))); - } - if !ntfn.add_waiter(tid) { - return SyscallOutcome::Complete(SyscallResult::Error(KernelError::EndpointFull)); - } - self.block_caller(tid, BlockReason::WaitingNotification(id)) - } - - pub(crate) fn poll(&mut self, pid: ProcessId, slot: CapSlot) -> Result { - let (id, _, _) = self.notification_cap(pid, slot, Permission::Read)?; - self.notifications - .get_mut(id) - .map(|n| n.take_bits()) - .ok_or(KernelError::NoSuchObject) - } - - pub(crate) fn bind_notification( - &mut self, - tid: ThreadId, - pid: ProcessId, - slot: CapSlot, - ) -> Result<(), KernelError> { - let (id, _, _) = self.notification_cap(pid, slot, Permission::Read)?; - if self.ipc(tid).is_none_or(|s| s.bound.is_some()) { - return Err(KernelError::InvalidArgument); - } - let ntfn = self - .notifications - .get_mut(id) - .ok_or(KernelError::NoSuchObject)?; - if !ntfn.bind(tid) { - return Err(KernelError::InvalidArgument); - } - if let Some(s) = self.ipc_mut(tid) { - s.bound = Some(id); - } - Ok(()) - } - - // ---- interrupts ---- - - fn interrupt_cap(&self, pid: ProcessId, slot: CapSlot) -> Result { - match self.check_cap(pid, slot, Permission::Execute)?.resource() { - Resource::Interrupt(irq) => Ok(*irq), - _ => Err(KernelError::WrongObject), - } - } - - pub(crate) fn set_irq_notification( - &mut self, - pid: ProcessId, - irq_slot: CapSlot, - ntfn_slot: CapSlot, - ) -> Result<(), KernelError> { - let irq = self.interrupt_cap(pid, irq_slot)?; - let (notification, badge, generation) = - self.notification_cap(pid, ntfn_slot, Permission::Write)?; - let route = domain::irq::IrqRoute { - notification, - generation, - badge, - }; - if self.irqs.set(irq, route) { - Ok(()) - } else { - Err(KernelError::InvalidIrq(irq)) - } - } - - pub(crate) fn ack_interrupt( - &mut self, - pid: ProcessId, - slot: CapSlot, - ) -> Result<(), KernelError> { - let irq = self.interrupt_cap(pid, slot)?; - self.platform.unmask_irq(irq); - Ok(()) - } - - /// An interrupt fired: mask the line and signal its notification. The - /// line stays masked until the handler acknowledges it. - pub fn handle_interrupt(&mut self, irq: IrqId) { - self.platform.mask_irq(irq); - let Some(route) = self.irqs.route(irq) else { - return; - }; - // A route set through a capability that has since been revoked, or - // to a notification whose slot was reused, is dead. - if self.notifications.generation(route.notification) != Some(route.generation) { - self.irqs.clear(irq); - return; - } - self.signal_notification(route.notification, route.badge); - } } diff --git a/crates/kernel/src/syscall/ipc/irq.rs b/crates/kernel/src/syscall/ipc/irq.rs new file mode 100644 index 0000000..29b6f8a --- /dev/null +++ b/crates/kernel/src/syscall/ipc/irq.rs @@ -0,0 +1,67 @@ +//! Interrupt routing to notifications. + +use domain::{error::KernelError, resource::Resource}; +use platform::Platform; +use types::{ + bounded::CapSlot, + id::{IrqId, ProcessId}, + permission::Permission, +}; + +use crate::Kernel; + +impl Kernel

{ + fn interrupt_cap(&self, pid: ProcessId, slot: CapSlot) -> Result { + match self.check_cap(pid, slot, Permission::Execute)?.resource() { + Resource::Interrupt(irq) => Ok(*irq), + _ => Err(KernelError::WrongObject), + } + } + + pub(crate) fn set_irq_notification( + &mut self, + pid: ProcessId, + irq_slot: CapSlot, + ntfn_slot: CapSlot, + ) -> Result<(), KernelError> { + let irq = self.interrupt_cap(pid, irq_slot)?; + let (notification, badge, generation) = + self.notification_cap(pid, ntfn_slot, Permission::Write)?; + let route = domain::irq::IrqRoute { + notification, + generation, + badge, + }; + if self.irqs.set(irq, route) { + Ok(()) + } else { + Err(KernelError::InvalidIrq(irq)) + } + } + + pub(crate) fn ack_interrupt( + &mut self, + pid: ProcessId, + slot: CapSlot, + ) -> Result<(), KernelError> { + let irq = self.interrupt_cap(pid, slot)?; + self.platform.unmask_irq(irq); + Ok(()) + } + + /// An interrupt fired: mask the line and signal its notification. The + /// line stays masked until the handler acknowledges it. + pub fn handle_interrupt(&mut self, irq: IrqId) { + self.platform.mask_irq(irq); + let Some(route) = self.irqs.route(irq) else { + return; + }; + // A route set through a capability that has since been revoked, or + // to a notification whose slot was reused, is dead. + if self.notifications.generation(route.notification) != Some(route.generation) { + self.irqs.clear(irq); + return; + } + self.signal_notification(route.notification, route.badge); + } +} diff --git a/crates/kernel/src/syscall/ipc/mod.rs b/crates/kernel/src/syscall/ipc/mod.rs new file mode 100644 index 0000000..6a462c2 --- /dev/null +++ b/crates/kernel/src/syscall/ipc/mod.rs @@ -0,0 +1,109 @@ +//! Endpoint IPC, notifications and interrupt delivery (see docs/ipc.md). + +mod endpoint; +mod irq; +mod notification; + +use domain::{ + error::KernelError, + message::Message, + scheduler::Scheduler, + thread::{BlockReason, ThreadState}, +}; +use platform::Platform; +use types::{ + badge::Badge, + generation::Generation, + id::{NotificationId, ThreadId}, +}; + +use super::{SyscallOutcome, SyscallResult}; +use crate::Kernel; + +/// A thread named by id and generation, so a stale reference can be told +/// apart from a new thread that reused the id. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub struct ThreadRef { + pub tid: ThreadId, + pub generation: Generation, +} + +/// A message a blocked sender is waiting to hand over. +#[derive(Debug, Clone, Copy)] +pub(crate) struct Outgoing { + message: Message, + badge: Badge, + /// The sender's endpoint cap had `Delegate`, so a capability may travel. + grant: bool, +} + +/// Per-thread IPC bookkeeping. +#[derive(Debug, Clone, Copy, Default)] +pub struct IpcState { + pub(crate) outgoing: Option, + /// The caller this thread owes a reply to. + pub(crate) reply_to: Option, + pub(crate) bound: Option, +} + +impl Kernel

{ + pub(crate) fn ipc(&self, tid: ThreadId) -> Option<&IpcState> { + self.ipc.get(tid.raw() as usize) + } + + pub(crate) fn ipc_mut(&mut self, tid: ThreadId) -> Option<&mut IpcState> { + self.ipc.get_mut(tid.raw() as usize) + } + + 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; + } + } + + fn thread_ref(&self, tid: ThreadId) -> Option { + Some(ThreadRef { + tid, + generation: self.threads.generation(tid)?, + }) + } + + fn is_live(&self, r: ThreadRef) -> bool { + self.threads.generation(r.tid) == Some(r.generation) + } + + fn is_blocked_as(&self, tid: ThreadId, f: impl Fn(&BlockReason) -> bool) -> bool { + matches!(self.threads.get(tid).map(|t| *t.state()), Ok(ThreadState::Blocked(r)) if f(&r)) + } + + /// Blocks the running caller. + pub(crate) fn block_caller(&mut self, tid: ThreadId, reason: BlockReason) -> SyscallOutcome { + if let Ok(t) = self.threads.get_mut(tid) { + let _ = t.block(reason); + } + self.scheduler.remove(tid); + SyscallOutcome::BlockCaller(reason) + } + + /// Makes a blocked thread runnable with `result` as its syscall result. + pub(crate) fn wake(&mut self, tid: ThreadId, result: SyscallResult) { + let Ok(thread) = self.threads.get_mut(tid) else { + return; + }; + let priority = thread.priority(); + if thread.unblock().is_ok() { + self.set_pending_result(tid, Some(result)); + self.make_ready(tid, priority); + } + } + + /// Releases a caller waiting on `reply` with `NoReply`, if it is still + /// that caller and still waiting. + pub(crate) fn release_caller(&mut self, reply: ThreadRef) { + if self.is_live(reply) + && self.is_blocked_as(reply.tid, |r| *r == BlockReason::AwaitingReply) + { + self.wake(reply.tid, SyscallResult::Error(KernelError::NoReply)); + } + } +} diff --git a/crates/kernel/src/syscall/ipc/notification.rs b/crates/kernel/src/syscall/ipc/notification.rs new file mode 100644 index 0000000..fb9dc54 --- /dev/null +++ b/crates/kernel/src/syscall/ipc/notification.rs @@ -0,0 +1,133 @@ +//! Notification objects: signal, wait, poll, bind. + +use domain::{ + error::KernelError, notification::SignalEffect, resource::Resource, thread::BlockReason, +}; +use platform::Platform; +use types::{ + badge::Badge, + bounded::CapSlot, + generation::Generation, + id::{NotificationId, ProcessId, ThreadId}, + permission::{Permission, PermissionSet}, +}; + +use super::super::{Delivery, SyscallOutcome, SyscallResult}; +use crate::Kernel; + +fn rw_delegate() -> PermissionSet { + PermissionSet::empty() + .with(Permission::Read) + .with(Permission::Write) + .with(Permission::Delegate) +} + +impl Kernel

{ + pub(super) fn notification_cap( + &self, + pid: ProcessId, + slot: CapSlot, + needed: Permission, + ) -> Result<(NotificationId, Badge, Generation), KernelError> { + let cap = self.check_cap(pid, slot, needed)?; + match cap.resource() { + Resource::Notification(id) => Ok((*id, cap.badge(), *cap.generation())), + _ => Err(KernelError::WrongObject), + } + } + + pub fn create_notification(&mut self, owner: ProcessId) -> Result { + self.processes.get(owner)?; + self.notifications + .create(owner) + .ok_or(KernelError::NoFreeSlot) + } + + pub(crate) fn create_notification_cap( + &mut self, + pid: ProcessId, + ) -> Result { + let id = self.create_notification(pid)?; + self.grant_cap(pid, Resource::Notification(id), rw_delegate()) + .inspect_err(|_| { + self.notifications.destroy(id); + }) + } + + /// Signals `id` with `badge`; shared by `Signal` and interrupts. + pub(super) fn signal_notification(&mut self, id: NotificationId, badge: Badge) { + let bound_receiving = self + .notifications + .get(id) + .and_then(|n| n.bound()) + .is_some_and(|t| self.is_blocked_as(t, |r| matches!(r, BlockReason::Receiving(_)))); + let Some(ntfn) = self.notifications.get_mut(id) else { + return; + }; + match ntfn.signal(badge, bound_receiving) { + SignalEffect::WakeWaiter(t, bits) => { + self.wake(t, SyscallResult::Received(Delivery::signal(bits))); + } + SignalEffect::WakeBound(t, bits) => { + self.leave_queue(t); + self.wake(t, SyscallResult::Received(Delivery::signal(bits))); + } + SignalEffect::Stored => {} + } + } + + pub(crate) fn signal(&mut self, pid: ProcessId, slot: CapSlot) -> Result<(), KernelError> { + let (id, badge, _) = self.notification_cap(pid, slot, Permission::Write)?; + self.signal_notification(id, badge); + Ok(()) + } + + pub(crate) fn wait(&mut self, tid: ThreadId, pid: ProcessId, slot: CapSlot) -> SyscallOutcome { + let id = match self.notification_cap(pid, slot, Permission::Read) { + Ok((id, _, _)) => id, + Err(e) => return SyscallOutcome::Complete(SyscallResult::Error(e)), + }; + let Some(ntfn) = self.notifications.get_mut(id) else { + return SyscallOutcome::Complete(SyscallResult::Error(KernelError::NoSuchObject)); + }; + if ntfn.has_bits() { + let bits = ntfn.take_bits(); + return SyscallOutcome::Complete(SyscallResult::Received(Delivery::signal(bits))); + } + if !ntfn.add_waiter(tid) { + return SyscallOutcome::Complete(SyscallResult::Error(KernelError::EndpointFull)); + } + self.block_caller(tid, BlockReason::WaitingNotification(id)) + } + + pub(crate) fn poll(&mut self, pid: ProcessId, slot: CapSlot) -> Result { + let (id, _, _) = self.notification_cap(pid, slot, Permission::Read)?; + self.notifications + .get_mut(id) + .map(|n| n.take_bits()) + .ok_or(KernelError::NoSuchObject) + } + + pub(crate) fn bind_notification( + &mut self, + tid: ThreadId, + pid: ProcessId, + slot: CapSlot, + ) -> Result<(), KernelError> { + let (id, _, _) = self.notification_cap(pid, slot, Permission::Read)?; + if self.ipc(tid).is_none_or(|s| s.bound.is_some()) { + return Err(KernelError::InvalidArgument); + } + let ntfn = self + .notifications + .get_mut(id) + .ok_or(KernelError::NoSuchObject)?; + if !ntfn.bind(tid) { + return Err(KernelError::InvalidArgument); + } + if let Some(s) = self.ipc_mut(tid) { + s.bound = Some(id); + } + Ok(()) + } +} diff --git a/crates/kernel/src/syscall/memory.rs b/crates/kernel/src/syscall/memory.rs index c7749c2..89a2f63 100644 --- a/crates/kernel/src/syscall/memory.rs +++ b/crates/kernel/src/syscall/memory.rs @@ -51,9 +51,7 @@ impl Kernel

{ ) } - /// Moves one of the caller's pages into the process named by - /// `process_cap`. Executable pages are mapped read-execute, others - /// read-write. + /// Moves one of the caller's pages into `process_cap`'s process (exec pages RX, others RW). pub(crate) fn handle_map_page( &mut self, caller_pid: ProcessId, @@ -99,9 +97,7 @@ impl Kernel

{ self.grant_cap(pid, Resource::Memory(id), all) } - /// Maps the region behind `slot` into the caller. The capability must - /// allow every access `perms` grants; the mapping lasts as long as - /// the capability. + /// Maps the region behind `slot` into the caller; the cap must allow `perms`, mapping lasts as long as the cap. pub(crate) fn map_region_cap( &mut self, pid: ProcessId, @@ -125,9 +121,7 @@ impl Kernel

{ self.map_region_via(id, pid, va, perms, via) } - /// The physical base of the region behind `slot`. Needs Read on the - /// capability; pool regions are physically contiguous, so the base is - /// enough to program a device. + /// Physical base of the region behind `slot` (needs Read); pool regions are contiguous. pub(crate) fn region_address_cap( &self, pid: ProcessId, diff --git a/crates/kernel/src/teardown.rs b/crates/kernel/src/teardown.rs new file mode 100644 index 0000000..37ef20e --- /dev/null +++ b/crates/kernel/src/teardown.rs @@ -0,0 +1,126 @@ +//! Process, thread, endpoint and notification teardown. + +use domain::{error::KernelError, notification::MAX_NOTIFICATIONS, thread::ThreadState}; +use platform::Platform; +use types::id::{ProcessId, ThreadId}; + +use crate::{Kernel, SyscallResult}; + +impl Kernel

{ + pub(crate) fn destroy_process(&mut self, pid: ProcessId) { + use domain::process::MAX_THREADS_PER_PROCESS; + + let thread_ids: [Option; MAX_THREADS_PER_PROCESS] = match self.processes.get(pid) + { + Ok(p) => { + let mut ids = [None; MAX_THREADS_PER_PROCESS]; + for (slot, tid) in ids.iter_mut().zip(p.thread_ids()) { + *slot = Some(tid); + } + ids + } + Err(_) => return, + }; + + self.cleanup_threads(&thread_ids); + self.delete_all_caps(pid); + self.destroy_endpoints_owned_by(pid); + self.destroy_notifications_owned_by(pid); + self.teardown_memory(pid); + + let _ = self.processes.destroy(pid); + } + + pub(crate) fn cleanup_threads(&mut self, thread_ids: &[Option]) { + use domain::scheduler::Scheduler; + for tid in thread_ids.iter().flatten() { + self.leave_queue(*tid); + if let Some(n) = self + .ipc(*tid) + .and_then(|s| s.bound) + .and_then(|n| self.notifications.get_mut(n)) + { + n.remove_thread(*tid); + } + let ipc = self.ipc_mut(*tid).map(core::mem::take).unwrap_or_default(); + if let Some(caller) = ipc.reply_to { + self.release_caller(caller); + } + self.evict(*tid); + self.scheduler.remove(*tid); + self.set_pending_result(*tid, None); + let _ = self.threads.destroy(*tid); + } + } + + /// Takes a blocked thread off the one queue its block reason names, so + /// nothing needs to scan every endpoint and notification. + pub(crate) fn leave_queue(&mut self, tid: ThreadId) { + use domain::thread::BlockReason::*; + let Ok(ThreadState::Blocked(reason)) = self.threads.get(tid).map(|t| *t.state()) else { + return; + }; + match reason { + Sending(ep) | Calling(ep) => { + self.endpoints.get_mut(ep).map(|e| e.remove_sender(tid)); + } + Receiving(ep) => { + self.endpoints.get_mut(ep).map(|e| e.remove_receiver(tid)); + } + WaitingNotification(n) => { + if let Some(n) = self.notifications.get_mut(n) { + n.remove_waiter(tid); + } + } + AwaitingReply => {} + } + } + + /// Destroys every endpoint `owner` created, waking anyone blocked on + /// them with an error instead of leaving them blocked forever. + pub(crate) fn destroy_endpoints_owned_by(&mut self, owner: ProcessId) { + let mut owned = [None; domain::endpoint::MAX_ENDPOINTS]; + for (slot, id) in owned.iter_mut().zip(self.endpoints.ids_owned_by(owner)) { + *slot = Some(id); + } + for id in owned.into_iter().flatten() { + let Some(mut ep) = self.endpoints.destroy(id) else { + continue; + }; + while let Some(tid) = ep.dequeue_sender().or_else(|| ep.dequeue_receiver()) { + self.wake_with_error(tid, KernelError::InvalidEndpoint(id)); + } + } + } + + /// Destroys every notification `owner` created, waking its waiters + /// with an error and unbinding its bound thread. + pub(crate) fn destroy_notifications_owned_by(&mut self, owner: ProcessId) { + let mut owned = [None; MAX_NOTIFICATIONS]; + for (slot, id) in owned.iter_mut().zip(self.notifications.ids_owned_by(owner)) { + *slot = Some(id); + } + for id in owned.into_iter().flatten() { + let Some(mut n) = self.notifications.destroy(id) else { + continue; + }; + if let Some(bound) = n.bound() + && let Some(s) = self.ipc_mut(bound) + { + s.bound = None; + } + while let Some(tid) = n.pop_waiter() { + self.wake_with_error(tid, KernelError::NoSuchObject); + } + } + } + + /// Makes a blocked thread runnable with `error` as its syscall result, + /// 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; + } + self.wake(tid, SyscallResult::Error(error)); + } +} diff --git a/crates/kernel/src/tests/bench.rs b/crates/kernel/src/tests/bench.rs index 5a433ec..da59b0f 100644 --- a/crates/kernel/src/tests/bench.rs +++ b/crates/kernel/src/tests/bench.rs @@ -1,7 +1,5 @@ -//! Worst-case timings of kernel paths that scan tables. Not run by default: +//! Worst-case timings of table-scanning paths; ignored by default: //! `cargo test -p kernel --lib bench -- --ignored --nocapture --test-threads 1`. -//! Numbers are host nanoseconds at the test profile's opt-level, good for -//! comparing before and after a change, not for absolute claims. extern crate std; diff --git a/crates/kernel/src/tests/captree_model.rs b/crates/kernel/src/tests/captree_model.rs index dbd8517..373ee13 100644 --- a/crates/kernel/src/tests/captree_model.rs +++ b/crates/kernel/src/tests/captree_model.rs @@ -1,8 +1,4 @@ -//! Randomized check of the derivation tree against an independent model. -//! The model applies the rules of docs/ipc.md (derive records a parent, -//! delete re-parents, revoke removes the subtree, death deletes everything -//! a process holds) to its own data; after every step the kernel must hold -//! exactly the capabilities the model says are alive. +//! Randomized check of the derivation tree against a model of the rules in docs/ipc.md. extern crate std; diff --git a/crates/kernel/src/tests/ipc_invariants.rs b/crates/kernel/src/tests/ipc_invariants.rs index 4cd5c40..738b48b 100644 --- a/crates/kernel/src/tests/ipc_invariants.rs +++ b/crates/kernel/src/tests/ipc_invariants.rs @@ -1,8 +1,5 @@ -//! Randomized check of the IPC state machine. Six threads in three -//! processes send, call, receive, reply and signal at random over two -//! endpoints and a notification; one process is periodically killed and -//! re-created. After every step the kernel's queues, block reasons, reply -//! slots and run queue must agree, and no message may be duplicated. +//! Randomized IPC state machine check: queues, block reasons, reply slots and run queue +//! agree after every step, and no message is duplicated. use super::*; use crate::syscall::{Delivery, DeliveryKind}; diff --git a/crates/kernel/src/tests/storm.rs b/crates/kernel/src/tests/storm.rs index 3baf54c..ae0e9a4 100644 --- a/crates/kernel/src/tests/storm.rs +++ b/crates/kernel/src/tests/storm.rs @@ -303,9 +303,8 @@ impl Rng { } } -/// Sets up a fresh round: a hub process owning the shared endpoints, -/// notification and region; two children with two threads each; and caps -/// to all shared objects for init and the children. +/// Sets up a round: a hub owning shared endpoints, notification and region; two children +/// with two threads each; caps to the shared objects for init and the children. fn new_round(k: &mut Kernel, init: ProcessId, init_thread: ThreadId) { use domain::resource::Resource; let all = types::permission::PermissionSet::empty() @@ -416,10 +415,8 @@ fn the_kernel_survives_a_syscall_storm() { storm(1); } -/// The same storm with threads homed on four cores. Each step runs on one -/// core, as the thread that core is running; the kernel is still entered -/// one call at a time (stage 1 takes a single lock), but threads on other -/// cores are live meanwhile and IPIs arrive late. +/// The same storm with threads homed on four cores; each step runs as that core's thread +/// and IPIs arrive late. #[test] fn the_kernel_survives_a_syscall_storm_on_four_cores() { storm(4); @@ -502,10 +499,7 @@ fn storm(cores: u8) { continue; } let mut args: [usize; 6] = core::array::from_fn(|_| rng.arg()); - // Random arguments almost never name a region cap, a free - // address and valid perms at once; half the time, pick one of - // the caller's region caps (often the hub's shared region) so - // regions really are mapped into several processes. + // Half the time pick one of the caller's region caps so regions really get shared. if nr == SYS_MAP_REGION && rng.below(2) == 0 { let regions = region_slots(&k, k.thread_process(tid)); if !regions.is_empty() { diff --git a/crates/platform/src/lib.rs b/crates/platform/src/lib.rs index f325933..3c3bee7 100644 --- a/crates/platform/src/lib.rs +++ b/crates/platform/src/lib.rs @@ -26,9 +26,7 @@ pub enum MapError { /// The kernel's contract with an architecture. The kernel decides what is /// mapped where; the platform only applies those decisions to hardware. pub trait Platform { - /// User mappings live in `[USER_VA_START, USER_VA_END)`. The platform - /// guarantees nothing else is mapped in that window in any address - /// space, so page tables covering it are private to each process. + /// User mappings live in `[USER_VA_START, USER_VA_END)`; nothing else is mapped there in any space. const USER_VA_START: usize; const USER_VA_END: usize; @@ -50,9 +48,7 @@ pub trait Platform { ) -> Result<(), MapError>; /// Removes the mapping at `va` and flushes it from the TLB. fn unmap_page(&mut self, process: ProcessId, va: VirtualAddress); - /// The frame `va` is mapped to in `process`, if any. Only a lookup: - /// the kernel confirms every answer against its own frame table, so a - /// wrong answer can make the kernel refuse but never trust a frame. + /// The frame `va` maps to in `process`, if any. Advisory: the kernel confirms against its frame table. fn translate(&self, process: ProcessId, va: VirtualAddress) -> Option; /// Fills a frame with zeros before it is handed to a process. fn zero_frame(&mut self, pa: PhysicalAddress); diff --git a/crates/types/src/badge.rs b/crates/types/src/badge.rs index 3f32b26..a4ac2a2 100644 --- a/crates/types/src/badge.rs +++ b/crates/types/src/badge.rs @@ -1,6 +1,4 @@ -/// A word stamped on an endpoint or notification capability by `Mint`. -/// Receivers see the badge of the capability a sender used, which is how a -/// server tells its clients apart. Zero means "unbadged". +/// A word stamped on an endpoint or notification cap by `Mint`; zero means unbadged. #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] pub struct Badge(usize); diff --git a/crates/types/src/bootinfo.rs b/crates/types/src/bootinfo.rs index 6e96b3c..76b4cf9 100644 --- a/crates/types/src/bootinfo.rs +++ b/crates/types/src/bootinfo.rs @@ -1,7 +1,4 @@ -//! What boot tells init: a read-only page at `BOOT_INFO_VA` saying which -//! of init's capability slots hold which board device (seL4's BootInfo, -//! reduced to what this system needs). Everything else init learns by -//! asking the devices themselves. +//! What boot tells init: a read-only page at `BOOT_INFO_VA` mapping init's capability slots to board devices. /// Where the page is mapped in init. pub const BOOT_INFO_VA: usize = 0x2F000; @@ -11,9 +8,7 @@ pub const MAX_BOOT_DEVICES: usize = 16; /// A slot field with no capability in it. pub const NO_SLOT: u64 = u64::MAX; -/// What kind of device a board entry is. Board code knows; init asks the -/// device itself only where a kind has several possibilities (which -/// virtio device sits in a slot). +/// What kind of device a board entry is; init asks the device itself to disambiguate. pub const KIND_VIRTIO: u64 = 1; pub const KIND_UART_16550: u64 = 2; diff --git a/crates/types/src/proofs/generation.rs b/crates/types/src/proofs/generation.rs index 0958505..6a2a402 100644 --- a/crates/types/src/proofs/generation.rs +++ b/crates/types/src/proofs/generation.rs @@ -1,8 +1,6 @@ use crate::generation::Generation; -/// Generations only ever increase, so a capability minted for an earlier -/// generation can never match again. (The old wrapping counter returned to -/// earlier values after 2^32 bumps.) +/// Generations only increase, so a capability minted for an earlier generation never matches again. #[kani::proof] fn generation_next_is_strictly_greater_or_exhausted() { let value: u32 = kani::any();