Development #9 — T-011 + T-008 + T-013 (B0 hygiene close + B1 EL drop)#9
Merged
Conversation
…rider, 6 small fixes)
Verified each finding against current state. Eight applied; three of them
required care.
Inline (all ✅ confirmed):
- mini-retro line 45: "ACı" (TR suffix on EN word) → "AC" — CLAUDE.md
language-policy fix, in-place since mini-retros are not append-only
per ADR-0025 §Rule 2 (which scopes only to ADR bodies and riders).
- mini-retro line 74: TR maintainer-quote with EN gloss → EN-only —
same policy fix, semantic preserved.
- T-009 task file: review-history table missing R3 round + Done
promotion rows. Two new append-only rows: one capturing the R3
fix-up commits (124 → 130 host tests; resolution-floor cases) and
one capturing the 2026-04-27 independent-agent Done promotion.
- ADR-0025 line 11 ("four ADRs (ADR-0021, ADR-0022)" — factually
off; the count is four riders across two ADRs): corrected via
§Revision notes append, not in-place. ADR-0025 is the document
defining the post-Accept append-only rule (§Rule 2); editing its
body in place — even for a factual correction — would set exactly
the precedent the rule forbids. Rider names the four riders
explicitly so the math is auditable.
- phase-b.md line 242 ADR-0026 row: "may go unused if T-011 absorbs
the exception-vector design" → "if T-012 absorbs it without a
separate ADR" — T-011 is missing-tests bundle, exception-vector
design is T-012's domain.
Nitpicks:
- write-adr step 4: retroactive-recovery exception was implicit; now
cross-references the new step-10 careful-re-read AC and anti-pattern 5
so the "Status: Accepted is permitted if recording after the fact"
carve-out reconciles cleanly with "Accept is never in the same commit
as the initial draft".
- ci.yml coverage-job comment: removed bogus CARGO_LLVM_COV_VERSION
env var reference (no such variable exists; the version pin is
inline on `tool: cargo-llvm-cov@0.6.16`); replaced "lockstep with
NIGHTLY_PIN" wording with "independent of NIGHTLY_PIN; bump together
or independently per docs/guides/ci.md", matching the docs.
- template.md Dependency-chain example: replaced concrete T-009 / T-012
references (statuses already drifting) with T-NNN (Status) placeholders
+ a "real T-NNNs" lead-in. Also added `text` language tag to the
fenced block (MD040).
- hal/src/timer.rs ticks_to_ns clippy reason: "if/else guard above"
→ "at the end of this function" — the guard is below the function
signature where the attribute lives.
Rejected (not applied):
- timer.rs round-to-nearest pedagogy comment requested adding 4–5
lines explaining the truncation-induced half-bias, the strict
round-half-up alternative, and its overflow constraint. Rejected:
the existing doc-comment already states "Round-to-nearest" and
"Sub-nanosecond precision is silently lost", which covers the
observable behaviour. The reviewer's wording ("documenting that the
current form rounds-half-to-even-ish") is pedagogy, not WHY-the-code-
is-this-way. CLAUDE.md's "default to writing no comments" applies.
Verification: cargo fmt clean, host-clippy clean, host-test 130/130 green
(77 + 19 + 34), kernel-clippy clean, kernel-build clean.
Refs: ADR-0025
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Closes T-011's five acceptance-criteria items in one bundled commit:
ipc: three new tests + one symmetric guard
- recv_with_full_table_preserves_pending_cap: ReceiverTableFull
pre-flight guard surfaces the typed error and leaves the in-flight
cap parked in SendPending; verified by retry after freeing one slot
on the receiver side.
- stale_send_pending_with_some_cap_panics_in_debug
(#[cfg(debug_assertions)] + #[should_panic]): the
reset_if_stale_generation debug_assert fires when an in-flight
Some(cap) would otherwise be silently dropped on slot reuse.
- stale_recv_waiting_resets_silently +
stale_send_pending_without_cap_resets_silently: paired
must-not-panic guards proving the assert's predicate is not
over-broad. Both reach reset_if_stale_generation via peek_state.
sched: start_prelude refactor + five new tests
- Refactor: the dequeue + state-mutation half of `start` is
extracted as `start_prelude(sched: *mut Scheduler<C>) -> usize`
— semantically unchanged for callers, but the prelude is now
directly testable from the host (the post-prelude
cpu.context_switch is ABI assembly the host harness cannot run).
- start_prelude_dispatches_head_and_marks_ready: happy-path
assertions (next_idx, task_states[next_idx] == Ready, current ==
Some(next_handle), ready.len() decremented).
- start_prelude_panics_on_empty_ready_queue: pinned to the named
panic message ("empty ready queue") so refactors cannot silently
drop the kernel-programming-error guard.
- ipc_send_and_yield three-case bundle: Delivered (unblocks
receiver + yields), Enqueued (no yield, scheduler unchanged), and
Err (ipc_send rights-check fails, scheduler state preserved
symmetrically to T-007's ipc_recv_and_yield Deadlock state-restore
test).
cap/table: four targeted error-branch tests (sweep)
- cap_derive_on_full_table_returns_caps_exhausted: the pop_free()
failure branch reached from cap_derive's call site (distinct from
insert_root's exhaustion test).
- cap_copy_on_stale_handle_returns_invalid_handle: the third entry
point delegating through lookup; previously covered for cap_drop
/ cap_take only.
- lookup_on_stale_handle_returns_invalid_handle: direct exercise
of the validation branch every other API delegates to.
- drop_first_child_updates_parent_first_child_pointer: completes
unlink_from_siblings's branch coverage (drop_middle_sibling test
already covered the mid-list case).
Test count delta: 130 → 143 (+4 ipc + 5 sched + 4 cap; +13 total).
77 + 4 + 5 + 4 = 90 kernel; 19 hal; 34 test-hal.
Coverage acceptance gates met (re-run report:
docs/analysis/reports/2026-04-27-coverage-rerun.md):
- kernel/src/sched/mod.rs regions: 83.93 % → 93.97 % (+9.81 pp;
AC ≥ 90 % ✅).
- workspace regions: 94.41 % → 96.33 % (+1.92 pp;
AC ≥ 96 % ✅).
- kernel/src/cap/table.rs regions: 96.84 % → 97.46 %.
Miri 143/143 clean across the workspace; fmt / host-clippy /
kernel-clippy / kernel-build all green.
Cap-table sweep delivered four targeted tests (the AC permits
"five or fewer"); the fifth slot was deliberately left empty after
audit found the obvious 'etc.' candidates already covered
(cap_take_stale_handle_fails, cap_take_on_node_with_children_fails,
cap_drop_on_interior_node_returns_has_children,
table_exhaustion_returns_caps_exhausted).
T-011 status: Draft → In Progress → In Review. Pending Done
promotion via the standard approval-review pass.
Refs: ADR-0017, ADR-0019, ADR-0021, ADR-0022
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…erview banner Synthesises the Phase A → B0 design state into the architecture folder so a future maintainer (or returning contributor) can read the *how* alongside the existing overview / boot / hal / security-model documents without having to traverse eight Accepted ADRs and the kernel source. scheduler.md (new, ~180 lines) - FIFO ready queue (ADR-0019), ContextSwitch + Cpu split (ADR-0020), idle task + typed SchedError::Deadlock (ADR-0022), raw-pointer scheduler IPC bridge (ADR-0021). - Two Mermaid diagrams: data structure (Scheduler<C> ⇄ SchedQueue ⇄ TaskState) and the task-slot lifecycle state machine. - Sequence trace through ipc_send_and_yield's Delivered path showing the three momentary &muts and the contained context-switch window. - Invariants + trade-offs + open questions sections in the house style; cross-links to T-004/T-006/T-007/T-011 and to UNSAFE-2026- 0008/0013/0014. ipc.md (new, ~190 lines) - Three-primitive set per ADR-0017 (ipc_send / ipc_recv / ipc_notify), four-state Endpoint state machine (Idle / SendPending / RecvWaiting / RecvComplete), slot_generations stale-reset rule, and the capability-transfer pre-flight discipline (sender-side validation → receiver-side is_full() pre-flight → atomic move on commit). - IpcError taxonomy with the PendingAfterResume special case documented per ADR-0022 §Revision notes (second rider). - Scheduler-bridge wrappers (ipc_send_and_yield / ipc_recv_and_yield) summary + BSP-side discipline (single derivation per pointer; StaticCell::as_mut_ptr) cross-linking to scheduler.md and the audit log. - Three Mermaid diagrams: state machine, generation-reset flow, bridge sequence. hal.md - Timer subsection expanded with the post-T-009 picture: CNTVCT_EL0 / CNTV_CVAL_EL0 / CNTV_CTL_EL0 register-family choice per ADR-0010, the host-testable helpers in tyrne_hal::timer (ticks_to_ns, resolution_ns_for_freq), and the explicit note that arm_deadline / cancel_deadline are deferred to T-012's IRQ work. overview.md - Status banner pinned to 2026-04-27 noting Phase A complete; cross- links to scheduler.md and ipc.md from the kernel-responsibilities list and the IPC capability-transfer paragraph. architecture/README.md - scheduler.md and ipc.md added as Accepted (v0.0.1). - Planned `kernel-core.md` and `scheduling.md` rows removed — scheduler.md + ipc.md jointly subsume both. - boot.md status note clarifies the EL drop is pending T-013. T-008 status: Draft → In Review (single arc; opened today). boot.md update for T-013's EL drop is explicitly out of T-008's scope per its DoD — T-013 owns that update. capabilities.md, memory.md, and a standalone timer.md are deferred to later phases. No code changes. host tests 143/143 green; fmt / host-clippy / kernel-clippy / kernel-build all clean. Refs: ADR-0010, ADR-0017, ADR-0019, ADR-0020, ADR-0021, ADR-0022 Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Implements ADR-0024's "always drop to EL1" policy at the BSP reset vector and provides a safe-Rust accessor for CurrentEL. bsp-qemu-virt/src/boot.s — three-phase _start - (1) K3-12: msr daifset, #0xf as the very first instruction at _start so the reset vector cannot accidentally take an interrupt before the kernel installs an exception vector table (T-012's future work). The mask carries across the EL drop because SPSR_EL2.DAIF propagates to PSTATE on eret. - (2) EL drop dispatch: read CurrentEL, mask bits[3:2]. EL2 → configure HCR_EL2 (RW=1; E2H=0, TGE=0 → non-VHE EL1 explicitly per ADR-0024), SPSR_EL2 (mode = EL1h, DAIF masked = 0x3c5), ELR_EL2 (= post_eret label), then eret. EL1 → branch to post_eret (no-op). EL3 (or any other unexpected value) → halt with `wfe; b .-` since no Rust panic infrastructure is up. - (3) Conventional setup unchanged from the pre-T-013 path: SP, CPACR_EL1.FPEN, BSS zero, bl kernel_entry, defensive halt. After phase 2, every later instruction runs at EL1 — the precondition T-009's UNSAFE-2026-0016 self-check now relies on as a load-bearing post-condition rather than a defensive guard. hal/src/cpu.rs — current_el() free function - pub fn current_el() -> u8, cfg-gated to target_arch = "aarch64" + target_os = "none" so the function is intentionally absent on host-test targets where MRS CurrentEL would either trap or yield no useful value. Test mocks (FakeCpu, ResetQueuesCpu, test-hal::cpu) therefore do not need to declare an EL. - Per ADR-0024 §Open questions, the free-function form (rather than a Cpu trait method) was chosen so the early-boot path could call this before any Cpu instance has been constructed, and so test mocks would not have to invent an EL. - hal/src/lib.rs: `mod cpu;` → `pub mod cpu;` so the public path is `tyrne_hal::cpu::current_el()`, matching the existing `pub mod timer;` convention. bsp-qemu-virt/src/cpu.rs — QemuVirtCpu::new now uses the helper - Inline-asm MRS CurrentEL block in QemuVirtCpu::new replaced by a call to tyrne_hal::cpu::current_el(). Behaviour and panic message unchanged; the unsafe block now lives in one auditable helper rather than at the call site. Future callers (e.g. kernel_entry validating the EL drop's outcome) reuse the same audited path. docs/audits/unsafe-log.md — two new entries + one Amendment - UNSAFE-2026-0017: boot.s reset-vector DAIF mask + EL2→EL1 transition. Pure asm; covers the two contiguous code blocks (K3-12 mask + EL drop dispatch). Five rejected alternatives enumerated, including "no EL drop" (status quo, breaks under -machine virtualization=on), Option B (multi-EL kernel code), Option C (hard-fail), DAIF mask in Rust (window unprotected), and SCTLR_EL1 configuration (out of scope). - UNSAFE-2026-0018: tyrne_hal::cpu::current_el safe wrapper. Documents the cfg-gating decision (absent on host) and the free-function-vs-trait-method choice from ADR-0024. - UNSAFE-2026-0016 Amendment (2026-04-27, T-013): records that the assertion is now a load-bearing post-condition of T-013's eret rather than a defensive guard against an absent transition, and that the read now goes through the current_el helper rather than duplicating the inline asm. docs/architecture/boot.md - Stage 1 wording updated: entry EL is now "EL1 (default) or EL2 (-machine virtualization=on or most real-hardware boot stacks)". - Stage 2 rewritten as three phases (K3-12 + EL drop + conventional setup) with the post-eret EL1 invariant explicit. - Line-by-line asm sample replaced with the new full _start body; cross-reference to UNSAFE-2026-0017 for the safety argument. - Invariants section gains "Interrupts are masked from the very first instruction" and "kernel_entry runs at EL1 unconditionally". - Trade-offs replace the "No EL drop" line with the ADR-0024 Option A trade-off summary; Open questions replace "Exception Level drop" with the future EL3→EL2→EL1 chain that ADR-0024 §Open questions tracks for hardware that requires it. docs/standards/bsp-boot-checklist.md - §1 (Exception level) rewritten as the always-drop-to-EL1 procedure (read CurrentEL, configure HCR_EL2/SPSR_EL2/ELR_EL2 on EL2, halt on EL3). UNSAFE-2026-0017 cross-referenced. - New §1a (K3-12) added covering the DAIF-mask-at-very-head-of- _start rule with a code sample and the failure mode. T-013 status: Draft → In Progress → In Review. Verification: cargo fmt clean; host-clippy clean; kernel-clippy clean; kernel-build clean; host-test 143/143 green; miri 143/143 clean. QEMU smoke not run from this development environment (harness cannot drive qemu-system-aarch64); maintainer/CI to run `qemu-system-aarch64 -M virt -kernel <binary>` (default config, EL1 entry) and again with `-machine virtualization=on` (EL2 entry) to verify both paths produce the unchanged A6 trace post-drop. ADR-0008 (Cpu trait) was deliberately NOT extended with a current_el method; ADR-0024 §Open questions documented the trade-off and the maintainer chose the free-function form. Refs: ADR-0024 Audit: UNSAFE-2026-0017, UNSAFE-2026-0018 Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
![sourcery-ai[bot]](https://avatars.githubusercontent.com/in/48477?s=60&v=4){kind=small}
There was a problem hiding this comment.
Sorry @cemililik, you have reached your weekly rate limit of 500000 diff characters.
Please try again later or upgrade to continue using Sourcery
|
Warning Rate limit exceeded
To keep reviews running without waiting, you can enable usage-based add-on for your organization. This allows additional reviews beyond the hourly cap. Account admins can enable it under billing. ⌛ How to resolve this issue?After the wait time has elapsed, a review can be triggered using the We recommend that you space out your commits to avoid hitting the rate limit. 🚦 How do rate limits work?CodeRabbit enforces hourly rate limits for each developer per organization. Our paid plans have higher rate limits than the trial, open-source and free plans. In all cases, we re-allow further reviews after a brief timeout. Please see our FAQ for further information. ℹ️ Review info⚙️ Run configurationConfiguration used: defaults Review profile: CHILL Plan: Pro Run ID: 📒 Files selected for processing (10)
📝 WalkthroughWalkthroughImplements a reset-to-EL1 boot sequence (mask DAIF, read CurrentEL, conditional EL2→EL1 via HCR_EL2/SPSR_EL2/ELR_EL2 + eret, halt on unexpected ELs), exposes a HAL Changes
Sequence Diagram(s)sequenceDiagram
participant Reset as Reset Vector
participant BootAsm as bsp boot.s (_start)
participant HAL as tyrne_hal::cpu
participant QemuCpu as QemuVirtCpu::new
participant Kernel as kernel_entry
Reset->>BootAsm: PC starts at _start
BootAsm->>BootAsm: msr daifset (mask interrupts)
BootAsm->>HAL: call current_el() (MRS CurrentEL)
alt CurrentEL == EL2
BootAsm->>BootAsm: write HCR_EL2, SPSR_EL2 (EL1h | DAIF masked)
BootAsm->>BootAsm: write ELR_EL2 = post_eret
BootAsm->>BootAsm: eret -> returns to post_eret at EL1
else CurrentEL == EL1
BootAsm-->>BootAsm: fallthrough (no-op)
else
BootAsm->>BootAsm: hang (wfe loop)
end
BootAsm->>BootAsm: SP init, CPACR_EL1 FP/SIMD enable, BSS zero
BootAsm->>Kernel: call kernel_entry
Kernel->>QemuCpu: QemuVirtCpu::new reads current_el() (via HAL)
Estimated code review effort🎯 4 (Complex) | ⏱️ ~60 minutes Possibly related PRs
Poem
🚥 Pre-merge checks | ✅ 5✅ Passed checks (5 passed)
✏️ Tip: You can configure your own custom pre-merge checks in the settings. ✨ Finishing Touches🧪 Generate unit tests (beta)
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
![gemini-code-assist[bot]](https://avatars.githubusercontent.com/in/956858?s=60&v=4){kind=small}
There was a problem hiding this comment.
Code Review
This pull request implements the Exception Level (EL) drop to EL1 in the QEMU virt boot stub, adds interrupt masking at reset, and introduces a current_el() HAL helper. It also significantly expands the project's documentation with new architecture guides for the scheduler and IPC, and adds 13 new host tests to improve coverage for critical kernel paths. Feedback was provided regarding the use of panic! in the scheduler's start_prelude function, suggesting a more graceful error handling approach for boot-time failures.
Comment on lines
+439
to
+441
| let Some(next_handle) = s.ready.dequeue() else { | ||
| panic!("scheduler start called with empty ready queue"); | ||
| }; |
There was a problem hiding this comment.
Using panic! in the scheduler's start_prelude is a critical failure during boot. While the comment notes this is a kernel programming error, consider if a more graceful recovery or a specific error type could be returned to avoid a hard panic in the boot sequence.
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 3
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (1)
bsp-qemu-virt/src/cpu.rs (1)
90-114:⚠️ Potential issue | 🟡 MinorUpdate audit references in doc-comments to reflect MRS delegation to HAL helper.
The inline-asm
MRS CurrentELblock originally audited underUNSAFE-2026-0016now lives in the safe wrappertyrne_hal::cpu::current_el(), audited underUNSAFE-2026-0018(per T-013 Amendment). Two doc-comment locations in this file still reference the pre-refactor layout and should be updated:
- Lines 90–93 (
# Panicsbullet): replaceAudit: UNSAFE-2026-0016withAudit: UNSAFE-2026-0018or add a note that 0016's scope was subsumed by the helper's audit.- Lines 19–26 (module-level Safety overview): include the now-relevant
UNSAFE-2026-0018entry (and optionallyUNSAFE-2026-0016's amendment) to reflect what this BSP transitively relies on.Per coding guidelines, audit tracking must align with docs/standards/ when modifying unsafe code.
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@bsp-qemu-virt/src/cpu.rs` around lines 90 - 114, Update the doc-comments to reference the HAL wrapper's audit (UNSAFE-2026-0018) instead of the original inline-asm audit: in the panic/`# Panics` bullet for the unsafe fn new() replace the `Audit: UNSAFE-2026-0016` tag with `Audit: UNSAFE-2026-0018` (or note that 0016 was subsumed), and add/adjust the module-level Safety overview to include `UNSAFE-2026-0018` as the audit covering the `tyrne_hal::cpu::current_el()` helper (optionally noting 0016's amendment) so the comments accurately reflect that `current_el()` holds the MRS audit provenance used by new().
🧹 Nitpick comments (3)
hal/src/lib.rs (1)
37-37: Optional: consider a flat re-export instead of a public submodule.
pub mod cpu;exposes the whole module path, while every other HAL trait/utility is surfaced via flatpub use cpu::{…};at lines 42–49. A consistent alternative would be:Optional refactor
-pub mod cpu; +mod cpu; @@ -pub use cpu::{CoreId, Cpu, IrqGuard, IrqState}; +pub use cpu::{current_el, CoreId, Cpu, IrqGuard, IrqState};Note:
current_eliscfg(all(target_arch = "aarch64", target_os = "none"))-gated, so the re-export would need the same#[cfg(...)]attribute on thepub useline — or accept the asymmetry and keeppub mod cpu;as you have it.Either form is fine; flagging only because the rest of the public surface uses the flat-re-export pattern. Feel free to ignore.
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@hal/src/lib.rs` at line 37, The public API currently exposes the entire cpu module via `pub mod cpu;` which is inconsistent with the rest of the crate that uses flat re-exports (`pub use cpu::{...}` at the later section); change the module export to flat re-exports by removing or making the `pub mod cpu;` private and instead adding `pub use cpu::{CpuTrait, SomeType, ...};` (matching the actual items listed at lines 42–49) so the public surface is consistent; if you need to keep `current_el` which is gated by `#[cfg(all(target_arch = "aarch64", target_os = "none"))]`, ensure that the corresponding `pub use` for that symbol carries the same cfg attribute to preserve build gating.docs/analysis/tasks/phase-b/T-011-missing-tests-bundle.md (1)
29-46: Minor: AC and DoD checkboxes still all unchecked despite status promotion toIn Review.The 2026-04-27 review-history entry asserts that both AC gates are met (sched ≥ 90 %, workspace ≥ 96 %), Miri 143/143, all clippy/fmt/build gates clean, etc. — yet every AC item (lines 31–46) and every DoD item (lines 70–78) is still rendered as
[ ]. T-009's task file flipped its corresponding boxes to[x]at the same promotion stage; for consistency and reviewer scanability, consider flipping the boxes whose narrative the new entry already certifies as completed.Not blocking — just keeps the visual status of the task file in sync with the prose.
Also applies to: 68-78, 110-110
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@docs/analysis/tasks/phase-b/T-011-missing-tests-bundle.md` around lines 29 - 46, Update the task file's markdown checkboxes to reflect the promoted "In Review" status by marking as completed ([x]) the specific Acceptance Criteria items whose prose the 2026-04-27 review-history entry already certifies (e.g., "IpcError::ReceiverTableFull test", the "Slot-reuse with pending transfer cap test" pair, the "ipc_send_and_yield three-case bundle", "start() prelude refactor + test", the "cap/table.rs targeted sweep", the "R2 coverage re-run" and "Miri stays clean" items) and likewise flip the matching DoD checkboxes referenced in the review note; apply the same checkbox updates to the other sections called out in the comment (the blocks around the other specified ranges) so the visual [x]/[ ] state matches the documented review-history claims.hal/src/cpu.rs (1)
149-170: Add the "rejected alternatives" line to the SAFETY rationale to match the codebase's audit convention.The function-level safety paragraph (Lines 149–156) and the inline
// SAFETY:block (Lines 161–163) cover why the read is needed and what invariants hold, but neither explicitly addresses why a safer alternative was rejected. Other unsafe blocks in the repo (e.g.kernel/src/sched/mod.rsLines 487–492 / 586–593) make this explicit. A one-liner like "no Rust intrinsic exposesCurrentEL; inline asm is the only available primitive" closes the (a)/(b)/(c) checklist locally without forcing a reader to chase UNSAFE-2026-0018.As per coding guidelines: Every
unsafeblock must have a comment explaining (a) why it is needed, (b) what invariants it upholds, (c) why safer alternatives were rejected.♻️ Proposed amendment to the function-level
# Safetysection/// # Safety /// /// `MRS x, CurrentEL` is a non-privileged read of a read-only system /// register. It is callable at every EL ≥ 0, does not modify any /// state, and `options(nostack, nomem)` is correct — there is no /// stack-pointer touch and no memory access. The function presents /// itself as `safe` because it upholds those invariants and returns a -/// plain `u8`. Audit: UNSAFE-2026-0018. +/// plain `u8`. Rejected alternatives: there is no Rust intrinsic or +/// `core::arch` wrapper for `CurrentEL`; inline asm is the only way +/// to issue an `MRS` of a system register from Rust. Audit: +/// UNSAFE-2026-0018.🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@hal/src/cpu.rs` around lines 149 - 170, Add a one-line "rejected alternatives" rationale to the function-level Safety paragraph and the inline `// SAFETY:` comment in `current_el()` to state why inline assembly is required (e.g., no Rust intrinsic or safe API exposes the `CurrentEL` register and inline asm is the only available primitive), so both the function docblock and the unsafe block explicitly cover (a) why the unsafe is needed, (b) what invariants hold, and (c) why safer alternatives were rejected; update the existing `# Safety` paragraph and the `// SAFETY:` comment above the `unsafe { core::arch::asm!(...) }` to include that one-liner referencing `CurrentEL` and `current_el()`.
🤖 Prompt for all review comments with AI agents
Verify each finding against the current code and only fix it if needed.
Inline comments:
In `@docs/architecture/boot.md`:
- Around line 16-17: Update the "Boot-time sequence" diagram to reflect the new
three-phase _start flow: show Phase 1 executing K3-12 with interrupts masked via
MSR DAIFSet,`#0xf`, Phase 2 performing the EL drop logic (reading CurrentEL and
handling EL2 by configuring HCR_EL2/SPSR_EL2/ELR_EL2 then eret, falling through
on EL1, halting on EL3), and Phase 3 doing the conventional setup (SP =
__stack_top, enable FP/SIMD via CPACR_EL1, zero BSS, branch to kernel_entry),
and note that later instructions run at EL1 and the T-009/UNSAFE-2026-0016
invariant is relied upon; ensure labels _start and kernel_entry appear in the
diagram and remove or replace the older SP/BSS-only path so text and diagram are
consistent.
In `@docs/architecture/ipc.md`:
- Around line 98-99: Reword the paragraph to remove the claim that the taxonomy
is "closed" and instead state that the enum is annotated #[non_exhaustive],
which explicitly allows future extension; keep the note that PendingAfterResume
is a special variant produced only by the scheduler bridge's resume path (not by
ipc_recv) and that it represents a kernel-internal invariant violation rather
than a userspace error, and preserve the ADR-0022 reference explaining why the
typed return replaced the untestable debug_assert!; in short, replace the
contradictory "closed taxonomy" wording with wording that #[non_exhaustive]
opens the taxonomy for extension while highlighting PendingAfterResume's
special, non-userspace semantics and the ADR rationale.
In `@kernel/src/cap/table.rs`:
- Around line 1111-1140: The test
drop_first_child_updates_parent_first_child_pointer is dropping the wrong
sibling: cap_derive prepends children so the most-recently-derived variable last
is actually the list head, not first; update the test to call t.cap_drop(last)
(and then assert lookup(last) is invalid) so unlink_from_siblings will hit the
head-of-list branch (parent.first_child == index) when exercising
unlink_from_siblings and cap_revoke on root will traverse the remaining
children.
---
Outside diff comments:
In `@bsp-qemu-virt/src/cpu.rs`:
- Around line 90-114: Update the doc-comments to reference the HAL wrapper's
audit (UNSAFE-2026-0018) instead of the original inline-asm audit: in the
panic/`# Panics` bullet for the unsafe fn new() replace the `Audit:
UNSAFE-2026-0016` tag with `Audit: UNSAFE-2026-0018` (or note that 0016 was
subsumed), and add/adjust the module-level Safety overview to include
`UNSAFE-2026-0018` as the audit covering the `tyrne_hal::cpu::current_el()`
helper (optionally noting 0016's amendment) so the comments accurately reflect
that `current_el()` holds the MRS audit provenance used by new().
---
Nitpick comments:
In `@docs/analysis/tasks/phase-b/T-011-missing-tests-bundle.md`:
- Around line 29-46: Update the task file's markdown checkboxes to reflect the
promoted "In Review" status by marking as completed ([x]) the specific
Acceptance Criteria items whose prose the 2026-04-27 review-history entry
already certifies (e.g., "IpcError::ReceiverTableFull test", the "Slot-reuse
with pending transfer cap test" pair, the "ipc_send_and_yield three-case
bundle", "start() prelude refactor + test", the "cap/table.rs targeted sweep",
the "R2 coverage re-run" and "Miri stays clean" items) and likewise flip the
matching DoD checkboxes referenced in the review note; apply the same checkbox
updates to the other sections called out in the comment (the blocks around the
other specified ranges) so the visual [x]/[ ] state matches the documented
review-history claims.
In `@hal/src/cpu.rs`:
- Around line 149-170: Add a one-line "rejected alternatives" rationale to the
function-level Safety paragraph and the inline `// SAFETY:` comment in
`current_el()` to state why inline assembly is required (e.g., no Rust intrinsic
or safe API exposes the `CurrentEL` register and inline asm is the only
available primitive), so both the function docblock and the unsafe block
explicitly cover (a) why the unsafe is needed, (b) what invariants hold, and (c)
why safer alternatives were rejected; update the existing `# Safety` paragraph
and the `// SAFETY:` comment above the `unsafe { core::arch::asm!(...) }` to
include that one-liner referencing `CurrentEL` and `current_el()`.
In `@hal/src/lib.rs`:
- Line 37: The public API currently exposes the entire cpu module via `pub mod
cpu;` which is inconsistent with the rest of the crate that uses flat re-exports
(`pub use cpu::{...}` at the later section); change the module export to flat
re-exports by removing or making the `pub mod cpu;` private and instead adding
`pub use cpu::{CpuTrait, SomeType, ...};` (matching the actual items listed at
lines 42–49) so the public surface is consistent; if you need to keep
`current_el` which is gated by `#[cfg(all(target_arch = "aarch64", target_os =
"none"))]`, ensure that the corresponding `pub use` for that symbol carries the
same cfg attribute to preserve build gating.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: defaults
Review profile: CHILL
Plan: Pro
Run ID: ca5c6ad8-f3c0-493d-9ce0-0e1916f33358
📒 Files selected for processing (29)
.claude/skills/write-adr/SKILL.md.github/workflows/ci.ymlbsp-qemu-virt/src/boot.sbsp-qemu-virt/src/cpu.rsdocs/analysis/reports/2026-04-27-coverage-rerun.mddocs/analysis/reviews/business-reviews/2026-04-27-T-009-mini-retro.mddocs/analysis/tasks/phase-b/README.mddocs/analysis/tasks/phase-b/T-008-architecture-docs.mddocs/analysis/tasks/phase-b/T-009-timer-init-cntvct.mddocs/analysis/tasks/phase-b/T-011-missing-tests-bundle.mddocs/analysis/tasks/phase-b/T-013-el-drop-to-el1.mddocs/architecture/README.mddocs/architecture/boot.mddocs/architecture/hal.mddocs/architecture/ipc.mddocs/architecture/overview.mddocs/architecture/scheduler.mddocs/audits/unsafe-log.mddocs/decisions/0025-adr-governance-amendments.mddocs/decisions/template.mddocs/roadmap/current.mddocs/roadmap/phases/phase-b.mddocs/standards/bsp-boot-checklist.mdhal/src/cpu.rshal/src/lib.rshal/src/timer.rskernel/src/cap/table.rskernel/src/ipc/mod.rskernel/src/sched/mod.rs
Verified each finding against the current code; 11 applied, 3 deliberately rejected with reasons recorded. Yüksek (blocking) — all fixed - UNSAFE-2026-0014 Amendment (T-011 commit 761af95): scope extended to cover `start_prelude` (the new T-011 site) and retroactively name `start` (a pre-existing site whose `// SAFETY:` comment cited this audit tag from commit f9b72f8 / T-006 but was never named in the original Location field). Single combined Amendment block; unsafe-policy §3 append-only. - ipc.md broken cross-references: three `T-003-ipc-primitive-set.md` links retargeted to the actual `T-003-ipc-primitives.md` (lines 12, 26, 168); one `bsp-qemu-virt/src/lib.rs` link retargeted to `bsp-qemu-virt/src/main.rs` (line 137 — BSP is a binary crate). - T-013 QEMU smoke remains genuinely deferred (cannot run from this development environment; flagged in PR #9 test plan checklist for the maintainer / CI runner). Not in this fix-round's scope. Inline comments — all fixed - boot.md "Boot-time sequence" Mermaid diagram updated to show the three-phase _start (Phase 1 K3-12 DAIF mask, Phase 2 EL drop with the EL2/EL1/EL3 alt branches, Phase 3 conventional setup); explicit note about the post-Phase-2 EL1 invariant and T-009 / UNSAFE-2026- 0016 load-bearing post-condition. - ipc.md "closed taxonomy" wording corrected: replaced the contradictory "taxonomy is closed and #[non_exhaustive]" framing with the accurate "annotated #[non_exhaustive] which deliberately *opens* it for future extension" framing. PendingAfterResume's special semantics + ADR-0022 rationale preserved. - kernel/src/cap/table.rs `drop_first_child_updates_parent_first_ child_pointer` test was actually testing the mid-list branch: cap_derive prepends children, so after first/middle/last the list head (parent.first_child) is `last`, not `first`. Fixed by dropping `last` instead of `first`. Comment expanded to document the prepend rule so future readers know why the variable name and list position are inverted. Outside-diff comments — all fixed - bsp-qemu-virt/src/cpu.rs module-level Safety overview now names UNSAFE-2026-0016 (with its T-013 Amendment) and UNSAFE-2026-0018 (the `current_el` helper) explicitly, plus a sentence noting the MRS now goes through the safe-Rust wrapper rather than duplicating inline asm. - `QemuVirtCpu::new` doc-comment for the EL panic case now references both audit entries (0016 for the assertion's load- bearing post-condition behaviour, 0018 for the helper providing the actual MRS) and cites ADR-0024 alongside ADR-0012 with a link definition added. Orta — all fixed - UNSAFE-2026-0017 §Invariants relied on gains a paragraph documenting why HCR_EL2 = 0x80000000 is a literal write rather than a read-modify-write (RMW would preserve firmware's reset values for E2H/TGE/IMO/FMO/AMO — bits the kernel must have at zero for non-VHE EL1 + EL1-bound trap handling); ARMv8.0 / 8.1+ baseline has no RES1 bits so the literal write does not violate any architecture-mandated bit; future BSPs targeting v8.2+ extensions should re-audit this assumption. - boot.md asm sample `;` → `//` (4+ inline comments). aarch64 GAS treats `;` as a statement separator, not a comment introducer; copy-pasting the original sample failed to assemble. Real boot.s uses `//` correctly; the doc now matches. - T-008 task file line 111: T-004 link retargeted from `T-004-scheduler-and-context-switch.md` (which never existed) to `../phase-a/T-004-cooperative-scheduler.md` (cross-phase relative path). Nitpicks — partially fixed - T-011 task file: all eight Acceptance-Criteria checkboxes and all nine Definition-of-Done checkboxes flipped from `[ ]` to `[x]`, with parenthetical delivery notes (e.g. "Delivered: 143" host tests, "Delivered: 93.97 % / 96.33 %" coverage). Visual state now matches the 2026-04-27 review-history row. - hal::cpu::current_el `# Safety` paragraph and the inline `// SAFETY:` comment gain explicit (a) why-unsafe-is-required, (b) invariants, (c) rejected-alternatives bullets per CLAUDE.md rule 2 ("every unsafe block must have a comment explaining a/b/c"). - hal/src/lib.rs `pub mod cpu` → keep as-is. The reviewer flagged this as "inconsistent with flat re-exports" but the existing `pub mod timer` already establishes the dual pattern (flat re-exports for the trait surface; submodule pub for free functions like `ticks_to_ns`); ADR-0024 §Open questions and T-013's task file both write `tyrne_hal::cpu::current_el()` as the canonical public path. Reverting to flat re-exports would change the documented path. Düşük — informational, not fixed - Commit body baseline test counts (D1) and llvm-cov sched pre-state delta (D2) — historical; commits not amended. - scheduler.md classDiagram array syntax (D3) — cosmetic, Mermaid-renderer-dependent; no observed render issue locally. - current_el host-test gating (D4) — resolved by T-013's QEMU smoke when it runs. - ipc.md state-diagram duplicate transition (D5) — cosmetic. Other comment (not numbered) — rejected - `panic!` in `start_prelude` (sched/mod.rs:439-441) — deliberate per ADR-0019 + ADR-0022 §Decision outcome ("empty ready queue is a kernel programming error; surfaces as a named panic at boot"), with idle task registered at boot making the panic structurally unreachable in v1. Keep. Verification: cargo fmt clean (rustfmt re-flowed one assert! call in the cap test as part of the fix); host-clippy / kernel-clippy / kernel-build clean; host-test 143 / 143 green; miri 143 / 143 clean. Refs: ADR-0024 Audit: UNSAFE-2026-0014, UNSAFE-2026-0017 Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Collaborator
Author
|
@coderabbitai review |
✅ Actions performedReview triggered.
|
There was a problem hiding this comment.
Actionable comments posted: 2
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (1)
bsp-qemu-virt/src/cpu.rs (1)
133-138:⚠️ Potential issue | 🟡 MinorStale SAFETY comment: parenthetical "
boot.sperforms no EL transition" is now incorrect.After T-013 (ADR-0024),
boot.sdoes perform an EL2→EL1 transition when entered at EL2 (audited underUNSAFE-2026-0017). The module-level doc-comment (lines 26-31) and the assertion's panic message (line 129) already reflect ADR-0024, so this// SAFETY:block is now the only remaining place in this file claiming no transition occurs. The safety argument still holds (we are at EL1 by the time the MRS runs, and the assertion above confirms it), but the justification text contradicts the new boot flow.The same stale parenthetical appears in the
now_nsSAFETY comment at lines 424-429 ("per ADR-0012 the kernel enters at EL1 and boot.s performs no EL transition") — please update both consistently.📝 Suggested wording (lines 133-138)
// SAFETY: `MRS x, CNTFRQ_EL0` is a non-privileged read of a read-only // system register. Tyrne enters `kernel_entry` at EL1 per - // [ADR-0012] (QEMU virt drops the kernel to EL1 before execution; - // `boot.s` performs no EL transition) — and the assertion above - // confirms this at runtime, so the EL-precondition reasoning that - // follows is not just documentation but a checked invariant. + // [ADR-0012] / [ADR-0024] (QEMU virt either delivers at EL1 directly + // or `boot.s` drops EL2→EL1 per ADR-0024; see UNSAFE-2026-0017) — + // and the assertion above confirms this at runtime, so the + // EL-precondition reasoning that follows is not just documentation + // but a checked invariant.As per coding guidelines: "Every
unsafeblock must have a comment explaining (a) why it is needed, (b) what invariants it upholds, (c) why safer alternatives were rejected."🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@bsp-qemu-virt/src/cpu.rs` around lines 133 - 138, Update the stale SAFETY comments that claim "boot.s performs no EL transition" in the SAFETY block immediately above the MRS x, CNTFRQ_EL0 usage and the SAFETY in the now_ns block so they reflect ADR-0024/T-013: mention that boot.s may perform an EL2→EL1 transition and that the safety argument instead relies on the runtime assertion (the existing EL-check/panic) which guarantees we are at EL1 before executing the non-privileged system register read; ensure each SAFETY comment still documents why the unsafe is required, which invariants (EL==1) are upheld, and that safer alternatives were considered and rejected.
🧹 Nitpick comments (2)
docs/analysis/tasks/phase-b/T-008-architecture-docs.md (1)
120-120: Comprehensive completion record.The review history entry thoroughly documents the deliverables (scheduler.md, ipc.md, hal.md Timer expansion, overview.md updates, README.md index), verification status (143/143 tests, clean builds), and state transition. The entry is dense but provides good traceability for the task completion.
💡 Optional: Consider breaking the entry into structured points for readability
While the current single-paragraph format works, table cells with complex content can sometimes benefit from line breaks or bullet structure. However, Markdown table formatting limits options, so this is purely a suggestion if you find the density impacts scanning later.
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@docs/analysis/tasks/phase-b/T-008-architecture-docs.md` at line 120, The table cell in T-008-architecture-docs.md is a dense single-paragraph release note; split it into clearer structured points for readability by breaking the content into short bullet-like lines (or HTML <br/> separated sentences) inside the table cell: list each new/updated doc on its own line with a short parenthetical summary (e.g., "docs/architecture/scheduler.md — FIFO + ContextSwitch + idle task + SchedError::Deadlock + raw-pointer bridge"), add a separate line for verification status (tests/build), and a final line for state transition ("Status → In Review"); update the single entry text (the one containing the file names and summaries) accordingly so scanners can quickly parse changes while preserving the same factual content.docs/audits/unsafe-log.md (1)
295-310: LGTM —UNSAFE-2026-0018correctly justifies the safe-fn / contained-unsafeboundary.The "Make the function
unsafe fn" rejected alternative (line 308) is the right framing: the MRS upholds the invariants required for a safe abstraction (read-only, side-effect-free, available at every EL ≥ 1), so the containedunsafeblock in the body is the correctly-narrow scope. The cfg-gate rationale (line 302) is also well-stated.One small clarification opportunity: line 302 says reading
CurrentELon a hosted EL0 target "would trap or yieldEL0" —CurrentELisUNDEFINEDat EL0 and will trap; it does not "yield EL0". Consider tightening the wording to remove the "or yield EL0" half so the cfg-gate justification reads unambiguously.🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@docs/audits/unsafe-log.md` around lines 295 - 310, Tighten the cfg-gate wording in the UNSAFE-2026-0018 entry: replace the phrase that says reading CurrentEL on a hosted EL0 target "would trap or yield `EL0`" with a definitive statement that reading the system register CurrentEL at EL0 is UNDEFINED and will trap; update the sentence referencing CurrentEL (and the free function current_el) so it unambiguously says it traps on hosted/EL0 targets and remove the "or yield `EL0`" alternative.
🤖 Prompt for all review comments with AI agents
Verify each finding against the current code and only fix it if needed.
Inline comments:
In `@docs/architecture/boot.md`:
- Line 41: The diagram uses an ambiguous branch syntax "Note over Asm: halt:
wfe; b .-" which is inconsistent with the explicit label used in the detailed
asm; change the diagram to match the line-by-line form by using the named label
and clear branch (e.g., "halt_unsupported_el: wfe; b halt_unsupported_el" or use
an unambiguous self-branch like "b .") so it aligns with the detailed asm and
the reference UNSAFE-2026-0017; update the diagram text that currently contains
"halt: wfe; b .-" to the chosen unambiguous form mentioning halt_unsupported_el.
In `@docs/audits/unsafe-log.md`:
- Line 277: The audit text uses non-standard GAS local-label backref syntax
"wfe; b -1b" which is invalid; update the sequence around "mrs x0, CurrentEL" so
the halt path uses a valid branch target (either "b 1b" with a matching "1:"
local label or a named label like "b halt_unsupported_el" and a corresponding
"halt_unsupported_el:"), and ensure the branch label matches the style used in
boot.md to keep the docs consistent.
---
Outside diff comments:
In `@bsp-qemu-virt/src/cpu.rs`:
- Around line 133-138: Update the stale SAFETY comments that claim "boot.s
performs no EL transition" in the SAFETY block immediately above the MRS x,
CNTFRQ_EL0 usage and the SAFETY in the now_ns block so they reflect
ADR-0024/T-013: mention that boot.s may perform an EL2→EL1 transition and that
the safety argument instead relies on the runtime assertion (the existing
EL-check/panic) which guarantees we are at EL1 before executing the
non-privileged system register read; ensure each SAFETY comment still documents
why the unsafe is required, which invariants (EL==1) are upheld, and that safer
alternatives were considered and rejected.
---
Nitpick comments:
In `@docs/analysis/tasks/phase-b/T-008-architecture-docs.md`:
- Line 120: The table cell in T-008-architecture-docs.md is a dense
single-paragraph release note; split it into clearer structured points for
readability by breaking the content into short bullet-like lines (or HTML <br/>
separated sentences) inside the table cell: list each new/updated doc on its own
line with a short parenthetical summary (e.g., "docs/architecture/scheduler.md —
FIFO + ContextSwitch + idle task + SchedError::Deadlock + raw-pointer bridge"),
add a separate line for verification status (tests/build), and a final line for
state transition ("Status → In Review"); update the single entry text (the one
containing the file names and summaries) accordingly so scanners can quickly
parse changes while preserving the same factual content.
In `@docs/audits/unsafe-log.md`:
- Around line 295-310: Tighten the cfg-gate wording in the UNSAFE-2026-0018
entry: replace the phrase that says reading CurrentEL on a hosted EL0 target
"would trap or yield `EL0`" with a definitive statement that reading the system
register CurrentEL at EL0 is UNDEFINED and will trap; update the sentence
referencing CurrentEL (and the free function current_el) so it unambiguously
says it traps on hosted/EL0 targets and remove the "or yield `EL0`" alternative.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: defaults
Review profile: CHILL
Plan: Pro
Run ID: fffc7581-24a3-4599-b66c-6510d2cbe29a
📒 Files selected for processing (8)
bsp-qemu-virt/src/cpu.rsdocs/analysis/tasks/phase-b/T-008-architecture-docs.mddocs/analysis/tasks/phase-b/T-011-missing-tests-bundle.mddocs/architecture/boot.mddocs/architecture/ipc.mddocs/audits/unsafe-log.mdhal/src/cpu.rskernel/src/cap/table.rs
✅ Files skipped from review due to trivial changes (1)
- docs/architecture/ipc.md
🚧 Files skipped from review as they are similar to previous changes (2)
- hal/src/cpu.rs
- docs/analysis/tasks/phase-b/T-011-missing-tests-bundle.md
…le SAFETY) Verified each finding; all five applied as suggested. Inline #1 — boot.md halt-loop syntax in Mermaid diagram + body text - Line 41 (Mermaid sequence diagram): `halt: wfe; b .-` → `halt_unsupported_el: wfe ; b halt_unsupported_el`. The named-label form matches the actual asm in `bsp-qemu-virt/src/boot.s` and removes the malformed `.-` token. - Line 16 (text description): `wfe; b .-` halt loop wording corrected in two places — the EL3 path now reads "named-label `wfe`-loop (`halt_unsupported_el: wfe ; b halt_unsupported_el`)" and the kernel_entry-return defensive halt now reads `wfe ; b 2b` (matching the local-label loop at the bottom of `_start`). Inline #2 — UNSAFE-2026-0017 GAS halt-loop syntax (Amendment) - §Operation said "halt via `wfe; b -1b`". `-1b` is not valid GAS syntax — `1b` is the back-reference to local label `1:`, but a leading `-` is meaningless there. Real asm uses `b halt_unsupported_el`. - §Rejected alternatives → "Halt on EL3 with a panic frame" said "`wfe; b .-` is the visible silence". `b .-` is a similar malformed token (`.` is the current address; `b .-` with no offset is not a valid branch target). - Both occurrences corrected via an Amendment block per unsafe-policy.md §3 (the entry was committed in f289d4d / T-013; in-place edits to a committed entry's body are forbidden). The behaviour the audit describes is unchanged; only the prose's asm rendering was wrong. Outside-diff #4 — bsp-qemu-virt/src/cpu.rs SAFETY blocks for CNTFRQ_EL0 (`new()`) + CNTVCT_EL0 (`now_ns()`) - Both blocks claimed "boot.s performs no EL transition" — true before T-013, stale after. Updated to reflect ADR-0024: `boot.s` drives an EL2 → EL1 transition when the firmware/emulator delivers at EL2, falls through at EL1, halts at EL3. The runtime EL-check via `tyrne_hal::cpu::current_el()` (audited under UNSAFE-2026-0018) is the checked invariant pinning `CurrentEL == 1` at this point. Both SAFETY paragraphs now name UNSAFE-2026-0017 (the boot.s sequence) explicitly, and document (a) why-unsafe-is- required, (b) invariants, (c) rejected alternatives per CLAUDE.md rule 2. Nitpick — UNSAFE-2026-0018 cfg-gating wording (Amendment) - §Invariants relied on → "Cfg-gating" said "user code reading `CurrentEL` would trap or yield `EL0` with no useful information". The "or yield `EL0`" alternative is wrong: per ARM ARM §D11.2 / §C5.2, `MRS x, CurrentEL` at EL0 is undefined — the system register is not accessible at EL0 and the read raises an Undefined Instruction exception (which becomes `SIGILL` on hosted Unix-like targets such as `aarch64-apple-darwin`). There is no fallback EL0 read. Corrected via Amendment block (same §3 reasoning as UNSAFE-2026-0017 above). Nitpick — T-008 task file:120 review-history release-note structure - Single dense paragraph split into structured bullets using `<br/>•` separators inside the table cell: New docs / Updated docs / Scope discipline / Verification / State transition. Same factual content, scannable. Verification: cargo fmt clean; host-clippy / kernel-clippy / kernel- build clean; host-test 143 / 143 green. Refs: ADR-0024 Audit: UNSAFE-2026-0015, UNSAFE-2026-0017, UNSAFE-2026-0018 Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Collaborator
Author
|
@coderabbitai review |
✅ Actions performedReview triggered.
|
Verified each open item from the second review pass. All applied; the deferred Q1 settled with a strict-§3 discipline call. Q1 (HCR_EL2 Amendment) — strict discipline picked over carve-out The first review-round (commit 9a8e312) added the HCR_EL2 literal- write rationale to UNSAFE-2026-0017's §Invariants relied on as an in-place body edit. The second review-round flagged this as asymmetric against V13/V14 (which went via Amendment) and offered two paths: (1) codify a same-PR-mutable carve-out in unsafe-policy.md §3, or (2) convert V7 to an Amendment. Picked Path 2 (strict). Reasoning, in detail: - The asymmetry within the PR is the actual problem; Path 1 does not fix it because V13/V14 went via Amendment despite being same- PR. The carve-out would need a sub-rule "additions in-place, corrections via Amendment" — a gray-zone rule that just opens more gray zones. - Precedent: UNSAFE-2026-0006's 2026-04-23 Amendment for the post- T-009 QemuVirtCpu struct shape is exactly this pattern — adding to an existing entry's content via Amendment. Strict §3 reading matches the precedent. - The §3 text "must not be rewritten once committed" is unambiguous when read literally. The strict reading is what the rule says. - "Merge boundary" as the locking event introduces a second ambiguity (PR merge ≠ commit, and not observable from inside the audit log). Strict introducing-commit boundary is auditable. Mechanics: removed the HCR_EL2 paragraph from §Invariants relied on (reverting to f289d4d's introducing-commit shape); added a new Amendment block at the end of UNSAFE-2026-0017 with the same content + a "Discipline note for future readers" paragraph documenting the introducing-commit boundary so the next PR does not stumble into the same trap. The existing 2026-04-27-second-review-round Amendment (GAS halt-loop syntax correction) stays as-is, now placed after the HCR_EL2 Amendment in chronological order (first review-round commit 9a8e312 → HCR_EL2; second review-round commit 39dd978 → GAS-syntax). Orta #1 — T-008 + T-013 task-file checkbox flips Same discipline T-011 received in 9a8e312, applied to T-008 and T-013. Every delivered AC + DoD item flipped to [x] with parenthetical delivery notes. T-013's two QEMU smoke items (AC "Tests — QEMU smoke at default config" / "QEMU smoke at -machine virtualization=on" + DoD's QEMU smoke line) are *intentionally* left at [ ] — settled item 8 from the second review pass: those gates are deferred to the maintainer / CI runner and the PR test plan checklists them explicitly. T-008's "Cross-references go both ways" DoD item is now [x] thanks to Düşük #3 below. Düşük #1 — boot.s:21 leading-comment typo Same wfe; b .- malformed token that V13 corrected via Amendment in UNSAFE-2026-0017 also appeared in bsp-qemu-virt/src/boot.s line 21 (the leading comment block, not the actual asm — the asm uses the named-label form correctly). In-source comment, not audit-log body; in-place fine. Replaced with the named-label loop description so the comment matches the asm. Düşük #2 — coverage rerun report follow-up note The 2026-04-27 coverage report's tables describe T-011's 761af95-tip state. The second review-round's drop_first_child_… test fix (in 9a8e312) bumped cap/table.rs regions from 97.46 % → 97.60 % (+0.14 pp), with a corresponding +0.04 pp on the workspace total (96.33 % → 96.37 %). The original tables are intentionally not rewritten — the report describes T-011's tip; the post-fix delta lives in a follow-up note appended to the report. Both AC gates (sched ≥ 90 %, workspace ≥ 96 %) remain comfortably met. Düşük #3 — bidirectional ADR ↔ architecture-doc cross-references T-008's DoD line 88 ("Cross-references go both ways") was deferred ("ADRs cited from architecture docs are the same ADRs whose §References sections cite the new architecture docs — or will cite, in their next rider"). Closed in this commit with five short §Revision notes riders pointing back at the architecture docs: - ADR-0010 (Timer trait) → architecture/hal.md Timer subsection. - ADR-0017 (IPC primitive set) → architecture/ipc.md. - ADR-0019 (Scheduler shape) → architecture/scheduler.md. - ADR-0020 (ContextSwitch + Cpu v2) → architecture/scheduler.md. - ADR-0022 (Idle task + typed Deadlock) → architecture/scheduler.md. ADR-0021 already had a direct architecture/scheduler.md citation (observed by the second review pass), so it does not need a rider. Each rider is one short paragraph dated 2026-04-27, framed "pointer to architecture doc" — same shape as ADR-0013's 2026-04-27 pointer-to-ADR-0025 rider. ADR-0019's rider also notes that its previously-open "Idle task" question was settled by ADR-0022. Verification: cargo fmt clean; host-clippy / kernel-clippy / kernel-build clean; host-test 143 / 143 green. Refs: ADR-0010, ADR-0017, ADR-0019, ADR-0020, ADR-0022, ADR-0024 Audit: UNSAFE-2026-0017 Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
cemililik
added a commit
that referenced
this pull request
Apr 27, 2026
Maintainer merged PR #9 to main (merge commit 9a66e8b). Closes the three In-Review tasks, marks the milestone, and updates the active state on `development`. T-008 / T-011 / T-013 promoted In Review → Done - All AC and DoD checkboxes reconciled with delivery (T-013's two QEMU smoke gates flipped to [x] with "Verified by maintainer 2026-04-27 prior to PR #9 merge"). Each task gains a final review-history row crediting the PR-merge promotion event and summarising the outcome of the two independent review passes (24 findings closed across `9a8e312` + `39dd978` + `9680e41`). phase-b/README.md status column flipped to Done for all three. phase-b.md - §B0 §"Tasks under B0": T-008 / T-011 status updated; T-010 (optional split) annotated "explicitly not opened — T-007 closed without needing the split". - §B0 §"Acceptance criteria": every line now carries a ✅ with a delivery cite or a deliberate-deferral note. ADR-0023 explicitly on the accept-deferred path; the "three architecture docs" expectation reduced to two with the kernel-core.md / scheduling.md pair subsumed into scheduler.md + ipc.md per T-008's scope- discipline call. Final test count 143 (vs the 109+ target). B0 declared **closed 2026-04-27** at the end of the AC list. - §B1 sub-breakdown items 1-4 marked ✅ delivered (ADR-0024, asm extension + K3-12, current_el helper, two QEMU smoke gates). Item 5 (T-012 exception infrastructure) remains the open B1 thread. current.md - Active phase B unchanged; active milestone shifted from "B0 in progress" to "B1 with T-013 done, T-012 the remaining work". - Active task: None. - "In review" cleared (was three; all three promoted). - "Last completed milestone" updated from A6 to B0 with the headline numbers (143 host tests, 93.97% sched / 96.33% workspace coverage, miri clean, two new architecture docs, three new audit entries plus four Amendments). - "Last completed tasks" updated to T-008 / T-011 / T-013, with a one-line note on the rule-validation outcome (zero post-Accept ADR riders during PR #9 — empirical first run of ADR-0025's §Rule 1 / §Rule 2). - "Active decisions": ADR-0024 description updated to "Implemented by T-013 (Done)" rather than "now unblocked". - "Next task to open": T-012 named as the next natural pickup. - "Next review trigger": B0 closure retrospective (with the cost- of-arc analysis the T-009 mini-retro's second-follow-up agenda pre-loaded for it) + the optional consolidated B0 security review. - "unsafe audit status" line refreshed to reflect the post-PR-#9 shape: UNSAFE-2026-0014 Amendment, UNSAFE-2026-0016 Amendment, UNSAFE-2026-0017 + 0018 active with the introducing-commit- boundary discipline note. Verification: cargo fmt clean; host-test 143 / 143 green (no functional changes — doc-only). Refs: ADR-0021, ADR-0022, ADR-0024, ADR-0025 Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
cemililik
added a commit
that referenced
this pull request
Apr 28, 2026
…ment items Closes the B0 milestone with two review artefacts and acts on four of the six adjustment items the retros surfaced. T-012 (B1's remaining task) and the future-session items wait for QEMU access; tracked in the retro Adjustments and current.md as the next-trigger. Two new review artefacts: - docs/analysis/reviews/business-reviews/2026-04-27-B0-closure.md Full milestone retrospective. Cost-of-arc analysis (Phase A: ~2 days / ~30 commits / 109 tests; B0: ~6 days / 50+ commits / 143 tests; 3× ratio explained by ADR-0025 emergence + review fix-rounds + audit-log discipline establishment, all one-time costs). Records ADR-0025 §Rule 1's first empirical run (zero post-Accept ADR riders during PR #9 — rule fired correctly). Lessons from the audit-log Amendment-vs-in-place asymmetry resolution. Closes 4 of 6 pre-loaded T-009 mini-retro items. - docs/analysis/reviews/security-reviews/2026-04-27-B0-closure.md 8-axis adversarial pass over UNSAFE-2026-0006..0018 plus the four post-introduction Amendments. Verdict: clean, no Yüksek findings. Two pre-existing items (cross-table revocation, generation overflow) re-stated at original severity. Two new positive observations: Amendment discipline codified; architecture docs identified as a security multiplier (recommendation: T-012 ships exceptions.md as a hard deliverable, not a follow-up). Both review-folder README indices updated with the new rows. A1: .claude/skills/conduct-approval-review/SKILL.md The independent verification pass that PR #9 ran three times (T-006/ T-007/T-009 promotion; ADR-0024/0025 Accept; T-008/T-011/T-013 promotion) is now canonised as a skill. Distinct from perform-code-review (style + correctness) and perform-security- review (adversarial axis): this skill is the promotion gate that verifies an artefact's claims about its own state match reality. Procedure: settled-decisions context → verification list (V1..VN) → reproduce gates locally → audit-log discipline spot-check → review dimensions → per-artefact AC audit → verdict (✅/🟡/❌). Anti- patterns explicitly cover "LGTM without verification list" and "re-litigating settled decisions" — the two failure modes the prior review rounds surfaced. .claude/skills/README.md index updated. A2: docs/standards/code-review.md Author's responsibilities item 7 Three data points (T-009 review-fix cascade, cool-down withdrawal ripple in PR #9 first round, ipc.md broken-link sweep in PR #9 second round) tip the post-fix sweep rule into codification. "After fixing a doc typo, renaming a symbol, or changing a literal string that may appear in multiple places, the author runs git grep -F '<old-token>' before staging." Specific failure modes named; reviewer-side verification step ("reviewers verify by running the same grep on the change's tip") added. A3: T-012 task file's Documentation AC tightened docs/architecture/exceptions.md is now a *required* deliverable (was conditional / optional in the original task file). Citation: B0 closure security review §8 ("Architecture docs are a security multiplier"). The doc must explain vector-table layout, dispatch flow, GIC programming sequence, and how IRQ delivery interacts with ADR-0021's raw-pointer scheduler bridge (likely an ADR-0021 Amendment when wired). exceptions.md lands alongside T-012's code, not as a follow-up. A4: B0 retro Adjustments section reflects the new state Three items flipped to [x] (post-fix sweep DoD codified; approval- review skill canonised; T-012 DoD updated for exceptions.md); the consolidated security review item flipped to [x] (delivered as the parallel security-review artefact); T-012 In Progress and B2 prep stay [ ] (deferred to a session with QEMU access). Performance baseline re-run stays [ ] (post-T-012). New [ ] item added: 2026-05-04 ADR-0024 rider-rate re-measurement per ADR-0025 §Rule 2 calibration. current.md updated: - "Last reviews" section gains the two new B0-closure reviews at the top. - "Next review trigger" replaced with B1 closure (T-012 Done + consolidated B1 security review + performance baseline re-run); separate scheduled trigger for the 2026-05-04 ADR-0024 rider-rate measurement. Future-session items (tracked in todo list, not closed in this commit): - B1: T-012 full implementation (needs QEMU access). - B2: docs/architecture/exceptions.md (bundled with T-012). - C1: performance baseline re-run (post-T-012). - C2: B1 closure retrospective (post-T-012). - C3: B1 consolidated security review (post-T-012, GIC focus). - C4: ADR-0024 first-week rider rate measurement (2026-05-04). Verification: cargo fmt clean; host-clippy / kernel-clippy / kernel-build / host-test (143 / 143) all green. No code changes in this commit — pure docs + skill addition. Refs: ADR-0021, ADR-0022, ADR-0024, ADR-0025 Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
cemililik
added a commit
that referenced
this pull request
Apr 28, 2026
Replaces eight `<TBD-commit-3>` placeholders with the actual SHA landed for the documentation sweep. Also flips the `exceptions.md` status banner from "In Progress" to "In Review" with the three implementation commits cited. Same back-fill pattern as commit 330e998 (UNSAFE-2026-0011 Amendment SHA back-fill from PR #9). The amendments themselves were correctly written in the introducing commit (28c5ce9) per unsafe-policy.md §3 + ADR-0025 §Rule 2; this is the SHA-resolution follow-up. Refs: T-012, ADR-0021 (Amendment), ADR-0022 (Sub-rider closure), ADR-0010 (Revision notes) Audit: UNSAFE-2026-0014 (Amendment SHA back-fill) Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
cemililik
added a commit
that referenced
this pull request
Apr 28, 2026
Two Düşük findings from the T-012-arc approval review:
1. `bsp-qemu-virt/src/main.rs::idle_entry` — function-level doc-comment
was stale: still described the body as `spin_loop` + `yield_now`
("not `wfi` + `yield_now` — until a timer IRQ source lands (T-009)")
and projected `wait_for_interrupt` as future work. The body itself
landed in commit b4ed68c using `cpu.wait_for_interrupt()`; only the
doc-comment lagged. The PR-#9 post-fix-sweep DoD rule
(code-review.md item 7 — `git grep -F` after a behaviour change)
would have caught this. Rewritten to describe the now-current
behaviour: WFI + yield, ADR-0022 first-rider Sub-rider closed,
v1's IPC demo never reaching idle in practice (so WFI is
structurally unreachable in the demo path).
2. `docs/decisions/0021-raw-pointer-scheduler-ipc-bridge.md:123` —
Amendment header read "2026-04-27" but the cited commit `28c5ce9`
landed 2026-04-28; the matching UNSAFE-2026-0014 Amendment in
`docs/audits/unsafe-log.md:225` already had the correct
2026-04-28 date. One-character fix bringing the two Amendments
into agreement on when the discipline-extension landed.
Bilgi #3 (TrapFrame `_reserved` never written by trampoline) and
Bilgi #4 (`compiler_fence` on spurious-acknowledge path is defensive)
are noted but not actioned — observation-grade only.
Gates: cargo fmt / host-clippy / kernel-clippy / kernel-build clean.
148/148 host tests unchanged (no code paths touched).
Refs: T-012, ADR-0021 (Amendment), ADR-0022 (Sub-rider closure)
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
5 tasks
cemililik
added a commit
that referenced
this pull request
Apr 28, 2026
Code (5 fixes): 1. `bsp-qemu-virt/src/exceptions.rs` — irq_entry and panic_entry are now `unsafe extern "C" fn` (was `extern "C" fn`). Both have caller-side safety preconditions (frame validity for irq_entry; class validity for panic_entry) already documented in `# Safety` doc-comments; making them `unsafe fn` enforces the contract at the type level for any future Rust caller. The asm trampolines `bl` them unchanged. 2. `bsp-qemu-virt/src/gic.rs` — enable/disable now assert `irq.0 < GIC_MAX_IRQ` (1020) per ARM IHI 0048B §4.3.2 before computing distributor offsets. Without the check, an out-of-range IrqNumber would compute an MMIO offset outside the distributor window even with saturating arithmetic — writing to reserved or wrong-window addresses. The IrqController trait returns no Result, so panic is the right mechanism for kernel-internal contract violations. SAFETY comments updated to cite the range invariant. 3. `hal/src/timer.rs` — ns_to_ticks switched from floor to ceiling division (via `u128::div_ceil`). ADR-0010 §Decision outcome specifies `arm_deadline` semantics as "When `now_ns()` reaches or exceeds `deadline_ns`, the hardware timer IRQ fires"; flooring could arm the comparator at a tick whose time-equivalent is sub-tick *before* deadline_ns, violating the contract. Ceiling guarantees the comparator's tick-equivalent is ≥ deadline_ns. New `# Rounding` doc section explains the choice. Existing tests (round-trip at 62.5 MHz divisor frequency, one-second-yields- frequency at multiple frequencies, zero-ns, panic-on-zero-frequency) all still pass — they exercise frequencies that divide evenly into 1e9 ns/s, where ceiling and floor agree. 4. `hal/src/timer.rs::ns_to_ticks_saturates_at_u64_max` — added two over-boundary cases (`freq = 1_000_000_001` and `freq = u64::MAX`) so the saturation *branch* (not just the boundary) is exercised. The original test hit only the exact boundary (`huge_ns * 1e9 = u64::MAX * 1e9` divides exactly). 5. `bsp-qemu-virt/src/exceptions.rs::TrapFrame` — no code change; the doc-comment's "Padding" claim about `_reserved` was already correct. Reviewer's Bilgi #3 was an observation, not a fix request. Documentation (8 fixes): 6. `.claude/skills/conduct-approval-review/SKILL.md` — Turkish quote in line 30 translated to English ("kabul edilen bulguların tamamı düzeltildi mi?" → "Have all accepted findings been fixed?"); severity labels in the output-format template translated (`Yüksek`/`Orta`/`Düşük` → `High`/`Medium`/`Low`); the line-53 "Yüksek finding" prose translated; the example fenced code block gained a `markdown` language tag. CLAUDE.md §3 mandates English in all committed artefacts. 7. `docs/analysis/reviews/business-reviews/2026-04-27-B0-closure.md` — "Five `unsafe` regions" → "Seven" to match the actual table count (UNSAFE-2026-0012 through 0018 inclusive = 7 entries). 8. `docs/analysis/tasks/phase-b/README.md` — T-012 row status changed from `In Progress (design-first 2026-04-28)` to `In Review (2026-04-28)` to match the task file's header. 9. `docs/architecture/exceptions.md` — IRQ dispatch flow Mermaid diagram updated to reflect shipped behaviour: timer-IRQ branch now shows "msr CNTV_CTL_EL0 → gic.end_of_interrupt → return" (ack-and-ignore for v1) instead of the placeholder sched::on_timer_irq call. Spurious-INTID arm added (returns without EOI per GICv2 architecture spec). Saved-register list corrected: trampoline saves `x0..x18, x30` (not `x0..x29`); the prose now explicitly states that `x19..x29` are AAPCS64 callee-saved and preserved by the Rust handler, not pushed by the trampoline. 10. `docs/decisions/0021-raw-pointer-scheduler-ipc-bridge.md` — the Amendment paragraph that said "When the first scheduler-touching IRQ handler lands, ... UNSAFE-2026-0014 ... gains an Amendment" reworded to reflect that the Amendment **already exists** (commit `28c5ce9`) and v1's body has no live citation yet because `irq_entry` is ack-and-ignore. Future scheduler-touching arcs add a follow-up Amendment recording the activation. 11. `docs/roadmap/current.md` — pre-T-011 baseline coverage numbers reconciled with the canonical B0 closure retro: sched/mod.rs was `83.93%` → `84.16%`; workspace was `96.33%` → `96.37%`. The post- T-011 numbers (93.97% / 96.37%) were already correct. 12. `docs/roadmap/phases/phase-b.md` — "T-012 closed" → "T-012 delivered (pending verification)". The bullet's existing parenthetical already explained that closure waits on QEMU verification; the lead label is now consistent with that. 13. `docs/analysis/tasks/phase-b/T-012-exception-and-irq-infrastructure.md` — Dependencies field: T-009 status `In Review` → `Done` (closed 2026-04-27 via PR #9); ADR-0024 mention sharpened to record its Accept date (2026-04-27). Bilgi findings #3 (`TrapFrame._reserved` never written) and #4 (spurious-acknowledge `compiler_fence` is defensive-not-load-bearing) intentionally not actioned per their "no action today" tags. Gates: cargo fmt / host-clippy / kernel-clippy / kernel-build all clean. host-test 148 / 148 unchanged (24 hal + 90 kernel + 34 test-hal); the new ns_to_ticks_saturates_at_u64_max assertions extend an existing test rather than add a new one. Refs: T-012, ADR-0010 (rounding clarification rider candidate), ADR-0021 (Amendment reword), ADR-0024 (precondition language) Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
5 tasks
cemililik
added a commit
that referenced
this pull request
Apr 29, 2026
Approval review on PR #11 returned a punch-list: 5 inline comments + 1 nitpick + 3 PR-level comments + 2 overall comments. This commit applies 9 of the 10 actionable findings; 1 finding (security review §4 irq_entry "loop" claim) was verified false against the source and is rejected with explanation below. The 2 overall comments (pattern-deduplication, narrative-tightening) are noted as known follow-up concerns but are out-of-scope for this commit. Findings applied: (F1) `docs/analysis/reviews/performance-optimization-reviews/` `2026-04-28-B1-closure.md` — security cross-reference line: "one forward-flagged non-blocking item" → "two forward-flagged non-blocking items" with both names (`arm_deadline` CVAL+CTL race + `cancel_deadline` CTL+GIC race). Synchronises with the security review (which gained the second item in commit `a5d4f9b`). (F3) `docs/analysis/reviews/security-reviews/2026-04-28-B1-closure.md` §Verdict — "no Yüksek findings" → "no high-severity findings". Brings the B1 trio's verdict prose under CLAUDE.md §3 (English in repository) without disrupting the established conduct-approval-review SKILL template's Turkish severity-label vocabulary (which the user explicitly approved earlier as "established pattern"). Scope kept narrow: this commit translates only the B1 trio's instances; the B0 closure security review's index entry retains "Yüksek" as a pre-existing committed artifact (unsafe-policy.md §3 Amendment discipline applies to audit-log entries, not review artifacts, but a broader sweep is a separate scope question and not trigger-driven by this review round). (F4) `docs/analysis/reviews/security-reviews/README.md` line 36 — same Yüksek → high-severity translation in the index entry's Verdict cell. (F5) `docs/analysis/tasks/phase-b/T-012-exception-and-irq-` `infrastructure.md` Definition-of-done checklist line 82 — "Task status updated to `In Review`" → "Task status updated to `Done`". The Status field at line 5 was already `Done` from ffefb76; the DoD checklist line was a stale residual from the `In Review` promotion. Now consistent. (F6) `docs/roadmap/phases/phase-b.md` B1 milestone status block — "B1 closure review trio is pending" → "B1 closure review trio landed 2026-04-28 via PR #11" with deep-links to the three artefacts. Only QEMU smoke + Miri remain pending. The B1 milestone-level `Done` flip happens after the maintainer-side verification. (N1) `README.md` Status: line — split from a dense single-paragraph summary into a four-bullet status list (Phase A / Phase B B0 / Phase B B1 / Path forward) plus a final pointer to `docs/roadmap/current.md`. Each bullet is a concise summary; dates retained; "Status:" label retained. (P1) `docs/analysis/reviews/business-reviews/2026-04-28-B1-closure.md` §"Design-first arc" — math `19 + 2 + 2 = 23 total findings` → `21 total review items (19 substantive findings — 11 round-1 + 8 round-2 — plus 2 round-2 nitpicks; the round-1 nitpick disposition is folded into the 11 applied)`. The `19+2+2` arithmetic was wrong (sums to 23, but the breakdown didn't match either round's commit-message numbers). The new text gives a clear decomposition matching `d820a88` ("apply 11 of 12 findings") and `5c9cf06` ("8 findings + 2 nitpicks") commit messages. (P2) `docs/analysis/reviews/business-reviews/2026-04-28-B1-closure.md` §"File renames and stale-link drift" — paragraph that said the `umbrix → tyrne` rename would land in "a follow-up `docs(refs):` commit (the immediate next commit after this retro lands)" was stale: the rename DID land in commit `10e3351`, which is one of PR #11's four commits — the same PR that lands this retro. Updated to "the `docs(refs):` commit `10e3351` (one of the four commits in PR #11, the same PR that lands this retro)" with deep-link. The Adjustments item already correctly says ✅ Done; this paragraph now matches. (P3) Merge-commit-SHA back-fill across 3 documents. PR #10's merge into `main` is commit `7b42bbe` (verified via `git log --oneline 9a66e8b..origin/main`); the documents that said "merge commit SHA pending back-fill in a follow-up `docs(audits)`-style commit" are now updated to reference `7b42bbe` directly with a clickable PR #10 link. Affected files: - `docs/analysis/tasks/phase-b/T-012-exception-and-irq-` `infrastructure.md` (review-history Done promotion row). - `docs/analysis/reviews/security-reviews/` `2026-04-28-B1-closure.md` (Change frontmatter). - `docs/roadmap/current.md` (Last-completed-tasks line; also added merge-commit `9a66e8b` cross-reference for T-013/PR #9 to match PR #10's back-fill shape). The earlier framing was process-detail noise (`docs(audits)-` style follow-up commit) that made each document feel dated immediately after merge; the new framing names the merge commit directly and is evergreen. Finding rejected: (F2) Security review §4 "Kernel-mode discipline" — claim that `irq_entry` is "straight-line / loop-free / constant-time". The reviewer asserted this is incorrect because "irq_entry uses a loop to acknowledge pending IRQs via repeated GICC_IAR reads". Verified against the source ([`bsp-qemu-virt/src/exceptions.rs` `irq_entry`](docs/architecture/exceptions.md) lines ~145-193): `irq_entry`'s body is straight-line. There is no `loop`, no `while`, no `for`. The dispatch shape is: 1. `let gic = ...` (single static deref) 2. `let Some(irq) = gic.acknowledge() else { return };` (single GICC_IAR read; spurious → early return) 3. `if irq.0 == TIMER_IRQ_ID { ... return; }` (single dispatch arm; mask + EOI + return) 4. `panic!("unhandled IRQ")` (structurally unreachable in v1) `gic.acknowledge()` returns `Option<IrqNumber>` — a single IRQ ID, not an iterator. The function does NOT drain pending IRQs in a loop; the GICv2 architecture actually delivers one IRQ per acknowledge cycle. To process additional pending IRQs, the CPU re-takes the exception after `eret` (if more are pending and DAIF.I is unmasked), which goes through the trampoline + `irq_entry` again — but each `irq_entry` invocation handles exactly one IRQ. The "constant-time / straight-line" claim is therefore correct and remains in the security review unchanged. The reviewer's mental model may have come from a typical edge-triggered GIC handler that DOES loop on IAR until spurious — but Tyrne's choice (per [docs/architecture/ exceptions.md](docs/architecture/exceptions.md) §"Dispatch flow") is one-IRQ-per-entry; the documentation accurately reflects the implementation. Overall comments not addressed (noted as known concerns): - **`Pending QEMU smoke verification` pattern repetition.** The pattern appears in `current.md`, `phase-b.md`, the three review artefacts, and the T-012 task file. Factoring into a single canonical explanation (in `unsafe-policy.md` or a short standard) is the right shape; per the [B1 closure retro Adjustments item + Appendix #2](docs/analysis/reviews/business-reviews/2026-04-28-B1-closure.md), the canonisation trigger is "the next IRQ-related arc reproduces the pattern" — cross-arc reproducibility threshold. Not actionable in this commit. - **B1 narrative repetition across files.** Real concern but addressing it via cross-linking would substantially restructure multiple committed review artefacts (which are append-only-style per the project convention). Better handled at the next milestone retro's plan-diff section, when the retro can decide whether to pivot to a cross-link-heavy style going forward. Recorded here for visibility. Gates (no code changed; documentation only): cargo fmt / kernel-build / kernel-clippy / host-clippy clean; host-test 149 / 149 unchanged. Refs: PR #11 approval review (the conversation-driven punch-list); T-012 (Done 2026-04-28; merge commit `7b42bbe`); ADR-0021 (2026-04-28 Amendment unchanged); ADR-0022 (first rider Sub-rider closed, unchanged); CLAUDE.md §3 (English-in-repository rule applied to verdict prose). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This was referenced May 7, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Four commits since PR #8 merged. Closes B0's last remaining test-coverage and architecture-doc gaps and lands B1's EL drop.
50c6758761af95start_preludeextracted fromstartfor testability (semantically unchanged). Coverage report atdocs/analysis/reports/2026-04-27-coverage-rerun.md.c658c3dscheduler.md(~180 lines) +ipc.md(~190 lines);hal.mdTimer subsection expanded;overview.mdPhase-A status banner;architecture/README.mdindex updated. No code changes.f289d4dboot.sextended with K3-12 (DAIF mask) + EL2→EL1 transition per ADR-0024; newtyrne_hal::cpu::current_el()helper; UNSAFE-2026-0017 + 0018 audited;boot.mdandbsp-boot-checklist.mdupdated.Coverage delta (from R2 baseline)
kernel/src/sched/mod.rsregions: 83.93 % → 93.97 % (+9.81 pp)Both T-011 acceptance gates (sched ≥ 90 %, workspace ≥ 96 %) hit.
Status of in-scope tasks
Promotion to Done is gated on an independent approval-review pass (the pattern shipped 2026-04-27 — see T-009 mini-retro second follow-up note). Not blocking PR merge; the In Review state is the canonical "ready for second-pair-of-eyes" status.
What is not in this PR
Gates verification (locally, all four commits)
cargo fmt --all -- --checkclean.cargo host-clippyclean (-D warnings).cargo kernel-clippyclean.cargo host-test— 143 / 143 green (90 kernel + 19 hal + 34 test-hal).cargo +nightly miri test --workspace --exclude tyrne-bsp-qemu-virt— 143 / 143 clean.cargo kernel-build— clean (aarch64-unknown-none).cargo llvm-cov --workspace --exclude tyrne-bsp-qemu-virt --summary-only— see deltas above.CI (
.github/workflows/ci.yml, R6 skeleton) coversfmt + clippy + host-test + kernel-build + miri + coverageon push.Test plan
lint-and-host-test,kernel-build,miri.coveragejob reports figures matching the local re-run (informational;continue-on-errorso does not block).qemu-system-aarch64:tools/run-qemu.shboots; trace matches the A6 + T-009 instrumentation lines.-machine virtualization=on(EL2 entry): same trace; proves T-013's EL2→EL1 transition lands cleanly.cargo +nightly llvm-cov --workspace --exclude tyrne-bsp-qemu-virt --lcov --output-path docs/analysis/reports/lcov-2026-04-27.infoif the lcov artefact is wanted alongside the report.🤖 Generated with Claude Code
Summary by CodeRabbit
Documentation
Tests
Architecture