Skip to content

track-a-kernel.md

Latest commit

 

History

History
89 lines (75 loc) · 20.9 KB

track-a-kernel.md

File metadata and controls

89 lines (75 loc) · 20.9 KB
Raw

Track A — Kernel correctness

  • Agent run by: Claude general-purpose agent, 2026-05-06
  • Scope: End-to-end correctness review of kernel crate (cap/obj/ipc/sched/lib).
  • HEAD reviewed: 214052d

Findings

Blocker

  • (none)

Non-blocking

  • kernel/src/cap/table.rs:105 CAP_TABLE_CAPACITY <= Index::MAX is asserted with const _: () = assert!(...), not the inline const { assert!(...) } form used in Arena::new (kernel/src/obj/arena.rs:90) — Phase A's recommended migration was not applied. Both produce hard build failure on violation; the inline form is preferred for stylistic consistency with the audited sibling pattern. Suggested resolution: replace with const { assert!(CAP_TABLE_CAPACITY <= Index::MAX as usize, "cap-table capacity exceeds Index::MAX"); }.
  • kernel/src/sched/mod.rs:48 SchedQueue<0> is still structurally legal — Phase A non-blocker. new() constructs a zero-length queue, enqueue short-circuits on len == N (0 == 0), dequeue returns None. Behaviourally a zero-capacity queue, not a UB hazard, but the type-level contract is unstated. Suggested resolution: add const { assert!(N > 0, "SchedQueue requires N > 0"); } at the top of SchedQueue::new so the invariant is a build-time guarantee rather than implicit semantics.
  • kernel/src/ipc/mod.rs:76 IpcError::InvalidCapability still collapses three distinct failure modes from validate_ep_cap / validate_notif_cap: (a) stale lookup, (b) missing right, (c) wrong object kind (ipc/mod.rs:419-450). Mirrored on the transfer side: IpcError::InvalidTransferCap collapses (a) stale handle and (b) missing TRANSFER right (ipc/mod.rs:271-278). Same observation Phase A made — T-006/T-007/T-009/T-012 did not introduce new conflations, but they did not split the variants either. Tests cannot distinguish "right missing" from "stale handle" by error variant. Suggested resolution: file an ADR introducing IpcError::WrongObjectKind and IpcError::MissingRight (and the symmetric transfer variants) before B2 begins, so userspace surface lands with the granular shape from day 1.
  • kernel/src/sched/mod.rs:294 unblock_receiver_on is single-waiter by return after the first match — correct for the v1 depth-1 endpoint queue and explicitly documented at sched/mod.rs:287-293. The IPC state machine in EndpointState cannot park more than one receiver, so the contract holds today. Multi-waiter wake-up remains an ADR-0019 open question; the call-site's loop-then-return shape will need refactoring (and the IPC waiter list will need to grow) before any blocked-task fairness claim can be made. Track for the ADR-0019 follow-up.
  • kernel/src/sched/mod.rs:773-778 The Deadlock rollback path restores s.current and s.task_states[current_idx], but the endpoint state was already moved from Idle to RecvWaiting by Phase 1's ipc_recv and is not reversed. The doc-comment on SchedError::Deadlock (sched/mod.rs:160-180) is honest about this gap and explains the consequence (a follow-up ipc_recv_and_yield from the same caller observes IpcError::QueueFull, not Pending). With an idle task registered the path is structurally unreachable in v1, so the asymmetry is benign — but worth re-visiting under an ADR before preemption / SMP land. Suggested resolution: leave as-is for v1; queue an ADR for "endpoint rollback / ipc_cancel_recv" before Phase B2.
  • kernel/src/ipc/mod.rs:211-228 IpcQueues::reset_if_stale_generation silently drops a Some(cap) payload (at the language level, core::mem::replace to Idle discards the prior EndpointState value, including any Capability). The debug_assert! catches the Some(_) case in tests, but in release the cap is leaked without diagnostic. Today no destruction path can leak a Some(cap)-state slot because no userspace-driven destroy is wired; the comment correctly identifies this as a future-Phase-B drain-before-destroy invariant. Suggested resolution: when endpoint destruction lands, route the prior state through the destroyer's table for a graceful drain; until then the debug_assert! is the right shape.
  • kernel/src/sched/mod.rs:558-560 yield_now's re-enqueue of current_handle uses an unwrap-style let-else panic! ("ready queue full on yield re-enqueue") rather than the Phase-A-suggested debug_assert!(self.ready.len() < TASK_ARENA_CAPACITY) before the call. The current shape is equivalent (the enqueue itself returns Err and the let-else panics with a named string) and matches the kernel's "typed-error or named panic" idiom. Acceptable as-is; the Phase A nit is effectively superseded by the let-else pattern.
  • kernel/src/sched/mod.rs:295-314 unblock_receiver_on is O(N) over TASK_ARENA_CAPACITY. With N=16 this is fine, but every IPC-deliver path runs it. Once the arena grows or multi-waiter wake lands, this becomes hot. Cross-track note rather than a kernel-correctness blocker.

