diff --git a/Makefile b/Makefile index 3ee4d56..c80c196 100644 --- a/Makefile +++ b/Makefile @@ -32,14 +32,17 @@ clippy: test: cargo test --workspace +# CBMC can eat all RAM and take the desktop down with it; cap each run. +KANI = systemd-run --user --scope -q -p MemoryMax=12G -p MemorySwapMax=0 cargo kani + kani-types: - cargo kani -p types + $(KANI) -p types kani-domain: - cargo kani -p domain + $(KANI) -p domain kani-kernel: - cargo kani -p kernel + $(KANI) -p kernel kani: kani-types kani-domain kani-kernel diff --git a/crates/adapter-riscv/src/trap/mod.rs b/crates/adapter-riscv/src/trap/mod.rs index 9bc1f06..3bce71a 100644 --- a/crates/adapter-riscv/src/trap/mod.rs +++ b/crates/adapter-riscv/src/trap/mod.rs @@ -144,152 +144,18 @@ pub fn set_kernel_stack(kernel_sp: usize) { } } -/// Decodes the syscall in `frame`, or `None` for an unknown number or an -/// argument that is not representable (e.g. a slot out of range). -fn decode_syscall(frame: &TrapFrame) -> Option { - use domain::message::Message; - use domain::syscall::Syscall; - use types::address::{DataRef, EntryPoint, StackPointer, VirtualAddress}; - use types::badge::Badge; - use types::bounded::{CapSlot, PageCount}; - use types::permission::PermissionSet; - use types::syscall_abi::*; - - let nr = frame.regs[17]; // a7 - let a = |i: usize| frame.regs[10 + i]; - let slot = |i: usize| CapSlot::new(u8::try_from(a(i)).ok()?); - let message = || -> Option { - let msg = Message::from_words([a(1), a(2), a(3), a(4)]); - Some(match a(5) { - NONE => msg, - _ => msg.with_cap(slot(5)?), - }) - }; - - Some(match nr { - SYS_EXIT => Syscall::Exit, - SYS_HALT => Syscall::Halt, - SYS_EXIT_THREAD => Syscall::ExitThread, - SYS_YIELD => Syscall::Yield, - SYS_GET_TIME => Syscall::GetTime, - SYS_GET_PROCESS_ID => Syscall::GetProcessId, - SYS_SEND => Syscall::Send { - endpoint: slot(0)?, - message: message()?, - }, - SYS_CALL => Syscall::Call { - endpoint: slot(0)?, - message: message()?, - }, - SYS_RECEIVE => Syscall::Receive { endpoint: slot(0)? }, - SYS_REPLY => Syscall::Reply { - message: message()?, - }, - SYS_REPLY_RECV => Syscall::ReplyRecv { - endpoint: slot(0)?, - message: message()?, - }, - SYS_DELEGATE => Syscall::Delegate { - slot: slot(0)?, - to_endpoint: slot(1)?, - permissions: PermissionSet::from_bits(u8::try_from(a(2)).ok()?), - }, - SYS_MINT => Syscall::Mint { - slot: slot(0)?, - badge: Badge::new(a(1)), - permissions: PermissionSet::from_bits(u8::try_from(a(2)).ok()?), - }, - SYS_CREATE_NOTIFICATION => Syscall::CreateNotification, - SYS_SIGNAL => Syscall::Signal { - notification: slot(0)?, - }, - SYS_WAIT => Syscall::Wait { - notification: slot(0)?, - }, - SYS_POLL => Syscall::Poll { - notification: slot(0)?, - }, - SYS_BIND_NOTIFICATION => Syscall::BindNotification { - notification: slot(0)?, - }, - SYS_SET_IRQ_NOTIFICATION => Syscall::SetIrqNotification { - irq: slot(0)?, - notification: slot(1)?, - }, - SYS_ACKNOWLEDGE_INTERRUPT => Syscall::AcknowledgeInterrupt { irq: slot(0)? }, - SYS_CREATE_PROCESS => Syscall::CreateProcess { - create_cap: slot(0)?, - image: DataRef::empty(), - }, - SYS_KILL => Syscall::Kill { process: slot(0)? }, - SYS_REVOKE => Syscall::Revoke { slot: slot(0)? }, - SYS_DROP_CAP => Syscall::DropCap { slot: slot(0)? }, - SYS_SPAWN_THREAD => Syscall::SpawnThread { - entry: EntryPoint::from_raw(a(0)), - stack: StackPointer::from_raw(a(1)), - }, - SYS_REQUEST_PAGES => Syscall::RequestPages { - count: PageCount::new(u16::try_from(a(0)).ok()?)?, - }, - SYS_RELEASE_PAGES => Syscall::ReleasePages { - addr: VirtualAddress::from_raw(a(0)), - count: PageCount::new(u16::try_from(a(1)).ok()?)?, - }, - SYS_SPAWN_THREAD_IN => Syscall::SpawnThreadIn { - process: slot(0)?, - entry: EntryPoint::from_raw(a(1)), - stack: StackPointer::from_raw(a(2)), - }, - SYS_CREATE_ENDPOINT => Syscall::CreateEndpoint, - SYS_CREATE_REGION => Syscall::CreateRegion { - pages: PageCount::new(u16::try_from(a(0)).ok()?)?, - }, - SYS_MAP_REGION => Syscall::MapRegion { - region: slot(0)?, - va: VirtualAddress::from_raw(a(1)), - perms: match a(2) { - PERMS_READ_ONLY => types::mapping::PagePerms::ReadOnly, - PERMS_READ_WRITE => types::mapping::PagePerms::ReadWrite, - PERMS_READ_EXECUTE => types::mapping::PagePerms::ReadExecute, - _ => return None, - }, - }, - SYS_DEBUG_PUTCHAR => Syscall::DebugPutchar { byte: a(0) as u8 }, - SYS_MAP_PAGE => Syscall::MapPage { - process: slot(0)?, - src_va: VirtualAddress::from_raw(a(1)), - dst_va: VirtualAddress::from_raw(a(2)), - executable: a(3) != 0, - }, - _ => return None, - }) +fn args(frame: &TrapFrame) -> [usize; 6] { + let mut a = [0usize; 6]; + a.copy_from_slice(&frame.regs[10..16]); + a } -/// Writes a completed syscall's result per the register ABI: status in -/// `a0`, results in `a1..`. -fn write_result(frame: &mut TrapFrame, result: &kernel::SyscallResult) { - use kernel::SyscallResult; - use kernel::syscall::DeliveryKind; - use types::syscall_abi::{KIND_CALL, KIND_MESSAGE, KIND_SIGNAL, NONE}; +fn set_results(frame: &mut TrapFrame, regs: [usize; 8]) { + frame.regs[10..18].copy_from_slice(®s); +} - let r = &mut frame.regs; - r[10] = 0; - match result { - SyscallResult::Ok => {} - SyscallResult::Value(v) => r[11] = *v, - SyscallResult::Slot(s) => r[11] = s.value() as usize, - SyscallResult::Received(d) => { - r[11] = d.badge; - r[12..16].copy_from_slice(&d.words); - r[16] = d.cap.map_or(NONE, |s| s.value() as usize); - r[17] = match d.kind { - DeliveryKind::Message => KIND_MESSAGE, - DeliveryKind::Call => KIND_CALL, - DeliveryKind::Signal => KIND_SIGNAL, - }; - } - SyscallResult::Error(e) => r[10] = kernel::syscall::error_code(e) as usize, - } +fn write_result(frame: &mut TrapFrame, result: &kernel::SyscallResult) { + set_results(frame, kernel::abi::encode(result)); } fn save_frame_to_context(frame: &TrapFrame, ctx: &mut domain::thread::SavedContext) { @@ -424,8 +290,8 @@ fn handle_exception(frame: &mut TrapFrame, scause: usize) { CAUSE_ECALL_U => { frame.sepc += 4; - let Some(syscall) = decode_syscall(frame) else { - frame.regs[10] = types::syscall_abi::ErrorCode::UnknownSyscall as usize; + let Some(syscall) = kernel::abi::decode(frame.regs[17], &args(frame)) else { + set_results(frame, kernel::abi::unknown_syscall()); return; }; { diff --git a/crates/domain/src/capability/derivation.rs b/crates/domain/src/capability/derivation.rs index 8c3be8f..a4d53b6 100644 --- a/crates/domain/src/capability/derivation.rs +++ b/crates/domain/src/capability/derivation.rs @@ -8,21 +8,26 @@ /// always exists before it does. pub fn descendants(parents: &[Option; N], root: usize) -> [bool; N] { let mut marked = [false; N]; - if root >= N { + let Some(r) = marked.get_mut(root) else { return marked; - } - marked[root] = true; + }; + *r = true; // Each pass extends the marked set by at least one generation of // children; a chain in an N-node forest is at most N - 1 long. for _ in 0..N { let mut changed = false; for i in 0..N { - if !marked[i] - && let Some(p) = parents[i].map(usize::from) - && p < N - && marked[p] + let parent_marked = parents + .get(i) + .copied() + .flatten() + .and_then(|p| marked.get(usize::from(p)).copied()) + .unwrap_or(false); + if let Some(m) = marked.get_mut(i) + && !*m + && parent_marked { - marked[i] = true; + *m = true; changed = true; } } diff --git a/crates/domain/src/capability/mod.rs b/crates/domain/src/capability/mod.rs index b12432b..09bfcc5 100644 --- a/crates/domain/src/capability/mod.rs +++ b/crates/domain/src/capability/mod.rs @@ -101,15 +101,20 @@ impl CapabilityTable { } } + fn slot(&self, slot: CapSlot) -> Option<&Capability> { + self.slots.get(slot.value() as usize)?.as_ref() + } + /// Generation of an occupied slot. pub fn slot_generation(&self, slot: CapSlot) -> Option { - self.slots[slot.value() as usize].as_ref()?; + self.slot(slot)?; self.generations.current(slot.value() as usize) } pub fn get_mut(&mut self, slot: CapSlot) -> Result<&mut Capability, KernelError> { - self.slots[slot.value() as usize] - .as_mut() + self.slots + .get_mut(slot.value() as usize) + .and_then(Option::as_mut) .ok_or(KernelError::InvalidSlot(slot)) } @@ -121,27 +126,28 @@ impl CapabilityTable { } pub fn get(&self, slot: CapSlot) -> Result<&Capability, KernelError> { - let idx = slot.value() as usize; - self.slots[idx] - .as_ref() - .ok_or(KernelError::InvalidSlot(slot)) + self.slot(slot).ok_or(KernelError::InvalidSlot(slot)) } pub fn insert(&mut self, cap: Capability) -> Result { - let idx = (0..MAX_CAPS_PER_PROCESS) - .find(|&i| self.slots[i].is_none() && self.generations.is_usable(i)) + let generations = &self.generations; + let (idx, free) = self + .slots + .iter_mut() + .enumerate() + .find(|(i, s)| s.is_none() && generations.is_usable(*i)) .ok_or(KernelError::NoFreeSlot)?; - - self.slots[idx] = Some(cap); - CapSlot::new(idx as u8).ok_or(KernelError::NoFreeSlot) + let slot = CapSlot::new(idx as u8).ok_or(KernelError::NoFreeSlot)?; + *free = Some(cap); + Ok(slot) } pub fn remove(&mut self, slot: CapSlot) -> Result<(), KernelError> { let idx = slot.value() as usize; - if self.slots[idx].is_none() { + let taken = self.slots.get_mut(idx).and_then(Option::take); + if taken.is_none() { return Err(KernelError::InvalidSlot(slot)); } - self.slots[idx] = None; self.generations.advance(idx); Ok(()) } diff --git a/crates/domain/src/endpoint/mod.rs b/crates/domain/src/endpoint/mod.rs index e9daa10..3dedec2 100644 --- a/crates/domain/src/endpoint/mod.rs +++ b/crates/domain/src/endpoint/mod.rs @@ -57,6 +57,14 @@ impl Endpoint { self.waiting_receivers.pop() } + pub fn senders(&self) -> impl Iterator + '_ { + self.waiting_senders.iter() + } + + pub fn receivers(&self) -> impl Iterator + '_ { + self.waiting_receivers.iter() + } + pub fn is_sender(&self, thread: ThreadId) -> bool { self.waiting_senders.contains(thread) } @@ -82,7 +90,7 @@ impl Endpoint { } } -pub const MAX_ENDPOINTS: usize = 256; +pub const MAX_ENDPOINTS: usize = if cfg!(kani) { 2 } else { 256 }; pub struct EndpointTable { endpoints: [Option; MAX_ENDPOINTS], @@ -98,10 +106,14 @@ impl EndpointTable { } pub fn create(&mut self, owner: ProcessId) -> Option { - let idx = (0..MAX_ENDPOINTS) - .find(|&i| self.endpoints[i].is_none() && self.generations.is_usable(i))?; + let generations = &self.generations; + let (idx, slot) = self + .endpoints + .iter_mut() + .enumerate() + .find(|(i, s)| s.is_none() && generations.is_usable(*i))?; let id = EndpointId::from_raw(idx as u16); - self.endpoints[idx] = Some(Endpoint::new(id, owner)); + *slot = Some(Endpoint::new(id, owner)); Some(id) } @@ -111,6 +123,10 @@ impl EndpointTable { self.generations.current(id.raw() as usize) } + pub fn iter(&self) -> impl Iterator { + self.endpoints.iter().flatten() + } + pub fn ids_owned_by(&self, owner: ProcessId) -> impl Iterator + '_ { self.endpoints .iter() diff --git a/crates/domain/src/endpoint/wait_queue.rs b/crates/domain/src/endpoint/wait_queue.rs index 926eaee..7861ad5 100644 --- a/crates/domain/src/endpoint/wait_queue.rs +++ b/crates/domain/src/endpoint/wait_queue.rs @@ -1,6 +1,6 @@ use types::id::ThreadId; -pub const MAX_WAITERS: usize = 16; +pub const MAX_WAITERS: usize = if cfg!(kani) { 2 } else { 16 }; /// Bounded FIFO of blocked threads. Order is preserved across pops and /// removals, so no waiter can be overtaken. @@ -21,13 +21,13 @@ impl WaitQueue { if self.len == N || self.contains(thread) { return None; } - self.entries[self.len] = Some(thread); + *self.entries.get_mut(self.len)? = Some(thread); self.len += 1; Some(()) } pub fn pop(&mut self) -> Option { - let head = self.entries[0]?; + let head = self.entries.first().copied().flatten()?; self.close_gap(0); Some(head) } @@ -45,20 +45,33 @@ impl WaitQueue { } } + pub fn iter(&self) -> impl Iterator + '_ { + self.entries.iter().take(self.len).flatten().copied() + } + pub fn contains(&self, thread: ThreadId) -> bool { - self.entries[..self.len].contains(&Some(thread)) + self.entries + .iter() + .take(self.len) + .any(|e| *e == Some(thread)) } pub fn is_empty(&self) -> bool { self.len == 0 } + /// Removes entry `i`, shifting later entries forward to keep order. fn close_gap(&mut self, i: usize) { - for j in i..self.len - 1 { - self.entries[j] = self.entries[j + 1]; + for j in i..self.len.saturating_sub(1) { + let next = self.entries.get(j + 1).copied().flatten(); + if let Some(e) = self.entries.get_mut(j) { + *e = next; + } + } + self.len = self.len.saturating_sub(1); + if let Some(last) = self.entries.get_mut(self.len) { + *last = None; } - self.len -= 1; - self.entries[self.len] = None; } } diff --git a/crates/domain/src/irq/mod.rs b/crates/domain/src/irq/mod.rs index d857e8d..279c670 100644 --- a/crates/domain/src/irq/mod.rs +++ b/crates/domain/src/irq/mod.rs @@ -8,7 +8,7 @@ use types::{ #[path = "tests.rs"] mod tests; -const MAX_IRQS: usize = 256; +const MAX_IRQS: usize = if cfg!(kani) { 2 } else { 256 }; /// Where an interrupt is delivered: a signal on a notification, through a /// capability snapshot (generation and badge) taken when the route was set. diff --git a/crates/domain/src/lib.rs b/crates/domain/src/lib.rs index 4e50784..6ce9f2c 100644 --- a/crates/domain/src/lib.rs +++ b/crates/domain/src/lib.rs @@ -1,4 +1,18 @@ #![no_std] +// A kernel panic takes the whole system down, so kernel code may not +// contain any way to panic. Tests and proofs are exempt. +#![cfg_attr( + not(any(test, kani)), + deny( + clippy::unwrap_used, + clippy::expect_used, + clippy::panic, + clippy::unreachable, + clippy::todo, + clippy::unimplemented, + clippy::indexing_slicing + ) +)] #[cfg(kani)] pub mod proofs; diff --git a/crates/domain/src/memory/frame/mod.rs b/crates/domain/src/memory/frame/mod.rs index 6d8b575..571261f 100644 --- a/crates/domain/src/memory/frame/mod.rs +++ b/crates/domain/src/memory/frame/mod.rs @@ -18,7 +18,7 @@ mod proofs; pub const PAGE_SIZE: usize = 4096; /// Frames the kernel can track. The board's user pool must fit. -pub const MAX_FRAMES: usize = 4096; +pub const MAX_FRAMES: usize = if cfg!(kani) { 6 } else { 4096 }; #[derive(Debug, Clone, Copy, PartialEq, Eq)] pub enum FrameUse { @@ -88,13 +88,26 @@ impl FrameTable { self.base.offset(idx) } + /// The frames that exist (`total` is clamped to `N` at construction). + fn live(&self) -> &[Option] { + self.frames.get(..self.total).unwrap_or(&[]) + } + + fn live_mut(&mut self) -> &mut [Option] { + self.frames.get_mut(..self.total).unwrap_or(&mut []) + } + pub fn get(&self, pa: PhysicalAddress) -> Option<&FrameUse> { - self.frames[self.index_of(pa)?].as_ref() + self.frames.get(self.index_of(pa)?)?.as_ref() } pub fn alloc(&mut self, usage: FrameUse) -> Option { - let idx = self.frames[..self.total].iter().position(Option::is_none)?; - self.frames[idx] = Some(usage); + let (idx, slot) = self + .live_mut() + .iter_mut() + .enumerate() + .find(|(_, f)| f.is_none())?; + *slot = Some(usage); self.free -= 1; Some(self.address_of(idx)) } @@ -110,8 +123,8 @@ impl FrameTable { } let mut run = 0; let mut start = None; - for idx in 0..self.total { - if self.frames[idx].is_some() { + for (idx, f) in self.live().iter().enumerate() { + if f.is_some() { run = 0; continue; } @@ -122,8 +135,9 @@ impl FrameTable { } } let start = start?; - for i in 0..count { - self.frames[start + i] = Some(usage(i)); + let run = self.live_mut().get_mut(start..start + count)?; + for (i, f) in run.iter_mut().enumerate() { + *f = Some(usage(i)); } self.free -= count; Some(self.address_of(start)) @@ -132,7 +146,7 @@ impl FrameTable { /// Frees an allocated frame and reports what it was used for. pub fn free(&mut self, pa: PhysicalAddress) -> Option { let idx = self.index_of(pa)?; - let usage = self.frames[idx].take()?; + let usage = self.frames.get_mut(idx)?.take()?; self.free += 1; Some(usage) } @@ -140,7 +154,11 @@ impl FrameTable { /// Changes the use of an allocated frame (e.g. moving it to another /// process). Fails on free frames. pub fn retag(&mut self, pa: PhysicalAddress, usage: FrameUse) -> bool { - match self.index_of(pa).and_then(|i| self.frames[i].as_mut()) { + match self + .index_of(pa) + .and_then(|i| self.frames.get_mut(i)) + .and_then(Option::as_mut) + { Some(slot) => { *slot = usage; true @@ -159,22 +177,19 @@ impl FrameTable { return None; } let page = u32::try_from(va.raw() / PAGE_SIZE).ok()?; - self.frames[..self.total] - .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 { + 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. pub fn iter(&self) -> impl Iterator + '_ { - self.frames[..self.total] + self.live() .iter() .enumerate() .filter_map(|(idx, f)| f.as_ref().map(|u| (self.address_of(idx), u))) @@ -185,7 +200,7 @@ impl FrameTable { &self, owner: ProcessId, ) -> impl Iterator + '_ { - self.frames[..self.total] + self.live() .iter() .enumerate() .filter_map(move |(idx, f)| match f { @@ -201,7 +216,7 @@ impl FrameTable { /// how many were freed. pub fn free_owned_by(&mut self, owner: ProcessId) -> usize { let mut freed = 0; - for slot in &mut self.frames[..self.total] { + for slot in self.live_mut().iter_mut() { let owned = matches!( slot, Some(FrameUse::User { owner: o, .. } | FrameUse::PageTable { owner: o }) if *o == owner diff --git a/crates/domain/src/memory/mod.rs b/crates/domain/src/memory/mod.rs index c2625ef..c2389dc 100644 --- a/crates/domain/src/memory/mod.rs +++ b/crates/domain/src/memory/mod.rs @@ -18,8 +18,8 @@ mod quota_tests; #[path = "tests.rs"] mod tests; -pub const MAX_REGIONS: usize = 64; -pub const MAX_REGION_MAPPINGS: usize = 4; +pub const MAX_REGIONS: usize = if cfg!(kani) { 1 } else { 64 }; +pub const MAX_REGION_MAPPINGS: usize = if cfg!(kani) { 2 } else { 4 }; /// Where a region's frames come from. #[derive(Debug, Clone, Copy, PartialEq, Eq)] @@ -136,7 +136,10 @@ impl RegionTable { } fn free_slot(&self) -> Option { - (0..MAX_REGIONS).find(|&i| self.regions[i].is_none() && self.generations.is_usable(i)) + self.regions + .iter() + .enumerate() + .position(|(i, r)| r.is_none() && self.generations.is_usable(i)) } /// The id the next `insert` will return. @@ -147,7 +150,7 @@ impl RegionTable { pub fn insert(&mut self, region: Region) -> Option { let idx = self.free_slot()?; - self.regions[idx] = Some(region); + *self.regions.get_mut(idx)? = Some(region); Some(RegionId::from_raw(idx as u16)) } diff --git a/crates/domain/src/message/mod.rs b/crates/domain/src/message/mod.rs index 21988c1..25dedfb 100644 --- a/crates/domain/src/message/mod.rs +++ b/crates/domain/src/message/mod.rs @@ -31,8 +31,9 @@ impl Message { &self.words } + /// Word `index`, or 0 past the end. pub fn word(&self, index: usize) -> usize { - self.words[index] + self.words.get(index).copied().unwrap_or(0) } pub fn cap(&self) -> Option { diff --git a/crates/domain/src/notification/mod.rs b/crates/domain/src/notification/mod.rs index beb0a7e..6dee2be 100644 --- a/crates/domain/src/notification/mod.rs +++ b/crates/domain/src/notification/mod.rs @@ -17,7 +17,7 @@ mod tests; #[path = "proofs.rs"] mod proofs; -pub const MAX_NOTIFICATIONS: usize = 128; +pub const MAX_NOTIFICATIONS: usize = if cfg!(kani) { 1 } else { 128 }; /// What the kernel must do after a signal. #[derive(Debug, Clone, Copy, PartialEq, Eq)] @@ -84,6 +84,10 @@ impl Notification { self.bits != 0 } + pub fn waiters(&self) -> impl Iterator + '_ { + self.waiters.iter() + } + pub fn is_waiter(&self, thread: ThreadId) -> bool { self.waiters.contains(thread) } @@ -132,10 +136,14 @@ impl NotificationTable { } pub fn create(&mut self, owner: ProcessId) -> Option { - let idx = (0..MAX_NOTIFICATIONS) - .find(|&i| self.slots[i].is_none() && self.generations.is_usable(i))?; + let generations = &self.generations; + let (idx, slot) = self + .slots + .iter_mut() + .enumerate() + .find(|(i, s)| s.is_none() && generations.is_usable(*i))?; let id = NotificationId::from_raw(idx as u16); - self.slots[idx] = Some(Notification::new(id, owner)); + *slot = Some(Notification::new(id, owner)); Some(id) } @@ -158,6 +166,10 @@ impl NotificationTable { Some(n) } + pub fn iter(&self) -> impl Iterator { + self.slots.iter().flatten() + } + pub fn ids_owned_by(&self, owner: ProcessId) -> impl Iterator + '_ { self.slots .iter() diff --git a/crates/domain/src/process/mod.rs b/crates/domain/src/process/mod.rs index 8334a29..172a558 100644 --- a/crates/domain/src/process/mod.rs +++ b/crates/domain/src/process/mod.rs @@ -10,8 +10,8 @@ use crate::{capability::CapabilityTable, error::KernelError, generations::SlotGe #[path = "tests.rs"] mod tests; -pub const MAX_THREADS_PER_PROCESS: usize = 4; -pub const MAX_PROCESSES: usize = 64; +pub const MAX_THREADS_PER_PROCESS: usize = if cfg!(kani) { 2 } else { 4 }; +pub const MAX_PROCESSES: usize = if cfg!(kani) { 3 } else { 64 }; pub struct Process { id: ProcessId, @@ -98,12 +98,16 @@ impl ProcessTable { capabilities: CapabilityTable, fault_handler: Option, ) -> Result { - let idx = (0..MAX_PROCESSES) - .find(|&i| self.processes[i].is_none() && self.generations.is_usable(i)) + let generations = &self.generations; + let (idx, slot) = self + .processes + .iter_mut() + .enumerate() + .find(|(i, s)| s.is_none() && generations.is_usable(*i)) .ok_or(KernelError::TooManyProcesses)?; let id = ProcessId::from_raw(idx as u16); - self.processes[idx] = Some(Process::new(id, capabilities, fault_handler)); + *slot = Some(Process::new(id, capabilities, fault_handler)); Ok(id) } diff --git a/crates/domain/src/resource.rs b/crates/domain/src/resource.rs index 01d89df..5370a92 100644 --- a/crates/domain/src/resource.rs +++ b/crates/domain/src/resource.rs @@ -1,6 +1,6 @@ use types::id::{EndpointId, IrqId, NotificationId, ProcessId, RegionId}; -#[derive(Clone)] +#[derive(Debug, Clone, Copy, PartialEq, Eq)] pub enum Resource { Memory(RegionId), Endpoint(EndpointId), diff --git a/crates/domain/src/scheduler/multi_core.rs b/crates/domain/src/scheduler/multi_core.rs index 9052d63..7c99d56 100644 --- a/crates/domain/src/scheduler/multi_core.rs +++ b/crates/domain/src/scheduler/multi_core.rs @@ -5,8 +5,8 @@ use types::{ use super::{Scheduler, SchedulerDecision, per_core::PerCoreScheduler}; -const MAX_CORES: usize = 8; -const MAX_SCHEDULED_THREADS: usize = 256; +const MAX_CORES: usize = if cfg!(kani) { 1 } else { 8 }; +const MAX_SCHEDULED_THREADS: usize = crate::thread::MAX_THREADS; const BALANCE_THRESHOLD: usize = 2; struct ThreadPlacement { @@ -25,32 +25,47 @@ impl MultiCoreScheduler { let cores = core::array::from_fn(|i| PerCoreScheduler::new(CoreId::from_raw(i as u8))); Self { cores, - num_cores, + num_cores: num_cores.min(MAX_CORES as u8), placements: [const { None }; MAX_SCHEDULED_THREADS], } } + fn core(&self, core: CoreId) -> Option<&PerCoreScheduler> { + self.active().get(core.raw() as usize) + } + + fn core_mut(&mut self, core: CoreId) -> Option<&mut PerCoreScheduler> { + let n = self.num_cores as usize; + self.cores.get_mut(..n)?.get_mut(core.raw() as usize) + } + + fn active(&self) -> &[PerCoreScheduler] { + self.cores.get(..self.num_cores as usize).unwrap_or(&[]) + } + + fn placement(&self, thread: ThreadId) -> Option<&ThreadPlacement> { + self.placements.get(thread.raw() as usize)?.as_ref() + } + /// Whether `thread` waits in some core's run queue. pub fn is_queued(&self, thread: ThreadId) -> bool { - self.cores[..self.num_cores as usize] - .iter() - .any(|c| c.is_queued(thread)) + self.active().iter().any(|c| c.is_queued(thread)) } pub fn current(&self, core: CoreId) -> Option { - self.cores[core.raw() as usize].current() + self.core(core)?.current() } pub fn set_current(&mut self, core: CoreId, thread: ThreadId) { - self.cores[core.raw() as usize].set_current(thread); + if let Some(c) = self.core_mut(core) { + c.set_current(thread); + } } /// Runs `thread` next on `core` regardless of its place in the queue. /// Fails if it is not queued there. pub fn run_now(&mut self, core: CoreId, thread: ThreadId) -> bool { - self.cores - .get_mut(core.raw() as usize) - .is_some_and(|c| c.run_now(thread)) + self.core_mut(core).is_some_and(|c| c.run_now(thread)) } fn thread_count_on(&self, core: CoreId) -> usize { @@ -75,38 +90,49 @@ impl MultiCoreScheduler { impl Scheduler for MultiCoreScheduler { fn add(&mut self, thread: ThreadId, priority: Priority, core: CoreId) { - let idx = thread.raw() as usize; - self.placements[idx] = Some(ThreadPlacement { core, priority }); - self.cores[core.raw() as usize].add(thread, priority); + if self.core(core).is_none() { + return; + } + let Some(placement) = self.placements.get_mut(thread.raw() as usize) else { + return; + }; + *placement = Some(ThreadPlacement { core, priority }); + if let Some(c) = self.core_mut(core) { + c.add(thread, priority); + } } fn remove(&mut self, thread: ThreadId) { - let idx = thread.raw() as usize; - if let Some(placement) = self.placements[idx].take() { - let core_idx = placement.core.raw() as usize; - self.cores[core_idx].remove(thread); - if self.cores[core_idx].current() == Some(thread) { - self.cores[core_idx].clear_current(); + let Some(placement) = self + .placements + .get_mut(thread.raw() as usize) + .and_then(Option::take) + else { + return; + }; + if let Some(c) = self.core_mut(placement.core) { + c.remove(thread); + if c.current() == Some(thread) { + c.clear_current(); } } } fn next(&mut self, core: CoreId) -> Option { - self.cores[core.raw() as usize].pick_next() + self.core_mut(core)?.pick_next() } fn tick(&mut self, core: CoreId, current: ThreadId) -> SchedulerDecision { - let idx = current.raw() as usize; - if let Some(placement) = &self.placements[idx] { - let current_priority = placement.priority; - let core_idx = core.raw() as usize; - if let Some(highest) = self.cores[core_idx].highest_waiting_priority() - && highest > current_priority - && let Some(next) = self.cores[core_idx].pick_next() - { - self.cores[core_idx].add(current, current_priority); - return SchedulerDecision::Preempt(next); - } + let Some(current_priority) = self.placement(current).map(|p| p.priority) else { + return SchedulerDecision::Continue; + }; + if let Some(c) = self.core_mut(core) + && let Some(highest) = c.highest_waiting_priority() + && highest > current_priority + && let Some(next) = c.pick_next() + { + c.add(current, current_priority); + return SchedulerDecision::Preempt(next); } SchedulerDecision::Continue } @@ -117,13 +143,14 @@ impl Scheduler for MultiCoreScheduler { _ => return, }; - if self.thread_count_on(busiest) > self.thread_count_on(lightest) + BALANCE_THRESHOLD { - let busiest_idx = busiest.raw() as usize; - if let Some((thread, priority)) = self.cores[busiest_idx].steal_lowest() { - let lightest_idx = lightest.raw() as usize; - self.cores[lightest_idx].add(thread, priority); - let tid = thread.raw() as usize; - self.placements[tid] = Some(ThreadPlacement { + if self.thread_count_on(busiest) > self.thread_count_on(lightest) + BALANCE_THRESHOLD + && let Some((thread, priority)) = self.core_mut(busiest).and_then(|c| c.steal_lowest()) + { + if let Some(c) = self.core_mut(lightest) { + c.add(thread, priority); + } + if let Some(p) = self.placements.get_mut(thread.raw() as usize) { + *p = Some(ThreadPlacement { core: lightest, priority, }); diff --git a/crates/domain/src/scheduler/priority_queue.rs b/crates/domain/src/scheduler/priority_queue.rs index 20f5973..d9370f3 100644 --- a/crates/domain/src/scheduler/priority_queue.rs +++ b/crates/domain/src/scheduler/priority_queue.rs @@ -58,62 +58,85 @@ impl PriorityQueue { self.links.get(thread.raw() as usize) } + fn links_mut(&mut self, thread: ThreadId) -> Option<&mut Links> { + self.links.get_mut(thread.raw() as usize) + } + /// Appends `thread` at `priority`. A thread that is already queued is /// left where it is; returns whether it was added. pub fn add(&mut self, thread: ThreadId, priority: Priority) -> bool { let idx = priority.value() as usize; - let t = thread.raw() as usize; - if t >= MAX_THREADS || idx >= NUM_PRIORITIES || self.links[t].queued_at.is_some() { + let queued = self.link(thread).is_none_or(|l| l.queued_at.is_some()); + let Some(old_tail) = self.lists.get(idx).map(|l| l.tail) else { + return false; + }; + if queued { return false; } - let old_tail = self.lists[idx].tail; - self.links[t] = Links { - prev: old_tail, - next: None, - queued_at: Some(idx as u8), - }; - match old_tail { - Some(tail) => self.links[tail.raw() as usize].next = Some(thread), - None => self.lists[idx].head = Some(thread), + if let Some(l) = self.links_mut(thread) { + *l = Links { + prev: old_tail, + next: None, + queued_at: Some(idx as u8), + }; + } + match old_tail.and_then(|t| self.links_mut(t)) { + Some(tail) => tail.next = Some(thread), + None => { + if let Some(list) = self.lists.get_mut(idx) { + list.head = Some(thread); + } + } + } + if let Some(list) = self.lists.get_mut(idx) { + list.tail = Some(thread); } - self.lists[idx].tail = Some(thread); self.bitmap |= 1 << idx; true } /// Unlinks `thread` from whichever level it is queued at. pub fn remove(&mut self, thread: ThreadId) -> bool { - let t = thread.raw() as usize; let Some(Links { prev, next, queued_at: Some(level), - }) = self.links.get(t).copied() + }) = self.link(thread).copied() else { return false; }; let idx = level as usize; - match prev { - Some(p) => self.links[p.raw() as usize].next = next, - None => self.lists[idx].head = next, + match prev.and_then(|p| self.links_mut(p)) { + Some(p) => p.next = next, + None => { + if let Some(list) = self.lists.get_mut(idx) { + list.head = next; + } + } } - match next { - Some(n) => self.links[n.raw() as usize].prev = prev, - None => self.lists[idx].tail = prev, + match next.and_then(|n| self.links_mut(n)) { + Some(n) => n.prev = prev, + None => { + if let Some(list) = self.lists.get_mut(idx) { + list.tail = prev; + } + } } - self.links[t] = Links { - prev: None, - next: None, - queued_at: None, - }; - if self.lists[idx].head.is_none() { + if let Some(l) = self.links_mut(thread) { + *l = Links { + prev: None, + next: None, + queued_at: None, + }; + } + if self.lists.get(idx).is_none_or(|l| l.head.is_none()) { self.bitmap &= !(1 << idx); } true } fn pop_level(&mut self, idx: usize) -> Option<(ThreadId, Priority)> { - let thread = self.lists[idx].head?; + let thread = self.lists.get(idx)?.head?; self.remove(thread); Some((thread, Priority::new(idx as u8)?)) } diff --git a/crates/domain/src/scheduler/tests.rs b/crates/domain/src/scheduler/tests.rs index 0bd4b0d..a200a44 100644 --- a/crates/domain/src/scheduler/tests.rs +++ b/crates/domain/src/scheduler/tests.rs @@ -307,3 +307,22 @@ fn run_now_rejects_a_thread_that_is_not_queued() { assert!(!s.run_now(core(0), thread(9))); assert_eq!(s.current(core(0)), None); } + +#[test] +fn an_unknown_core_is_ignored_not_a_panic() { + let mut s = MultiCoreScheduler::new(1); + s.add(thread(1), prio(10), core(200)); + assert_eq!(s.next(core(200)), None); + assert_eq!(s.current(core(200)), None); + s.set_current(core(200), thread(1)); + assert!(!s.run_now(core(200), thread(1))); +} + +#[test] +fn an_out_of_range_thread_id_is_ignored_not_a_panic() { + let mut s = MultiCoreScheduler::new(1); + s.add(thread(60000), prio(10), core(0)); + s.remove(thread(60000)); + assert!(!s.is_queued(thread(60000))); + let _ = s.tick(core(0), thread(60000)); +} diff --git a/crates/domain/src/thread/mod.rs b/crates/domain/src/thread/mod.rs index d8ec382..56e5af7 100644 --- a/crates/domain/src/thread/mod.rs +++ b/crates/domain/src/thread/mod.rs @@ -229,7 +229,7 @@ impl Thread { } } -pub const MAX_THREADS: usize = 256; +pub const MAX_THREADS: usize = if cfg!(kani) { 3 } else { 256 }; pub struct ThreadTable { threads: [Option; MAX_THREADS], @@ -252,7 +252,10 @@ impl ThreadTable { } fn free_slot(&self) -> Option { - (0..MAX_THREADS).find(|&i| self.threads[i].is_none() && self.generations.is_usable(i)) + self.threads + .iter() + .enumerate() + .position(|(i, t)| t.is_none() && self.generations.is_usable(i)) } pub fn spawn( @@ -265,7 +268,10 @@ impl ThreadTable { let idx = self.free_slot().ok_or(KernelError::TooManyThreads)?; let id = ThreadId::from_raw(idx as u16); - self.threads[idx] = Some(Thread::new( + *self + .threads + .get_mut(idx) + .ok_or(KernelError::TooManyThreads)? = Some(Thread::new( id, process, priority, @@ -286,7 +292,10 @@ impl ThreadTable { let idx = self.free_slot().ok_or(KernelError::TooManyThreads)?; let id = ThreadId::from_raw(idx as u16); - self.threads[idx] = Some(Thread::with_context( + *self + .threads + .get_mut(idx) + .ok_or(KernelError::TooManyThreads)? = Some(Thread::with_context( id, process, priority, diff --git a/crates/kernel/src/abi.rs b/crates/kernel/src/abi.rs new file mode 100644 index 0000000..969e039 --- /dev/null +++ b/crates/kernel/src/abi.rs @@ -0,0 +1,157 @@ +//! The syscall register ABI (docs/ipc.md), as pure functions so it can be +//! tested and proved: registers in, `Syscall` out; result out, registers +//! in. Architecture adapters only move registers in and out of a frame. + +use domain::{message::Message, syscall::Syscall}; +use types::{ + address::{DataRef, EntryPoint, StackPointer, VirtualAddress}, + badge::Badge, + bounded::{CapSlot, PageCount}, + permission::PermissionSet, + syscall_abi::*, +}; + +use crate::syscall::{SyscallResult, error_code}; + +fn slot(r: usize) -> Option { + reg_slot(r)? +} + +fn pages(r: usize) -> Option { + PageCount::new(u16::try_from(r).ok()?) +} + +fn permissions(r: usize) -> Option { + Some(PermissionSet::from_bits(u8::try_from(r).ok()?)) +} + +/// The message in `a1..a5`. +fn message(a: &[usize; 6]) -> Option { + let msg = Message::from_words([a[1], a[2], a[3], a[4]]); + Some(match reg_slot(a[5])? { + None => msg, + Some(cap) => msg.with_cap(cap), + }) +} + +/// 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. +pub fn decode(nr: usize, a: &[usize; 6]) -> Option { + Some(match nr { + SYS_EXIT => Syscall::Exit, + SYS_HALT => Syscall::Halt, + SYS_EXIT_THREAD => Syscall::ExitThread, + SYS_YIELD => Syscall::Yield, + SYS_GET_TIME => Syscall::GetTime, + SYS_GET_PROCESS_ID => Syscall::GetProcessId, + SYS_SEND => Syscall::Send { + endpoint: slot(a[0])?, + message: message(a)?, + }, + SYS_CALL => Syscall::Call { + endpoint: slot(a[0])?, + message: message(a)?, + }, + SYS_RECEIVE => Syscall::Receive { + endpoint: slot(a[0])?, + }, + SYS_REPLY => Syscall::Reply { + message: message(a)?, + }, + SYS_REPLY_RECV => Syscall::ReplyRecv { + endpoint: slot(a[0])?, + message: message(a)?, + }, + SYS_DELEGATE => Syscall::Delegate { + slot: slot(a[0])?, + to_endpoint: slot(a[1])?, + permissions: permissions(a[2])?, + }, + SYS_MINT => Syscall::Mint { + slot: slot(a[0])?, + badge: Badge::new(a[1]), + permissions: permissions(a[2])?, + }, + SYS_CREATE_NOTIFICATION => Syscall::CreateNotification, + SYS_SIGNAL => Syscall::Signal { + notification: slot(a[0])?, + }, + SYS_WAIT => Syscall::Wait { + notification: slot(a[0])?, + }, + SYS_POLL => Syscall::Poll { + notification: slot(a[0])?, + }, + SYS_BIND_NOTIFICATION => Syscall::BindNotification { + notification: slot(a[0])?, + }, + SYS_SET_IRQ_NOTIFICATION => Syscall::SetIrqNotification { + irq: slot(a[0])?, + notification: slot(a[1])?, + }, + SYS_ACKNOWLEDGE_INTERRUPT => Syscall::AcknowledgeInterrupt { irq: slot(a[0])? }, + SYS_CREATE_PROCESS => Syscall::CreateProcess { + create_cap: slot(a[0])?, + image: DataRef::empty(), + }, + SYS_KILL => Syscall::Kill { + process: slot(a[0])?, + }, + SYS_REVOKE => Syscall::Revoke { slot: slot(a[0])? }, + SYS_DROP_CAP => Syscall::DropCap { slot: slot(a[0])? }, + SYS_SPAWN_THREAD => Syscall::SpawnThread { + entry: EntryPoint::from_raw(a[0]), + stack: StackPointer::from_raw(a[1]), + }, + SYS_REQUEST_PAGES => Syscall::RequestPages { + count: pages(a[0])?, + }, + SYS_RELEASE_PAGES => Syscall::ReleasePages { + addr: VirtualAddress::from_raw(a[0]), + count: pages(a[1])?, + }, + SYS_SPAWN_THREAD_IN => Syscall::SpawnThreadIn { + process: slot(a[0])?, + entry: EntryPoint::from_raw(a[1]), + stack: StackPointer::from_raw(a[2]), + }, + SYS_CREATE_ENDPOINT => Syscall::CreateEndpoint, + SYS_CREATE_REGION => Syscall::CreateRegion { + pages: pages(a[0])?, + }, + SYS_MAP_REGION => Syscall::MapRegion { + region: slot(a[0])?, + va: VirtualAddress::from_raw(a[1]), + perms: reg_perms(a[2])?, + }, + SYS_DEBUG_PUTCHAR => Syscall::DebugPutchar { byte: a[0] as u8 }, + SYS_MAP_PAGE => Syscall::MapPage { + process: slot(a[0])?, + src_va: VirtualAddress::from_raw(a[1]), + dst_va: VirtualAddress::from_raw(a[2]), + executable: a[3] != 0, + }, + _ => return None, + }) +} + +/// Result registers `a0..a7` for a completed syscall. +pub fn encode(result: &SyscallResult) -> [usize; 8] { + let mut r = [0usize; 8]; + match result { + SyscallResult::Ok => {} + SyscallResult::Value(v) => r[1] = *v, + SyscallResult::Slot(s) => r[1] = s.value() as usize, + SyscallResult::Received(d) => r = delivery_regs(d), + SyscallResult::Error(e) => r[0] = error_code(e) as usize, + } + r +} + +/// Registers for a syscall number that does not decode. +pub fn unknown_syscall() -> [usize; 8] { + let mut r = [0usize; 8]; + r[0] = ErrorCode::UnknownSyscall as usize; + r +} diff --git a/crates/kernel/src/captree.rs b/crates/kernel/src/captree.rs index 7734de4..fae69b3 100644 --- a/crates/kernel/src/captree.rs +++ b/crates/kernel/src/captree.rs @@ -101,8 +101,10 @@ impl Kernel

