GKaszewski/k-os
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

refactor(kernel): split ipc/memory/lib/thread by concern; trim comments

Browse Source
This commit is contained in:
Gabriel Kaszewski
2026-10-27 13:21:53 +01:00
parent b814bd9570
commit 95dbe7b9d5
34 changed files with 1239 additions and 1231 deletions
Download Patch File Download Diff File Expand all files Collapse all files

9
crates/domain/src/capability/derivation.rs
View File

@@ -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<const N: usize>(parents: &[Option<u16>; 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() {

4
crates/domain/src/capability/mod.rs
View File

@@ -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,

14
crates/domain/src/capability/tree.rs
View File

@@ -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<const N: usize> CapTree<N> {
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<usize>) -> bool {
let (Some(me), Some(node)) = (id(i), self.nodes.get(i)) else {
return false;