Observation

  • kernel/src/lib.rs:38-43 The kernel-stricter denylist (clippy::panic, unwrap_used, expect_used, todo, arithmetic_side_effects, float_arithmetic) layers on top of the workspace lint set in Cargo.toml:31-44. The intersection is sane — workspace owns pedantic, undocumented_unsafe_blocks, missing_safety_doc, alloc_instead_of_core; the kernel does not redundantly re-state those. Phase A's "double-stated" nit is effectively resolved (no overlap between the two sets today). Worth one-line comment in lib.rs saying "these layer onto [workspace.lints]; do not re-state workspace denies here".
  • kernel/src/cap/table.rs:307-398 cap_revoke BFS is correct under release-mode break on desc_len >= CAP_TABLE_CAPACITY. Because the derivation tree's descendants[] array is sized exactly at CAP_TABLE_CAPACITY, and free_slot is only invoked after the scan (table.rs:388-390), the buffer cannot be reached in correct trees (each live node appears at most once via parent/first_child/next_sibling invariants). The debug_assert!+break shape is the right defensive pattern. Phase A's recommendation to add a comment like "descendants fit because every live node appears at most once" still applies — the docstring at table.rs:329-336 explains the cycle-detection intent but does not state the size proof. Worth a one-liner inside the body.
  • kernel/src/cap/table.rs:444-464 cap_take correctly extracts the entry via Option::take() before free_slot; free_slot's slot.entry = None is then idempotent. The pattern is identical to Phase A's verified shape; tested by cap_take_middle_sibling_preserves_list_integrity. OK.
  • kernel/src/cap/table.rs:262-277 cap_derive's saturating depth cap ((parent_depth as usize).saturating_add(1) > MAX_DERIVATION_DEPTH) handles parent_depth == u8::MAX cleanly because parent_depth is u8 and the conversion to usize cannot lose precision. The cast back via new_depth_usize as u8 is bounded by MAX_DERIVATION_DEPTH (16) and annotated. OK.
  • kernel/src/cap/rights.rs:67-70 CapRights::from_raw masks reserved bits via bits & Self::KNOWN_BITS.0. Tested by from_raw_masks_unknown_bits. OK.
  • kernel/src/cap/mod.rs:140-161 CapError variants (CapsExhausted, InvalidHandle, WidenedRights, InsufficientRights, DerivationTooDeep, HasChildren) each have unique semantic ownership; no collapsed variants. #[non_exhaustive] is set. OK.
  • kernel/src/obj/arena.rs:89-121 Arena<T,N>::new correctly handles N == 0 via free_head: if N > 0 { Some(0) } else { None }. Generation reuse (free → bump → reallocate) is exercised by free_then_allocate_bumps_generation. OK.
  • kernel/src/obj/mod.rs:60-69 ObjError::StillReachable is documented as caller-enforced (obj/mod.rs:62-68) — destroy_* does not itself walk capability tables. Caller's reachability check uses CapabilityTable::references_object. The contract is correctly stated; the gap (no kernel-side enforcement) remains a Phase B follow-up.
  • kernel/src/obj/task.rs:60 Test handles via TaskHandle::test_handle are #[cfg(test)] + pub(crate) — production builds cannot construct synthetic handles. Symmetric for endpoint and notification. OK.
  • kernel/src/ipc/mod.rs:298-316 ipc_send's atomicity contract is preserved: take_cap_if_some runs before core::mem::replace(state, Idle), so a cap_take failure (e.g. HasChildren) leaves both the caller's table and the endpoint state intact. RecvWaiting is preserved across the failure — covered by send_with_bad_transfer_cap_preserves_recv_waiting. OK.
  • kernel/src/ipc/mod.rs:355-363 ipc_recv's ReceiverTableFull pre-flight is correct: pending_has_cap && caller_table.is_full() is checked before the core::mem::replace(state, Idle), so a full receiver table leaves both the cap parked in SendPending / RecvComplete and the endpoint state unchanged. Covered by recv_with_full_table_preserves_pending_cap.
  • kernel/src/ipc/mod.rs:403-415 ipc_notify correctly takes &CapabilityTable (immutable) — it never mutates the caller's table. Asymmetric vs ipc_send/ipc_recv because notifications are non-blocking and carry no cap transfer. OK.
  • kernel/src/sched/mod.rs:439-441 start_prelude's empty-queue panic is the documented programming-error path; covered by start_prelude_panics_on_empty_ready_queue. OK.
  • kernel/src/sched/mod.rs:531-602 yield_now raw-pointer split borrow: (*sched).contexts.as_mut_ptr() is dereferenced after the inner &mut Scheduler<C> is dropped, then ctx_ptr.add(current_idx) and ctx_ptr.add(next_idx) form two non-overlapping pointers because current_idx != next_idx (asserted via debug_assert_ne! at line 581). IrqGuard is held across the cpu.context_switch call site. The // SAFETY: block enumerates UNSAFE-2026-0008 rationale + alternatives and references the Shared safety contract above. UNSAFE-2026-0014 is named in start_prelude and yield_now's pre-switch blocks. OK.
  • kernel/src/sched/mod.rs:712-832 ipc_recv_and_yield Phase 1 / Phase 2 / Phase 3 separation: each phase materialises momentary &muts inside its own block and drops them before the switch. The Phase 3 re-call of ipc_recv after resume is now a typed-Err(SchedError::Ipc(IpcError::PendingAfterResume)) rather than a panic / silent Ok(Pending) (per ADR-0022). The Phase A non-blocker about debug_assert!(!Pending) is superseded — the typed return replaces it (the comment at lines 820-826 explicitly states the redundancy). Tested by ipc_recv_and_yield_resume_pending_returns_typed_err.
  • kernel/src/sched/mod.rs:475-507 start is unsafe fn over *mut Scheduler<C> per ADR-0021. The throwaway-context discipline is right: let mut throwaway = <C::TaskContext as Default>::default() lives on the abandoned bootstrap frame; cpu.context_switch never returns to it; the loop { spin_loop } satisfies -> ! defensively. IrqGuard is held but never dropped (-> !), so tasks begin with IRQs masked — explicitly documented at lines 454-462. Acceptable v1 posture.
  • kernel/src/sched/mod.rs:622-678 ipc_send_and_yield's pre-switch block correctly drops every &mut (Scheduler, EndpointArena, IpcQueues, CapabilityTable) before the conditional yield_now(sched, cpu)? re-entry. The re-entry takes its own raw pointer, satisfying the Shared safety contract's non-aliasing rule. Tested by the three-case bundle (Delivered + Enqueued + send-error preserves state).
  • kernel/src/sched/mod.rs:181 SchedError::Deadlock is the typed-error replacement for the prior panic! per ADR-0022. The variant is documented end-to-end (rollback scope; v1 unreachability with idle registered). Tested by ipc_recv_and_yield_returns_deadlock_when_ready_queue_empty. OK.
  • The kernel crate's Cargo.toml (kernel/Cargo.toml:13-20) declares only tyrne-hal as a direct dep and tyrne-test-hal as [dev-dependencies]. Production builds cannot pick up the fakes. [lints] workspace = true opts into the workspace denylist. OK.
  • The kernel crate has zero unsafe in cap/, obj/, ipc/, lib.rs. The 45 unsafe occurrences in sched/mod.rs (counted via grep) all carry // SAFETY: blocks and reference UNSAFE-2026-0008 / 0009 / 0014 audit tags consistently. No unsafe in any kernel file is undocumented.
  • ADR-0018 deferrals (Reply / ReplyRecv / badges) remain absent from IpcError, Message, SendOutcome, RecvOutcome. Verified.
  • Endpoint destroy/create cycles: IpcQueues::reset_if_stale_generation (peeked via state_of / peek_state) detects generation mismatch and resets to Idle. The fault model is therefore: a SendPending { cap: Some(_) } survives endpoint slot destruction only via in-flight loss (the cap is owned by the now-stale state and the reset silently drops it before the assert fires in debug). With no userspace destroy path wired, this remains a future-Phase-B drain-before-destroy invariant — see the non-blocker on reset_if_stale_generation above.