{ let mut children = [false; ALL_CAPS]; self.for_each_cap(|i, _, cap| { - if cap.parent() == Some(me) { - children[i] = true; + if cap.parent() == Some(me) + && let Some(c) = children.get_mut(i) + { + *c = true; } }); for (i, _) in children.iter().enumerate().filter(|(_, c)| **c) { @@ -131,10 +133,12 @@ impl Kernel

{ // a root rather than trusted. let mut parents: [Option; ALL_CAPS] = [None; ALL_CAPS]; self.for_each_cap(|i, _, cap| { - parents[i] = cap - .parent() - .filter(|r| self.resolves(*r)) - .map(|r| flat(r.process, r.slot) as u16); + if let Some(p) = parents.get_mut(i) { + *p = cap + .parent() + .filter(|r| self.resolves(*r)) + .map(|r| flat(r.process, r.slot) as u16); + } }); let root = flat(pid, slot); let marked = descendants(&parents, root); diff --git a/crates/kernel/src/lib.rs b/crates/kernel/src/lib.rs index 403c87e..21fc436 100644 --- a/crates/kernel/src/lib.rs +++ b/crates/kernel/src/lib.rs @@ -1,5 +1,20 @@ #![no_std] +// A kernel panic takes the whole system down, so kernel code may not +// contain any way to panic. Tests and proofs are exempt. +#![cfg_attr( + not(any(test, kani)), + deny( + clippy::unwrap_used, + clippy::expect_used, + clippy::panic, + clippy::unreachable, + clippy::todo, + clippy::unimplemented, + clippy::indexing_slicing + ) +)] +pub mod abi; mod captree; pub mod interrupt; mod memory; @@ -136,11 +151,11 @@ impl Kernel

{ } pub fn pending_result(&self, thread: ThreadId) -> Option<&SyscallResult> { - self.pending_results[thread.raw() as usize].as_ref() + self.pending_results.get(thread.raw() as usize)?.as_ref() } pub fn take_pending_result(&mut self, thread: ThreadId) -> Option { - self.pending_results[thread.raw() as usize].take() + self.pending_results.get_mut(thread.raw() as usize)?.take() } pub fn set_thread_running( @@ -268,10 +283,8 @@ impl Kernel

{ { Ok(p) => { let mut ids = [None; MAX_THREADS_PER_PROCESS]; - for (i, tid) in p.thread_ids().enumerate() { - if i < MAX_THREADS_PER_PROCESS { - ids[i] = Some(tid); - } + for (slot, tid) in ids.iter_mut().zip(p.thread_ids()) { + *slot = Some(tid); } ids } @@ -292,19 +305,19 @@ impl Kernel

{ for tid in thread_ids.iter().flatten() { self.endpoints.remove_thread_from_all(*tid); self.notifications.remove_thread_from_all(*tid); - let ipc = core::mem::take(&mut self.ipc[tid.raw() as usize]); + 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.scheduler.remove(*tid); - self.pending_results[tid.raw() as usize] = None; + self.set_pending_result(*tid, None); let _ = self.threads.destroy(*tid); } } /// Destroys every endpoint `owner` created, waking anyone blocked on /// them with an error instead of leaving them blocked forever. - fn destroy_endpoints_owned_by(&mut self, owner: ProcessId) { + 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); @@ -330,8 +343,10 @@ impl Kernel

{ let Some(mut n) = self.notifications.destroy(id) else { continue; }; - if let Some(bound) = n.bound() { - self.ipc[bound.raw() as usize].bound = None; + 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); @@ -342,7 +357,9 @@ impl Kernel

{ /// 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) { - self.ipc[tid.raw() as usize].outgoing = None; + if let Some(s) = self.ipc_mut(tid) { + s.outgoing = None; + } self.wake(tid, SyscallResult::Error(error)); } diff --git a/crates/kernel/src/memory.rs b/crates/kernel/src/memory.rs index 877ea3b..0fb32ae 100644 --- a/crates/kernel/src/memory.rs +++ b/crates/kernel/src/memory.rs @@ -124,10 +124,14 @@ impl Kernel

{ } pub(crate) fn create_address_space(&mut self, pid: ProcessId) -> Result<(), KernelError> { - self.quotas[pid.raw() as usize] = Quota::default(); + 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: &mut self.quotas[pid.raw() as usize], + quota, owner: pid, }; let created = self @@ -136,7 +140,9 @@ impl Kernel

{ .map_err(map_error); if created.is_err() { self.frames.free_owned_by(pid); - self.quotas[pid.raw() as usize] = Quota::default(); + if let Some(q) = self.quotas.get_mut(pid.raw() as usize) { + *q = Quota::default(); + } } created } diff --git a/crates/kernel/src/proofs/abi.rs b/crates/kernel/src/proofs/abi.rs new file mode 100644 index 0000000..f131ba0 --- /dev/null +++ b/crates/kernel/src/proofs/abi.rs @@ -0,0 +1,75 @@ +use crate::abi::{decode, encode}; +use crate::syscall::SyscallResult; +use domain::error::KernelError; +use domain::syscall::Syscall; +use types::bounded::CapSlot; +use types::syscall_abi::*; + +/// No register contents can make decoding panic or overflow. +#[kani::proof] +fn decode_is_total() { + let nr: usize = kani::any(); + let args: [usize; 6] = kani::any(); + let _ = decode(nr, &args); +} + +/// A decoded slot argument is exactly the register it came from. +#[kani::proof] +fn decoded_slots_match_their_registers() { + let args: [usize; 6] = kani::any(); + if let Some(Syscall::Receive { endpoint }) = decode(SYS_RECEIVE, &args) { + assert!(endpoint.value() as usize == args[0]); + } + if let Some(Syscall::Delegate { + slot, to_endpoint, .. + }) = decode(SYS_DELEGATE, &args) + { + assert!(slot.value() as usize == args[0]); + assert!(to_endpoint.value() as usize == args[1]); + } +} + +/// What libkos encodes for a Send is decoded back to the same message. +#[kani::proof] +fn send_roundtrips() { + let ep = CapSlot::new(kani::any::() % (CapSlot::MAX + 1)).unwrap(); + let words: [usize; 4] = kani::any(); + let cap = if kani::any() { + CapSlot::new(kani::any::() % (CapSlot::MAX + 1)) + } else { + None + }; + let regs = message_regs(ep.value() as usize, words, cap); + match decode(SYS_SEND, ®s) { + Some(Syscall::Send { endpoint, message }) => { + assert!(endpoint == ep); + assert!(*message.words() == words); + assert!(message.cap() == cap); + } + _ => panic!("valid send did not decode"), + } +} + +/// A failed syscall always reports a real, non-zero error code. +#[kani::proof] +fn errors_encode_to_valid_codes() { + let e = match kani::any::() % 6 { + 0 => KernelError::NoReply, + 1 => KernelError::OutOfMemory, + 2 => KernelError::InvalidAddress, + 3 => KernelError::WrongObject, + 4 => KernelError::NoSuchObject, + _ => KernelError::InvalidSlot(CapSlot::new(0).unwrap()), + }; + let regs = encode(&SyscallResult::Error(e)); + assert!(regs[0] != 0); + assert!(ErrorCode::from_raw(regs[0]).is_some()); +} + +#[kani::proof] +fn successes_report_status_zero() { + let v: usize = kani::any(); + assert!(encode(&SyscallResult::Ok)[0] == 0); + let regs = encode(&SyscallResult::Value(v)); + assert!(regs[0] == 0 && regs[1] == v); +} diff --git a/crates/kernel/src/proofs/authority.rs b/crates/kernel/src/proofs/authority.rs new file mode 100644 index 0000000..79c744c --- /dev/null +++ b/crates/kernel/src/proofs/authority.rs @@ -0,0 +1,118 @@ +//! 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. + +use super::platform::KaniPlatform; +use crate::Kernel; +use domain::{capability::MAX_CAPS_PER_PROCESS, process::MAX_PROCESSES, resource::Resource}; +use types::{ + address::PhysicalAddress, + badge::Badge, + bounded::{CapSlot, Priority}, + id::ProcessId, + permission::PermissionSet, + time::TimeSlice, +}; + +#[derive(Clone, Copy, PartialEq)] +struct Held { + resource: Resource, + perms: PermissionSet, + badge: Badge, +} + +type Snapshot = [[Option; MAX_CAPS_PER_PROCESS]; MAX_PROCESSES]; + +fn snapshot(k: &Kernel) -> Snapshot { + let mut s = [[None; MAX_CAPS_PER_PROCESS]; MAX_PROCESSES]; + for (p, row) in s.iter_mut().enumerate() { + if let Ok(process) = k.processes.get(ProcessId::from_raw(p as u16)) { + for (slot, cap) in process.capabilities().iter() { + row[slot.value() as usize] = Some(Held { + resource: *cap.resource(), + perms: *cap.permissions(), + badge: cap.badge(), + }); + } + } + } + s +} + +/// Whether `resource` named a live object before the operation. +fn existed(before: &Snapshot, resource: &Resource) -> bool { + before + .iter() + .flatten() + .flatten() + .any(|h| h.resource == *resource) +} + +/// Some capability before the operation already granted at least `h`. +fn justified(before: &Snapshot, h: &Held) -> bool { + before.iter().flatten().flatten().any(|b| { + b.resource == h.resource + && h.perms.is_subset_of(&b.perms) + && (b.badge == h.badge || b.badge.is_none()) + }) +} + +fn any_perms() -> PermissionSet { + PermissionSet::from_bits(kani::any::() & 0b1111) +} + +fn any_slot() -> CapSlot { + CapSlot::new(kani::any::() % (CapSlot::MAX + 1)).unwrap() +} + +/// Init and one more process, an endpoint, a notification, and caps with +/// arbitrary rights spread over both, including a cap to the other process. +fn small_world() -> Kernel { + let mut k = Kernel::new(KaniPlatform, PhysicalAddress::from_raw(0x8400_0000), 6); + let (init, _) = k.boot(Priority::DEFAULT, TimeSlice::DEFAULT).unwrap(); + let b = k.create_process_internal().unwrap(); + k.spawn_thread_internal(b).unwrap(); + let ep = k.create_endpoint(init).unwrap(); + let n = k.create_notification(b).unwrap(); + k.grant_capability(init, Resource::Endpoint(ep), any_perms()) + .unwrap(); + k.grant_capability(init, Resource::Process(b), any_perms()) + .unwrap(); + k.grant_capability(b, Resource::Endpoint(ep), any_perms()) + .unwrap(); + k.grant_capability(b, Resource::Notification(n), any_perms()) + .unwrap(); + k +} + +/// The caller is concrete: a symbolic pid turns every table lookup into a +/// symbolic index and blows CBMC's formula up past 30 GB. +#[kani::proof] +#[kani::unwind(8)] +fn mint_creates_no_authority() { + let mut k = small_world(); + let (slot, badge, perms) = (any_slot(), Badge::new(kani::any()), any_perms()); + let before = snapshot(&k); + let _ = k.mint(ProcessId::from_raw(0), slot, badge, perms); + let after = snapshot(&k); + for (p, row) in after.iter().enumerate() { + for (s, held) in row.iter().enumerate() { + let Some(h) = held else { continue }; + if before[p][s] == Some(*h) { + continue; // untouched + } + if existed(&before, &h.resource) { + assert!(justified(&before, h), "authority appeared from nowhere"); + } + } + } +} diff --git a/crates/kernel/src/proofs/delegation.rs b/crates/kernel/src/proofs/delegation.rs index 459080b..554d010 100644 --- a/crates/kernel/src/proofs/delegation.rs +++ b/crates/kernel/src/proofs/delegation.rs @@ -25,7 +25,7 @@ fn kernel_delegate_path_never_escalates() { let original_perms = *cap.permissions(); let restricted = original_perms.restrict_to(&PermissionSet::from_bits(restrict_bits)); - let delegated = Capability::new(cap.resource().clone(), restricted, Generation::initial()); + let delegated = Capability::new(*cap.resource(), restricted, Generation::initial()); let mut target_table = CapabilityTable::new(); let target_slot = insert_cap(&mut target_table, delegated); @@ -69,7 +69,7 @@ fn kernel_chained_delegate_never_escalates() { .restrict_to(&PermissionSet::from_bits(restrict1_bits)); let mut table_b = CapabilityTable::new(); - let cap_b = Capability::new(resource.clone(), perms_for_b, Generation::initial()); + let cap_b = Capability::new(resource, perms_for_b, Generation::initial()); let slot_b = insert_cap(&mut table_b, cap_b); let cap_in_b = table_b.get(slot_b).unwrap(); diff --git a/crates/kernel/src/proofs/mediation.rs b/crates/kernel/src/proofs/mediation.rs index 3a277ed..4da9257 100644 --- a/crates/kernel/src/proofs/mediation.rs +++ b/crates/kernel/src/proofs/mediation.rs @@ -38,7 +38,7 @@ fn handle_receive_rejects_without_read_permission() { #[kani::proof] fn missing_cap_always_rejected() { let slot_val: u8 = kani::any(); - kani::assume(slot_val <= 63); + kani::assume(slot_val <= CapSlot::MAX); let slot = CapSlot::new(slot_val).unwrap(); let table = CapabilityTable::new(); diff --git a/crates/kernel/src/proofs/mod.rs b/crates/kernel/src/proofs/mod.rs index a3551d3..9bee150 100644 --- a/crates/kernel/src/proofs/mod.rs +++ b/crates/kernel/src/proofs/mod.rs @@ -1,6 +1,9 @@ +mod abi; +mod authority; mod delegation; mod mediation; mod message; +mod platform; mod revocation; use domain::capability::{Capability, CapabilityTable}; diff --git a/crates/kernel/src/proofs/platform.rs b/crates/kernel/src/proofs/platform.rs new file mode 100644 index 0000000..71850f0 --- /dev/null +++ b/crates/kernel/src/proofs/platform.rs @@ -0,0 +1,62 @@ +//! A platform with no hardware behind it, for running the real kernel +//! under Kani. Page tables cost one frame per address space. + +use platform::{FrameSource, MapError, Platform}; +use types::{ + address::{EntryPoint, PhysicalAddress, StackPointer, VirtualAddress}, + id::{CoreId, IrqId, ProcessId}, + mapping::PagePerms, + time::{Ticks, TimerDuration}, +}; + +pub struct KaniPlatform; + +impl Platform for KaniPlatform { + const USER_VA_START: usize = 0x1000; + const USER_VA_END: usize = 0x0200_0000; + + fn create_address_space( + &mut self, + _process: ProcessId, + frames: &mut dyn FrameSource, + ) -> Result<(), MapError> { + frames.alloc_table_frame().ok_or(MapError::OutOfFrames)?; + Ok(()) + } + fn destroy_address_space(&mut self, _process: ProcessId) {} + fn map_page( + &mut self, + _process: ProcessId, + _va: VirtualAddress, + _pa: PhysicalAddress, + _perms: PagePerms, + _frames: &mut dyn FrameSource, + ) -> Result<(), MapError> { + Ok(()) + } + fn unmap_page(&mut self, _process: ProcessId, _va: VirtualAddress) {} + fn zero_frame(&mut self, _pa: PhysicalAddress) {} + fn enable_user_mode(&mut self, _entry: EntryPoint, _stack: StackPointer) -> ! { + kani::assume(false); + loop {} + } + fn set_timer(&mut self, _duration: TimerDuration) {} + fn current_ticks(&self) -> Ticks { + Ticks::from_raw(0) + } + fn mask_irq(&mut self, _irq: IrqId) {} + fn unmask_irq(&mut self, _irq: IrqId) {} + fn send_ipi(&mut self, _target: CoreId) {} + fn core_id(&self) -> CoreId { + CoreId::from_raw(0) + } + fn num_cores(&self) -> u8 { + 1 + } + fn halt(&self) -> ! { + // Halting ends the run; there is no state after it to check. + kani::assume(false); + loop {} + } + fn debug_putchar(&self, _byte: u8) {} +} diff --git a/crates/kernel/src/syscall/capability.rs b/crates/kernel/src/syscall/capability.rs index d6f4d4a..9181512 100644 --- a/crates/kernel/src/syscall/capability.rs +++ b/crates/kernel/src/syscall/capability.rs @@ -15,7 +15,7 @@ impl Kernel

{ // travel with it; only the permissions narrow. let copy = match self.check_cap(caller_pid, slot, types::permission::Permission::Delegate) { Ok(cap) => domain::capability::Capability::new( - cap.resource().clone(), + *cap.resource(), cap.permissions().restrict_to(&restrict), *cap.generation(), ) diff --git a/crates/kernel/src/syscall/ipc.rs b/crates/kernel/src/syscall/ipc.rs index 46fa2f5..b571bcb 100644 --- a/crates/kernel/src/syscall/ipc.rs +++ b/crates/kernel/src/syscall/ipc.rs @@ -56,6 +56,20 @@ fn rw_delegate() -> PermissionSet { } 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, @@ -87,7 +101,7 @@ impl Kernel

{ }; let priority = thread.priority(); if thread.unblock().is_ok() { - self.pending_results[tid.raw() as usize] = Some(result); + self.set_pending_result(tid, Some(result)); let core = self.platform.core_id(); self.scheduler.add(tid, priority, core); } @@ -170,7 +184,10 @@ impl Kernel

{ _ => None, }; if kind == DeliveryKind::Call { - self.ipc[receiver.raw() as usize].reply_to = self.thread_ref(sender); + let caller = self.thread_ref(sender); + if let Some(s) = self.ipc_mut(receiver) { + s.reply_to = caller; + } } Delivery { kind, @@ -237,7 +254,9 @@ impl Kernel

{ if !queued { return SyscallOutcome::Complete(SyscallResult::Error(KernelError::EndpointFull)); } - self.ipc[tid.raw() as usize].outgoing = Some(out); + if let Some(s) = self.ipc_mut(tid) { + s.outgoing = Some(out); + } let reason = if is_call { BlockReason::Calling(ep) } else { @@ -258,11 +277,11 @@ impl Kernel

{ Ok(v) => v, Err(e) => return SyscallOutcome::Complete(SyscallResult::Error(e)), }; - if drop_reply && let Some(pending) = self.ipc[tid.raw() as usize].reply_to.take() { + if drop_reply && let Some(pending) = self.ipc_mut(tid).and_then(|s| s.reply_to.take()) { self.release_caller(pending); } - if let Some(n) = self.ipc[tid.raw() as usize].bound + if let Some(n) = self.ipc(tid).and_then(|s| s.bound) && let Some(ntfn) = self.notifications.get_mut(n) && ntfn.has_bits() { @@ -273,7 +292,7 @@ impl Kernel

{ let sender = self.endpoints.get_mut(ep).and_then(|e| e.dequeue_sender()); if let Some(sender) = sender { let is_call = self.is_blocked_as(sender, |r| matches!(r, BlockReason::Calling(_))); - let Some(out) = self.ipc[sender.raw() as usize].outgoing.take() else { + let Some(out) = self.ipc_mut(sender).and_then(|s| s.outgoing.take()) else { // A queued sender always has a message; treat a missing one // as a sender that vanished. return SyscallOutcome::Complete(SyscallResult::Error(KernelError::WouldBlock)); @@ -310,9 +329,9 @@ impl Kernel

{ pid: ProcessId, message: Message, ) -> Result<(), KernelError> { - let caller = self.ipc[tid.raw() as usize] - .reply_to - .take() + let caller = self + .ipc_mut(tid) + .and_then(|s| s.reply_to.take()) .ok_or(KernelError::NoReply)?; let waiting = self.is_live(caller) && self.is_blocked_as(caller.tid, |r| *r == BlockReason::AwaitingReply); @@ -343,7 +362,7 @@ impl Kernel

{ if let Err(e) = self.endpoint_cap(pid, slot, Permission::Read) { return SyscallOutcome::Complete(SyscallResult::Error(e)); } - if self.ipc[tid.raw() as usize].reply_to.is_some() { + if self.ipc(tid).is_some_and(|s| s.reply_to.is_some()) { let _ = self.reply(tid, pid, message); } self.receive(tid, pid, slot, false) @@ -367,7 +386,7 @@ impl Kernel

{ return Err(KernelError::InvalidArgument); } let minted = Capability::new( - source.resource().clone(), + *source.resource(), source.permissions().restrict_to(&permissions), *source.generation(), ) @@ -475,7 +494,7 @@ impl Kernel

{ slot: CapSlot, ) -> Result<(), KernelError> { let (id, _, _) = self.notification_cap(pid, slot, Permission::Read)?; - if self.ipc[tid.raw() as usize].bound.is_some() { + if self.ipc(tid).is_none_or(|s| s.bound.is_some()) { return Err(KernelError::InvalidArgument); } let ntfn = self @@ -485,7 +504,9 @@ impl Kernel

{ if !ntfn.bind(tid) { return Err(KernelError::InvalidArgument); } - self.ipc[tid.raw() as usize].bound = Some(id); + if let Some(s) = self.ipc_mut(tid) { + s.bound = Some(id); + } Ok(()) } diff --git a/crates/kernel/src/syscall/mod.rs b/crates/kernel/src/syscall/mod.rs index 6e6c080..f1067fa 100644 --- a/crates/kernel/src/syscall/mod.rs +++ b/crates/kernel/src/syscall/mod.rs @@ -12,6 +12,7 @@ use types::{bounded::CapSlot, id::ThreadId, syscall_abi::ErrorCode}; use crate::Kernel; pub use ipc::{IpcState, ThreadRef}; +pub use types::syscall_abi::{Delivery, DeliveryKind}; pub enum SyscallOutcome { Complete(SyscallResult), @@ -21,38 +22,6 @@ pub enum SyscallOutcome { TerminateCaller, } -#[derive(Debug, Clone, Copy, PartialEq, Eq)] -pub enum DeliveryKind { - /// A `Send`; no reply expected. - Message, - /// A `Call`; the receiver's reply slot now names the caller. - Call, - /// Notification bits. - Signal, -} - -/// What a receiving syscall hands back (docs/ipc.md, register ABI). -#[derive(Debug, Clone, Copy, PartialEq, Eq)] -pub struct Delivery { - pub kind: DeliveryKind, - /// The sender's badge, or the signal bits. - pub badge: usize, - pub words: [usize; 4], - /// Where a transferred capability landed in the receiver's table. - pub cap: Option, -} - -impl Delivery { - pub fn signal(bits: usize) -> Self { - Self { - kind: DeliveryKind::Signal, - badge: bits, - words: [0; 4], - cap: None, - } - } -} - #[derive(Debug)] pub enum SyscallResult { Ok, diff --git a/crates/kernel/src/tests/abi.rs b/crates/kernel/src/tests/abi.rs new file mode 100644 index 0000000..9e6b215 --- /dev/null +++ b/crates/kernel/src/tests/abi.rs @@ -0,0 +1,99 @@ +use crate::abi::{decode, encode, unknown_syscall}; +use crate::syscall::SyscallResult; +use domain::syscall::Syscall; +use types::syscall_abi::*; + +/// Every syscall number the ABI defines decodes with ordinary arguments, +/// so the decoder cannot silently drop one. +#[test] +fn every_defined_syscall_decodes() { + let numbers = [ + SYS_SEND, + SYS_RECEIVE, + SYS_DELEGATE, + SYS_ACKNOWLEDGE_INTERRUPT, + SYS_CREATE_PROCESS, + SYS_KILL, + SYS_REVOKE, + SYS_SPAWN_THREAD, + SYS_EXIT_THREAD, + SYS_REQUEST_PAGES, + SYS_RELEASE_PAGES, + SYS_GET_TIME, + SYS_GET_PROCESS_ID, + SYS_YIELD, + SYS_EXIT, + SYS_HALT, + SYS_CREATE_ENDPOINT, + SYS_DEBUG_PUTCHAR, + SYS_MAP_PAGE, + SYS_SPAWN_THREAD_IN, + SYS_DROP_CAP, + SYS_CALL, + SYS_REPLY, + SYS_REPLY_RECV, + SYS_MINT, + SYS_CREATE_NOTIFICATION, + SYS_SIGNAL, + SYS_WAIT, + SYS_POLL, + SYS_BIND_NOTIFICATION, + SYS_SET_IRQ_NOTIFICATION, + SYS_CREATE_REGION, + SYS_MAP_REGION, + ]; + // slot 1, slot 2, small values, no cap + let args = [1, 2, 1, 0, 0, NONE]; + for nr in numbers { + assert!(decode(nr, &args).is_some(), "syscall {nr} does not decode"); + } +} + +#[test] +fn retired_and_unknown_numbers_do_not_decode() { + for nr in [3, 5, 35, 1000, usize::MAX] { + assert!(decode(nr, &[0; 6]).is_none(), "{nr} decoded"); + } +} + +#[test] +fn out_of_range_arguments_do_not_decode() { + assert!(decode(SYS_RECEIVE, &[64, 0, 0, 0, 0, 0]).is_none()); + assert!( + decode(SYS_SEND, &[1, 0, 0, 0, 0, 64]).is_none(), + "bad cap slot" + ); + assert!( + decode(SYS_REQUEST_PAGES, &[0, 0, 0, 0, 0, 0]).is_none(), + "zero pages" + ); + assert!(decode(SYS_REQUEST_PAGES, &[1025, 0, 0, 0, 0, 0]).is_none()); + assert!( + decode(SYS_MAP_REGION, &[1, 0x30000, 3, 0, 0, 0]).is_none(), + "bad perms" + ); + assert!( + decode(SYS_DELEGATE, &[1, 2, 256, 0, 0, 0]).is_none(), + "perm bits overflow u8" + ); +} + +#[test] +fn none_means_no_capability() { + match decode(SYS_SEND, &[1, 9, 8, 7, 6, NONE]) { + Some(Syscall::Send { message, .. }) => { + assert_eq!(message.cap(), None); + assert_eq!(message.words(), &[9, 8, 7, 6]); + } + _ => panic!("send did not decode"), + } +} + +#[test] +fn results_follow_the_status_convention() { + assert_eq!(encode(&SyscallResult::Ok), [0; 8]); + assert_eq!(encode(&SyscallResult::Value(7))[..2], [0, 7]); + let err = encode(&SyscallResult::Error(domain::error::KernelError::NoReply)); + assert_eq!(err[0], ErrorCode::NoReply as usize); + assert_eq!(unknown_syscall()[0], ErrorCode::UnknownSyscall as usize); +} diff --git a/crates/kernel/src/tests/helpers.rs b/crates/kernel/src/tests/helpers.rs index 86f1a22..6170ce9 100644 --- a/crates/kernel/src/tests/helpers.rs +++ b/crates/kernel/src/tests/helpers.rs @@ -144,6 +144,27 @@ impl Kernel { } } + /// Whether `slot` of `pid` holds a capability whose object is gone. + pub fn is_dead_cap_for_test(&self, pid: ProcessId, slot: CapSlot) -> bool { + let Ok(p) = self.processes.get(pid) else { + return false; + }; + p.capabilities() + .get(slot) + .is_ok_and(|c| self.resource_generation(c.resource()) != Some(*c.generation())) + } + + /// Whether `slot` of `pid` holds a capability to a process that is gone. + pub fn is_dead_process_cap_for_test(&self, pid: ProcessId, slot: CapSlot) -> bool { + let Ok(p) = self.processes.get(pid) else { + return false; + }; + match p.capabilities().get(slot).map(|c| *c.resource()) { + Ok(Resource::Process(target)) => !self.process_exists(target), + _ => false, + } + } + /// Which slots of `pid`'s capability table are occupied. pub fn cap_slots_for_test(&self, pid: ProcessId) -> [bool; 64] { let mut used = [false; 64]; diff --git a/crates/kernel/src/tests/mod.rs b/crates/kernel/src/tests/mod.rs index 19c372e..b7e2569 100644 --- a/crates/kernel/src/tests/mod.rs +++ b/crates/kernel/src/tests/mod.rs @@ -1,6 +1,7 @@ mod helpers; mod mock_platform; +mod abi; mod capability; mod captree_model; mod exit; @@ -13,6 +14,7 @@ mod lifetimes; mod memory; mod revocation; mod simple; +mod storm; mod tick; pub use helpers::{kernel_with_process, test_kernel}; diff --git a/crates/kernel/src/tests/storm.rs b/crates/kernel/src/tests/storm.rs new file mode 100644 index 0000000..c507a7c --- /dev/null +++ b/crates/kernel/src/tests/storm.rs @@ -0,0 +1,429 @@ +//! Global kernel invariants, and a storm of random syscalls with random +//! (mostly garbage) arguments decoded through the real ABI. The kernel must +//! never panic and every invariant must hold after every single call. + +extern crate std; + +use std::format; +use std::string::String; + +use super::*; +use crate::syscall::ThreadRef; +use domain::memory::{RegionBacking, frame::FrameUse}; +use domain::thread::{BlockReason, MAX_THREADS, ThreadState}; +use platform::Platform; +use types::address::DataRef; +use types::bounded::CapSlot; +use types::id::ThreadId; +use types::syscall_abi::*; + +impl Kernel { + fn live_threads(&self) -> impl Iterator + '_ { + (0..MAX_THREADS as u16) + .map(ThreadId::from_raw) + .filter(|t| self.threads.get(*t).is_ok()) + } + + /// Every invariant the kernel promises, over every live object. + pub fn check_invariants(&self) -> Result<(), String> { + // ---- memory ---- + let mut charged = 0; + for p in 0..domain::process::MAX_PROCESSES as u16 { + let pid = ProcessId::from_raw(p); + let usage = self.page_usage(pid); + charged += usage; + let owned = self + .frames + .iter() + .filter(|(_, u)| { + matches!(u, FrameUse::User { owner, .. } | FrameUse::PageTable { owner } if *owner == pid) + }) + .count(); + let regions: usize = self + .regions + .iter() + .filter(|(_, r)| r.owner() == pid && r.backing() == RegionBacking::Pool) + .map(|(_, r)| r.pages().value() as usize) + .sum(); + if usage != owned + regions { + return Err(format!( + "quota of {pid:?} is {usage}, owns {owned}+{regions}" + )); + } + if !self.process_exists(pid) && (usage != 0 || self.platform.mapping_count(pid) != 0) { + return Err(format!("dead {pid:?} still holds memory")); + } + } + if charged + self.free_page_count() != self.frames.capacity() { + return Err(String::from("frames leaked or double counted")); + } + let window = MockPlatform::USER_VA_START..MockPlatform::USER_VA_END; + for (pid, va, pa) in self.platform.mappings() { + if !window.contains(&va) { + return Err(format!("{pid:?} mapped outside the window at {va:#x}")); + } + let v = types::address::VirtualAddress::from_raw(va); + let user = self.frames.find_user(pid, v).map(|(p, _)| p.raw()); + let region = self.regions.covering(pid, v).and_then(|id| { + let r = self.regions.get(id)?; + let m = r.mappings().find(|m| m.process == pid)?; + Some(r.base().raw() + (va - m.va.raw())) + }); + if user != Some(pa) && region != Some(pa) { + return Err(format!("{pid:?} has unrecorded mapping {va:#x}")); + } + } + for (pa, usage) in self.frames.iter() { + if let FrameUse::User { owner, page, .. } = usage + && self.platform.mapping(*owner, *page as usize * 4096) != Some(pa.raw()) + { + return Err(String::from("recorded user page is not mapped")); + } + } + + // ---- capabilities ---- + for p in 0..domain::process::MAX_PROCESSES as u16 { + let pid = ProcessId::from_raw(p); + let Ok(process) = self.processes.get(pid) else { + continue; + }; + for (slot, cap) in process.capabilities().iter() { + if let Some(parent) = cap.parent() + && !self.resolves(parent) + { + return Err(format!("{pid:?}/{slot:?} has a dangling parent")); + } + } + } + for (_, region) in self.regions.iter() { + for m in region.mappings() { + if let Some(via) = m.via + && (!self.resolves(via) || via.process != m.process) + { + return Err(String::from("mapping outlived its capability")); + } + } + } + + // ---- queues hold only live threads blocked on that very object ---- + let blocked_as = |t: ThreadId, want: BlockReason| { + self.threads.get(t).ok().map(|x| *x.state()) == Some(ThreadState::Blocked(want)) + }; + for ep in self.endpoints.iter() { + let id = *ep.id(); + for t in ep.senders() { + if !blocked_as(t, BlockReason::Sending(id)) + && !blocked_as(t, BlockReason::Calling(id)) + { + return Err(format!( + "{t:?} queued as a sender on {id:?} but not blocked there" + )); + } + } + for t in ep.receivers() { + if !blocked_as(t, BlockReason::Receiving(id)) { + return Err(format!( + "{t:?} queued as a receiver on {id:?} but not blocked there" + )); + } + } + } + for n in self.notifications.iter() { + for t in n.waiters() { + if !blocked_as(t, BlockReason::WaitingNotification(n.id())) { + return Err(format!( + "{t:?} waits on {:?} but is not blocked there", + n.id() + )); + } + } + if let Some(b) = n.bound() + && self.ipc.get(b.raw() as usize).and_then(|s| s.bound) != Some(n.id()) + { + return Err(format!( + "{:?} bound to {b:?} which does not know it", + n.id() + )); + } + } + + // ---- threads, IPC, scheduling ---- + for t in self.live_threads() { + let Ok(thread) = self.threads.get(t) else { + continue; + }; + let state = *thread.state(); + if !self.process_exists(thread.process()) { + return Err(format!("{t:?} outlived its process")); + } + let ipc = self.ipc[t.raw() as usize]; + let in_endpoint = |e: types::id::EndpointId| { + self.endpoints + .get(e) + .map(|ep| (ep.is_sender(t), ep.is_receiver(t))) + }; + match state { + ThreadState::Blocked(BlockReason::Sending(e) | BlockReason::Calling(e)) => { + if in_endpoint(e) != Some((true, false)) || ipc.outgoing.is_none() { + return Err(format!("{t:?} blocked sending but not queued")); + } + } + ThreadState::Blocked(BlockReason::Receiving(e)) => { + if in_endpoint(e) != Some((false, true)) { + return Err(format!("{t:?} blocked receiving but not queued")); + } + } + ThreadState::Blocked(BlockReason::WaitingNotification(n)) => { + if !self.notifications.get(n).is_some_and(|x| x.is_waiter(t)) { + return Err(format!("{t:?} waits on a notification it is not queued on")); + } + } + ThreadState::Blocked(BlockReason::AwaitingReply) => { + let me = ThreadRef { + tid: t, + generation: self + .threads + .generation(t) + .unwrap_or(types::generation::Generation::initial()), + }; + let holders = self + .live_threads() + .filter(|s| self.ipc[s.raw() as usize].reply_to == Some(me)) + .count(); + if holders != 1 { + return Err(format!("{t:?} awaits a reply held by {holders} threads")); + } + } + _ => { + if ipc.outgoing.is_some() { + return Err(format!("{t:?} runnable with a queued message")); + } + } + } + if self.scheduler.is_queued(t) != matches!(state, ThreadState::Ready) { + return Err(format!("{t:?} in {state:?} has wrong run-queue membership")); + } + if let Some(r) = ipc.reply_to + && self.threads.generation(r.tid) == Some(r.generation) + && self.threads.get(r.tid).ok().map(|x| *x.state()) + != Some(ThreadState::Blocked(BlockReason::AwaitingReply)) + { + return Err(format!("{t:?} holds a reply for a thread not waiting")); + } + } + Ok(()) + } +} + +struct Rng(u64); + +impl Rng { + fn next(&mut self) -> u64 { + self.0 ^= self.0 << 13; + self.0 ^= self.0 >> 7; + self.0 ^= self.0 << 17; + self.0 + } + + fn below(&mut self, n: usize) -> usize { + (self.next() % n as u64) as usize + } + + /// An argument that is usually meaningful and sometimes garbage. + fn arg(&mut self) -> usize { + match self.below(9) { + 0..=2 => self.below(8), // small slots and counts + 8 => self.below(3), // the first few slots + 3 => NONE, + 4 => 0x40000 + self.below(64) * 4096, // heap-ish addresses + 5 => 0x10000 + self.below(32) * 4096, + 6 => self.below(70), // slots just past the end + _ => self.next() as usize, // anything at all + } + } +} + +/// 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. +fn new_round(k: &mut Kernel, init: ProcessId, init_thread: ThreadId) { + use domain::resource::Resource; + let all = types::permission::PermissionSet::empty() + .with(types::permission::Permission::Read) + .with(types::permission::Permission::Write) + .with(types::permission::Permission::Execute) + .with(types::permission::Permission::Delegate); + // init's caps to anything that died last round would fill its table. + for slot in 1..=CapSlot::MAX { + let slot = CapSlot::new(slot).unwrap(); + if k.is_dead_cap_for_test(init, slot) { + let _ = k.delete_cap(init, slot); + } + } + let Some(hub) = k.create_process_internal() else { + if std::env::var("STORM_DEBUG").is_ok() { + std::eprintln!("no hub: free pages {}", k.free_page_count()); + } + return; + }; + let (Ok(e0), Ok(e1), Ok(n)) = ( + k.create_endpoint(hub), + k.create_endpoint(hub), + k.create_notification(hub), + ) else { + return; + }; + let region = k + .create_pool_region(hub, types::bounded::PageCount::new(2).unwrap()) + .ok(); + let mut members = std::vec![init]; + for _ in 0..2 { + k.switch_to_thread_for_test(init_thread); + if let crate::SyscallOutcome::Complete(crate::SyscallResult::Slot(cap)) = + k.handle_syscall(domain::syscall::Syscall::CreateProcess { + create_cap: CapSlot::new(0).unwrap(), + image: DataRef::empty(), + }) + { + let pid = k.process_of_cap_for_test(cap); + for _ in 0..2 { + k.spawn_thread_for_test(pid, Priority::DEFAULT, TimeSlice::DEFAULT); + } + members.push(pid); + } else if std::env::var("STORM_DEBUG").is_ok() { + std::eprintln!( + "create child failed; init thread state {:?}", + k.thread_state_for_test(init_thread) + ); + } + } + for pid in members { + for ep in [e0, e1] { + let _ = k.grant_capability(pid, Resource::Endpoint(ep), all); + } + let _ = k.grant_capability(pid, Resource::Notification(n), all); + if let Some(r) = region { + let _ = k.grant_capability(pid, Resource::Memory(r), all); + } + } +} + +#[test] +fn the_kernel_survives_a_syscall_storm() { + let mut total = [0usize; 36]; + for seed in [17u64, 0xABCD_EF01, 4242, 0x1357_9BDF, 8] { + let (mut k, init) = kernel_with_process(); + let init_thread = k.current_thread().unwrap(); + k.spawn_thread_for_test(init, Priority::DEFAULT, TimeSlice::DEFAULT); + let mut rng = Rng(seed); + let mut executed = 0; + let mut rounds = 0; + let mut succeeded = [0usize; 36]; + new_round(&mut k, init, init_thread); + + let mut step = 0; + while executed < 4000 && step < 200_000 { + step += 1; + let runnable: std::vec::Vec = k + .live_threads() + .filter(|t| { + matches!( + k.thread_state_for_test(*t), + Some(ThreadState::Ready | ThreadState::Running(_)) + ) + }) + .collect(); + if runnable.is_empty() || rng.below(300) == 0 { + // Kill everyone but init, hub included: destroying the shared + // objects wakes whoever was blocked on them. + for p in 1..domain::process::MAX_PROCESSES as u16 { + k.destroy_process(ProcessId::from_raw(p)); + } + // init may be blocked on objects it made itself. + k.destroy_endpoints_owned_by(init); + k.destroy_notifications_owned_by(init); + k.check_invariants() + .unwrap_or_else(|e| panic!("seed {seed:#x} step {step} after teardown: {e}")); + new_round(&mut k, init, init_thread); + rounds += 1; + continue; + } + let tid = runnable[rng.below(runnable.len())]; + let is_init = k.thread_process(tid) == Some(init); + let nr = rng.below(36); + // Halting stops the machine and init exiting ends the test. + if nr == SYS_HALT || (is_init && (nr == SYS_EXIT || nr == SYS_EXIT_THREAD)) { + continue; + } + let args: [usize; 6] = core::array::from_fn(|_| rng.arg()); + // init keeps the capability it creates processes with. + if is_init && nr == SYS_DROP_CAP && args[0] == 0 { + continue; + } + let Some(syscall) = crate::abi::decode(nr, &args) else { + continue; + }; + k.switch_to_thread_for_test(tid); + k.take_pending_result(tid); + let out = k.handle_syscall(syscall); + executed += 1; + if !matches!( + out, + crate::SyscallOutcome::Complete(crate::SyscallResult::Error(_)) + ) { + succeeded[nr] += 1; + } + k.check_invariants() + .unwrap_or_else(|e| panic!("seed {seed:#x} step {step} (syscall {nr}): {e}")); + assert!( + k.process_exists(init), + "seed {seed:#x}: init died at step {step}" + ); + } + if std::env::var("STORM_STATS").is_ok() { + std::eprintln!( + "seed {seed:#x}: executed {executed} rounds {rounds} ok per syscall {succeeded:?}" + ); + } + assert!( + executed >= 4000, + "seed {seed:#x}: only {executed} syscalls ran" + ); + assert!( + rounds < executed / 4, + "seed {seed:#x}: rounds too short ({rounds} rounds)" + ); + for (t, n) in total.iter_mut().zip(succeeded) { + *t += n; + } + } + let exercised = [ + SYS_SEND, + SYS_RECEIVE, + SYS_CALL, + SYS_REPLY, + SYS_REPLY_RECV, + SYS_SIGNAL, + SYS_WAIT, + SYS_POLL, + SYS_BIND_NOTIFICATION, + SYS_MINT, + SYS_DELEGATE, + SYS_REVOKE, + SYS_DROP_CAP, + SYS_REQUEST_PAGES, + SYS_RELEASE_PAGES, + SYS_CREATE_REGION, + SYS_MAP_REGION, + SYS_KILL, + SYS_CREATE_PROCESS, + SYS_SPAWN_THREAD, + SYS_SPAWN_THREAD_IN, + ]; + for nr in exercised { + assert!( + total[nr] > 0, + "syscall {nr} never succeeded in the whole storm" + ); + } +} diff --git a/crates/libkos/src/syscall.rs b/crates/libkos/src/syscall.rs index 937708e..dc857d6 100644 --- a/crates/libkos/src/syscall.rs +++ b/crates/libkos/src/syscall.rs @@ -27,20 +27,8 @@ fn call0(nr: usize) -> Result<[usize; 8]> { raw(nr, [0; 6]) } -fn slot_arg(slot: Option) -> usize { - slot.map_or(NONE, |s| s.value() as usize) -} - fn slot_result(r: usize) -> Option { - if r == NONE { - None - } else { - CapSlot::new(r as u8) - } -} - -fn slot_of(r: Result<[usize; 8]>) -> Result { - r.and_then(|r| slot_result(r[1]).ok_or(Error::InvalidArgument)) + reg_slot(r).flatten() } /// What a receiving call got. @@ -63,22 +51,14 @@ pub enum Received { } impl Received { - fn decode(r: [usize; 8]) -> Self { - let words = [r[2], r[3], r[4], r[5]]; - let cap = slot_result(r[6]); - match r[7] { - KIND_CALL => Received::Call { - badge: r[1], - words, - cap, - }, - KIND_SIGNAL => Received::Signal { bits: r[1] }, - _ => Received::Message { - badge: r[1], - words, - cap, - }, - } + fn decode(r: [usize; 8]) -> Result { + let d = regs_delivery(&r).ok_or(Error::InvalidArgument)?; + let (badge, words, cap) = (d.badge, d.words, d.cap); + Ok(match d.kind { + DeliveryKind::Message => Received::Message { badge, words, cap }, + DeliveryKind::Call => Received::Call { badge, words, cap }, + DeliveryKind::Signal => Received::Signal { bits: badge }, + }) } pub fn words(&self) -> [usize; 4] { @@ -89,8 +69,8 @@ impl Received { } } -fn message_args(ep: usize, words: [usize; 4], cap: Option) -> [usize; 6] { - [ep, words[0], words[1], words[2], words[3], slot_arg(cap)] +fn slot_of(r: Result<[usize; 8]>) -> Result { + r.and_then(|r| slot_result(r[1]).ok_or(Error::InvalidArgument)) } // ---- threads, processes, time ---- @@ -266,7 +246,7 @@ pub fn send(endpoint: CapSlot, w0: usize, w1: usize, w2: usize, w3: usize) -> us pub fn send_msg(endpoint: CapSlot, words: [usize; 4], cap: Option) -> Result<()> { raw( SYS_SEND, - message_args(endpoint.value() as usize, words, cap), + message_regs(endpoint.value() as usize, words, cap), ) .map(|_| ()) } @@ -278,30 +258,30 @@ pub fn receive(endpoint: CapSlot) -> (usize, usize, usize, usize) { } pub fn receive_msg(endpoint: CapSlot) -> Result { - raw(SYS_RECEIVE, [endpoint.value() as usize, 0, 0, 0, 0, 0]).map(Received::decode) + raw(SYS_RECEIVE, [endpoint.value() as usize, 0, 0, 0, 0, 0]).and_then(Received::decode) } /// Sends and waits for the reply. pub fn call(endpoint: CapSlot, words: [usize; 4], cap: Option) -> Result { raw( SYS_CALL, - message_args(endpoint.value() as usize, words, cap), + message_regs(endpoint.value() as usize, words, cap), ) - .map(Received::decode) + .and_then(Received::decode) } /// Answers the last `Call` this thread received. pub fn reply(words: [usize; 4], cap: Option) -> Result<()> { - raw(SYS_REPLY, message_args(0, words, cap)).map(|_| ()) + raw(SYS_REPLY, message_regs(0, words, cap)).map(|_| ()) } /// Replies to the pending `Call` (if any), then receives the next message. pub fn reply_recv(endpoint: CapSlot, words: [usize; 4], cap: Option) -> Result { raw( SYS_REPLY_RECV, - message_args(endpoint.value() as usize, words, cap), + message_regs(endpoint.value() as usize, words, cap), ) - .map(Received::decode) + .and_then(Received::decode) } // ---- notifications and interrupts ---- diff --git a/crates/types/src/bounded.rs b/crates/types/src/bounded.rs index 0fffd39..2213391 100644 --- a/crates/types/src/bounded.rs +++ b/crates/types/src/bounded.rs @@ -1,6 +1,7 @@ use crate::macros::bounded; -bounded!(CapSlot, u8, 0, 63); +// Kani runs the real kernel with tiny tables; see kernel/src/proofs. +bounded!(CapSlot, u8, 0, if cfg!(kani) { 3 } else { 63 }); bounded!(Priority, u8, 0, 31); bounded!(PageCount, u16, 1, 1024); diff --git a/crates/types/src/proofs/abi.rs b/crates/types/src/proofs/abi.rs new file mode 100644 index 0000000..d206d16 --- /dev/null +++ b/crates/types/src/proofs/abi.rs @@ -0,0 +1,62 @@ +use crate::bounded::CapSlot; +use crate::syscall_abi::*; + +fn any_slot() -> Option { + if kani::any() { + CapSlot::new(kani::any::() % (CapSlot::MAX + 1)) + } else { + None + } +} + +#[kani::proof] +fn optional_slots_roundtrip() { + let s = any_slot(); + assert!(reg_slot(slot_reg(s)) == Some(s)); +} + +#[kani::proof] +fn every_register_decodes_to_none_or_a_valid_slot() { + let r: usize = kani::any(); + if let Some(Some(slot)) = reg_slot(r) { + assert!(slot.value() <= CapSlot::MAX); + assert!(slot.value() as usize == r); + } +} + +#[kani::proof] +fn page_perms_roundtrip_and_reject_the_rest() { + let r: usize = kani::any(); + match reg_perms(r) { + Some(p) => assert!(perms_reg(p) == r), + None => assert!(r > PERMS_READ_EXECUTE), + } +} + +/// What the kernel writes for a receive is what libkos reads back. +#[kani::proof] +fn deliveries_roundtrip() { + let kind = match kani::any::() % 3 { + 0 => DeliveryKind::Message, + 1 => DeliveryKind::Call, + _ => DeliveryKind::Signal, + }; + let d = Delivery { + kind, + badge: kani::any(), + words: kani::any(), + cap: any_slot(), + }; + let regs = delivery_regs(&d); + assert!(regs[0] == 0); + assert!(regs_delivery(®s) == Some(d)); +} + +#[kani::proof] +fn error_codes_roundtrip() { + let r: usize = kani::any(); + if let Some(code) = ErrorCode::from_raw(r) { + assert!(code as usize == r); + assert!(r != 0, "0 means success"); + } +} diff --git a/crates/types/src/proofs/bounded.rs b/crates/types/src/proofs/bounded.rs index 99b15a3..618f82f 100644 --- a/crates/types/src/proofs/bounded.rs +++ b/crates/types/src/proofs/bounded.rs @@ -4,14 +4,14 @@ use crate::bounded::{CapSlot, PageCount, Priority}; fn capslot_always_valid_index() { let value: u8 = kani::any(); if let Some(slot) = CapSlot::new(value) { - assert!(slot.value() <= 63); + assert!(slot.value() <= CapSlot::MAX); } } #[kani::proof] fn capslot_rejects_out_of_range() { let value: u8 = kani::any(); - kani::assume(value > 63); + kani::assume(value > CapSlot::MAX); assert!(CapSlot::new(value).is_none()); } diff --git a/crates/types/src/proofs/mod.rs b/crates/types/src/proofs/mod.rs index 4d45d1f..f366be6 100644 --- a/crates/types/src/proofs/mod.rs +++ b/crates/types/src/proofs/mod.rs @@ -1,3 +1,4 @@ +mod abi; mod bounded; mod generation; mod permissions; diff --git a/crates/types/src/syscall_abi.rs b/crates/types/src/syscall_abi.rs index 69d2330..7247cd4 100644 --- a/crates/types/src/syscall_abi.rs +++ b/crates/types/src/syscall_abi.rs @@ -1,5 +1,9 @@ //! Register-level syscall contract shared by the kernel and libkos. -//! See docs/ipc.md for the meaning of each call. +//! See docs/ipc.md for the meaning of each call. Both sides encode and +//! decode through the functions below, so they cannot drift apart. + +use crate::bounded::CapSlot; +use crate::mapping::PagePerms; pub const SYS_SEND: usize = 0; pub const SYS_RECEIVE: usize = 1; @@ -91,3 +95,115 @@ impl ErrorCode { }) } } + +// ---- wire encoding ---- + +/// An optional capability slot as a register. +pub fn slot_reg(slot: Option) -> usize { + slot.map_or(NONE, |s| s.value() as usize) +} + +/// Decodes an optional capability slot: `Some(None)` for `NONE`, `None` +/// for a value that is neither `NONE` nor a valid slot. +pub fn reg_slot(reg: usize) -> Option> { + match reg { + NONE => Some(None), + r => Some(Some(CapSlot::new(u8::try_from(r).ok()?)?)), + } +} + +pub fn perms_reg(perms: PagePerms) -> usize { + match perms { + PagePerms::ReadOnly => PERMS_READ_ONLY, + PagePerms::ReadWrite => PERMS_READ_WRITE, + PagePerms::ReadExecute => PERMS_READ_EXECUTE, + } +} + +pub fn reg_perms(reg: usize) -> Option { + match reg { + PERMS_READ_ONLY => Some(PagePerms::ReadOnly), + PERMS_READ_WRITE => Some(PagePerms::ReadWrite), + PERMS_READ_EXECUTE => Some(PagePerms::ReadExecute), + _ => None, + } +} + +/// Argument registers `a0..a5` of a message-carrying call. +pub fn message_regs(target: usize, words: [usize; 4], cap: Option) -> [usize; 6] { + [ + target, + words[0], + words[1], + words[2], + words[3], + slot_reg(cap), + ] +} + +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum DeliveryKind { + /// A `Send`; no reply expected. + Message, + /// A `Call`; the receiver's reply slot now names the caller. + Call, + /// Notification bits. + Signal, +} + +/// What a receiving syscall hands back. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub struct Delivery { + pub kind: DeliveryKind, + /// The sender's badge, or the signal bits. + pub badge: usize, + pub words: [usize; 4], + /// Where a transferred capability landed in the receiver's table. + pub cap: Option, +} + +impl Delivery { + pub fn signal(bits: usize) -> Self { + Self { + kind: DeliveryKind::Signal, + badge: bits, + words: [0; 4], + cap: None, + } + } +} + +/// Result registers `a0..a7` for a successful receive. +pub fn delivery_regs(d: &Delivery) -> [usize; 8] { + let kind = match d.kind { + DeliveryKind::Message => KIND_MESSAGE, + DeliveryKind::Call => KIND_CALL, + DeliveryKind::Signal => KIND_SIGNAL, + }; + [ + 0, + d.badge, + d.words[0], + d.words[1], + d.words[2], + d.words[3], + slot_reg(d.cap), + kind, + ] +} + +/// Inverse of `delivery_regs`; `None` if the registers are not a delivery. +pub fn regs_delivery(r: &[usize; 8]) -> Option { + let kind = match r[7] { + KIND_MESSAGE => DeliveryKind::Message, + KIND_CALL => DeliveryKind::Call, + KIND_SIGNAL => DeliveryKind::Signal, + _ => return None, + }; + Some(Delivery { + kind, + badge: r[1], + words: [r[2], r[3], r[4], r[5]], + cap: reg_slot(r[6])?, + }) +}