Regression vs Phase A code review

  • cap_copy peer depth (Phase A: non-blocking, depth identical to source's) — still applies, OK. The shape at table.rs:212 is unchanged (depth: depth for the new peer); covered by copy_of_a_child_shares_parent.
  • cap_derive saturating depth cap (Phase A: non-blocking) — still applies, OK. table.rs:268-271.
  • cap_revoke BFS w/ release-mode break (Phase A: non-blocking, recommended a one-liner comment) — still applies; comment recommendation unfulfilled. Recorded as Observation above.
  • cap_take ordering vs free_slot (Phase A: non-blocking, OK) — still applies, OK.
  • CapRights::from_raw reserved-bit masking (Phase A: non-blocking, OK) — still applies, OK.
  • CAP_TABLE_CAPACITY <= Index::MAX const-block migration (Phase A: non-blocking) — still applies; migration not done. Recorded as Non-blocking above.
  • Arena<T,N>::new for N == 0 (Phase A: non-blocking, OK) — still applies, OK.
  • destroy_ doc-comment "callers must check references_object"* (Phase A: non-blocking) — still applies, OK. The contract remains a v1 caller responsibility; obj/mod.rs documents it; objection deferred to Phase B.
  • #[cfg(test)] test_handle hygiene (Phase A: non-blocking, OK) — still applies, OK.
  • ipc_recv ReceiverTableFull pre-flight (Phase A: non-blocking, important) — still applies; T-011 added the test. recv_with_full_table_preserves_pending_cap closes the test gap Phase A flagged.
  • ipc_send cap-take-before-state (Phase A: non-blocking, important) — still applies, OK.
  • IpcQueues::sync_generation (Phase A: non-blocking, OK) — superseded by reset_if_stale_generation with stronger debug-assert + generation-tracking shape; functionally equivalent + more diagnostic.
  • IpcError::InvalidCapability collapse (Phase A: non-blocking, watch) — still applies; T-006/T-007/T-009/T-012 did not introduce new conflations and did not split the variants either. Recorded as Non-blocking above.
  • ipc_notify takes &CapabilityTable immutably (Phase A: non-blocking, OK) — still applies, OK.
  • Message default w/ label==0 sentinel risk (Phase A: non-blocking, watch) — still applies; no change. No sentinel use observed in T-006/T-007/T-011/T-012; park.
  • SchedQueue<0> structural legality (Phase A: non-blocking, deferred const-assert) — still applies; not added. Recorded as Non-blocking above.
  • yield_now silent-discard via let _ = enqueue(...) (Phase A: non-blocking, suggested debug_assert) — superseded by the let-else panic! at sched/mod.rs:558-560.
  • Split-borrow via ctx_ptr.add(...) debug_assert_ne (Phase A: non-blocking) — fixed. debug_assert_ne!(current_idx, next_idx, ...) is at lines 581-584 (yield_now) and 786-789 (ipc_recv_and_yield).
  • ipc_recv_and_yield post-resume re-call + debug_assert!(!Pending) (Phase A: non-blocking) — superseded by the typed Err(SchedError::Ipc(IpcError::PendingAfterResume)) per ADR-0022, with explicit comment at sched/mod.rs:820-826 explaining the redundancy.
  • unblock_receiver_on single-waiter (Phase A: non-blocking, important) — still applies, OK. Multi-waiter remains an ADR-0019 open question.
  • Scheduler::start empty-queue panic (Phase A: non-blocking, OK) — still applies; T-011 added a host test via start_prelude_panics_on_empty_ready_queue.
  • Tasks begin with IRQs masked (Phase A: non-blocking, doc) — still applies; documented at sched/mod.rs:454-462. Re-examine for B2 once a timer-IRQ-driven task exists.
  • kernel/src/lib.rs duplicates workspace deny list (nit) (Phase A: non-blocking nit) — fixed-ish. No actual duplication today; kernel adds clippy::panic / unwrap_used / expect_used / todo / arithmetic_side_effects / float_arithmetic over the workspace's pedantic (warn) + undocumented_unsafe_blocks / missing_safety_doc / alloc_instead_of_core (deny). Recorded as Observation with a suggested one-line comment.

Cross-track notes (route to merge)

  • → Track B: HAL Cpu::wait_for_interrupt is invoked by the BSP idle task, not by the kernel scheduler — confirm the trait contract is tight enough that the BSP-side WFI cannot wedge on a missed-edge if a future preemptive scheduler races a deadline arm.
  • → Track C: IpcQueues::reset_if_stale_generation silently drops Some(cap) payloads in release builds (debug_assert only). Document under the audit log's "future destroy-path drain" line so security review can assess the leak window once endpoint destruction lands.
  • → Track C: unsafe fn over *mut Scheduler<C> in start / yield_now / ipc_send_and_yield / ipc_recv_and_yield (UNSAFE-2026-0014). All four entry points carry the "Shared safety contract" header at sched/mod.rs:317-396; per-block // SAFETY: comments reference it correctly. Confirmed for security row-by-row.
  • → Track D: unblock_receiver_on is O(N) over TASK_ARENA_CAPACITY=16 in every IPC-deliver path. With a single-waiter contract this is correct; if multi-waiter or a larger arena lands, this becomes hot.
  • → Track D: validate_ep_cap performs two table lookups per ipc_send_and_yield (once via Scheduler::resolve_ep_cap, once inside ipc_send::validate_ep_cap). Double-validation is intentional (the bridge needs the EndpointHandle for unblock_receiver_on), but worth a perf measurement when IPC throughput becomes a target.
  • → Track E: ADR-0022's "Revision notes" claim (no debug_assert! companion to the typed return) is materialised at sched/mod.rs:820-826 — verify that comment matches ADR-0022's revision history exactly.
  • → Track F: IpcError::PendingAfterResume is exercised by ipc_recv_and_yield_resume_pending_returns_typed_err; SchedError::Deadlock by ipc_recv_and_yield_returns_deadlock_when_ready_queue_empty; start_prelude empty-queue panic by start_prelude_panics_on_empty_ready_queue. The three Phase A test gaps are closed.
  • → Track I: Trait-contract check — kernel uses only Cpu, ContextSwitch, IrqGuard, IrqState from tyrne-hal. IrqController / Mmu / Timer / Console are BSP-side, not kernel-side. No kernel-internal dyn-trait usage.
  • → Track J: zero umbrix matches in any kernel-crate file (spot-checked via the imports and ADR cross-references — every link points at cemililik/TyrneOS).

Sub-verdict

Approve