Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion CONTRIBUTING.md
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ Thank you for your interest. Tyrne is currently in the **architecture phase**

## What is not useful yet

- Pull requests against source code. There is no source code to extend or refactor meaningfully yet. Adding code before the architecture settles would force premature rewrites.
- Pull requests against source code outside the active milestone scope. The Rust workspace exists and the kernel boots end-to-end on QEMU virt (Phase A + B0/B1 closed), but each subsystem is being grown along the phased roadmap in [`docs/roadmap/`](docs/roadmap/); changes outside the current milestone's scope force premature rewrites and are usually not merged. Check [`docs/roadmap/current.md`](docs/roadmap/current.md) before opening a non-trivial PR.
- Feature requests for subsystems that have not yet been designed. File those as discussion issues if you want to influence the design, not as feature requests.

## When the project enters the implementation phase
Expand Down
10 changes: 9 additions & 1 deletion README.md
Original file line number Diff line number Diff line change
Expand Up @@ -40,11 +40,19 @@ Tiers describe the level of support committed to a target, not the quality of th

```
.
├── kernel/ # tyrne-kernel: capability tables, IPC, scheduler
├── hal/ # tyrne-hal: portable Console/Cpu/ContextSwitch/Mmu/Timer/IrqController traits
├── test-hal/ # tyrne-test-hal: in-tree fakes for the HAL traits (host tests only)
├── bsp-qemu-virt/ # tyrne-bsp-qemu-virt: QEMU virt aarch64 BSP (boot.s, vectors.s, GIC v2, PL011)
├── tools/ # run-qemu.sh and other developer-side helpers
├── docs/ # All project documentation
│ ├── architecture/ # System design, components, data flow
│ ├── decisions/ # Architecture Decision Records (ADRs)
│ ├── guides/ # How-to guides for contributors and porters
│ ├── standards/ # Coding, documentation, review standards
│ ├── audits/ # `unsafe`-block audit log
│ ├── analysis/ # Tasks, reviews, reports
│ ├── roadmap/ # Phase plans + current focus
│ └── glossary.md
├── CLAUDE.md # Entry point for Claude-based AI agents
├── AGENTS.md # Entry point for all AI agents
Expand All @@ -54,7 +62,7 @@ Tiers describe the level of support committed to a target, not the quality of th
└── NOTICE
```

Source code layout — the Rust workspace, HAL crates, userspace services — will be added after the architecture phase.
The Rust workspace contains four crates (`kernel`, `hal`, `test-hal`, `bsp-qemu-virt`) per [ADR-0006](docs/decisions/0006-workspace-layout.md). The kernel boots end-to-end on QEMU virt today (Phase A + B0/B1 closed); see [`docs/guides/two-task-demo.md`](docs/guides/two-task-demo.md) for the boot trace and [`docs/roadmap/current.md`](docs/roadmap/current.md) for active work.

## Where to start reading

Expand Down
2 changes: 1 addition & 1 deletion SECURITY.md
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ Tyrne is a security-oriented operating system project. Even while it is in pre-a

## Project status and guarantees

Tyrne is **pre-alpha**. There is no runnable kernel yet. No production use is supported, and no security guarantees are made for the current tree. The formal threat model is a work in progress and will be documented in `docs/architecture/security-model.md` (planned, Phase 2).
Tyrne is **pre-alpha**. The kernel boots end-to-end on QEMU virt aarch64 (Phase A + B0/B1 closed) and runs a two-task IPC demo through to completion, but it is not yet a userspace-bearing OS — no production use is supported, and no security guarantees are made for the current tree. The formal threat model is documented in [`docs/architecture/security-model.md`](docs/architecture/security-model.md) (Accepted) and refined as Phase B progresses; both the model and the codebase will continue to evolve until the project reaches a stable release.

## Reporting a security issue

Expand Down
8 changes: 4 additions & 4 deletions docs/architecture/hal.md
Original file line number Diff line number Diff line change
Expand Up @@ -47,7 +47,7 @@ flowchart TB
subgraph BSP["BSP (per-board, selected at build time)"]
BCpu["aarch64 Cpu impl"]
BMmu["VMSAv8 Mmu impl"]
BIrq["GICv3 / GIC-400 impl"]
BIrq["GICv2 / GIC-400 impl"]
BTimer["ARM generic timer impl"]
BConsole["PL011 / mini-UART impl"]
BIommu["SMMUv3 impl (bsp-qemu-virt)"]
Expand Down Expand Up @@ -123,9 +123,9 @@ On aarch64 the BSP reads the **virtual** counter family — `CNTVCT_EL0` for the

Helper conversions live in `tyrne_hal::timer` — `ticks_to_ns(count, frequency_hz)` uses 128-bit intermediate arithmetic and a saturating cast back to `u64` so monotonicity holds at the wrap edge; `resolution_ns_for_freq(frequency_hz)` returns the round-to-nearest period in nanoseconds, clamped to a floor of 1 ns to keep callers from dividing by zero on >2 GHz counters. Both functions are pure, host-testable, and sit at 100 % region coverage per the [2026-04-27 coverage rerun](../analysis/reports/2026-04-27-coverage-rerun.md).

The IRQ-armed half of the trait — `arm_deadline` / `cancel_deadline` — is `unimplemented!()` in QEMU virt's BSP today: it depends on the GIC + EL1 exception-vector-table install that [T-012](../analysis/tasks/phase-b/T-012-exception-and-irq-infrastructure.md) (B1) will land. The time-source half is fully wired and used by performance reviews and the boot-to-end timing instrumentation.
The IRQ-armed half of the trait — `arm_deadline` / `cancel_deadline` — is fully implemented in QEMU virt's BSP as of T-012 (Done 2026-04-28); the bodies write `CNTV_CVAL_EL0` / `CNTV_CTL_EL0` and route through `gic.enable(TIMER_IRQ)` / `gic.disable(TIMER_IRQ)`, audited under [UNSAFE-2026-0021](../audits/unsafe-log.md) (timer compare-register writes). [ADR-0010 §Revision notes 2026-04-28](../decisions/0010-timer-trait.md) records the closure: the time-source half landed with T-009 and the IRQ-delivery half with T-012, so both deferred halves of ADR-0010 are now live.

The kernel will use this trait for scheduler tick, deadline-based wakeups, and the `time_now` / `time_sleep_until` syscalls. In v1 the read side is exercised by the BSP's boot-to-end measurement; the IRQ side is dormant until T-012.
The kernel will use this trait for scheduler tick, deadline-based wakeups, and the `time_now` / `time_sleep_until` syscalls. In v1 the read side is exercised by the BSP's boot-to-end measurement; the IRQ-armed bodies are kernel-build clean but not exercised by the cooperative IPC demo (no caller arms a deadline). Their `Pending QEMU smoke verification` notation in [UNSAFE-2026-0021](../audits/unsafe-log.md) records this — the deadline-fire path lights up only when a future preemption-using task arrives.

#### `Console`

Expand Down Expand Up @@ -178,7 +178,7 @@ Runtime multi-board support (one kernel binary that detects its host and selects
| Architecture | aarch64 |
| CPU | generic ARMv8-A (whatever QEMU exposes for `-cpu max` / `-cpu cortex-a72`) |
| RAM base | `0x4000_0000` |
| Interrupt controller | GICv3 |
| Interrupt controller | GICv2 |
| Console | PL011 UART at `0x0900_0000` |
| Timer | ARM generic timer |
| IOMMU | SMMUv3 (optional, enabled with `-device smmuv3`; CI uses it) |
Expand Down
4 changes: 2 additions & 2 deletions docs/architecture/overview.md
Original file line number Diff line number Diff line change
Expand Up @@ -64,7 +64,7 @@ The kernel is **not** responsible for: drivers (every driver is a userspace task

The HAL is the trait boundary between the kernel's portable core and any one board's concrete hardware. It is not a driver layer; drivers live in userspace. It is the narrow interface the kernel needs to manipulate the CPU, the [MMU](../glossary.md), the interrupt controller, and a minimal boot-time console.

Expected HAL trait surface (final form documented in `hal.md`, planned):
HAL trait surface (final form documented in [`hal.md`](hal.md), Accepted):

- `Cpu` — disable / enable interrupts at the CPU level, halt / wait-for-interrupt, context-switch primitives.
- `Mmu` — translation-table layout, entry installation, TLB invalidation.
Expand All @@ -74,7 +74,7 @@ Expected HAL trait surface (final form documented in `hal.md`, planned):

A BSP is a crate that implements these traits for a specific target. Initial BSPs:

- `bsp-qemu-virt` — QEMU `virt` aarch64 (GICv3, PL011 UART, generic timer).
- `bsp-qemu-virt` — QEMU `virt` aarch64 (GICv2, PL011 UART, generic timer). The QEMU `virt` machine defaults to GICv2; `bsp-qemu-virt` ships a v2-only driver in [`gic.rs`](../../bsp-qemu-virt/src/gic.rs) per [ADR-0011](../decisions/0011-irq-controller-trait.md), audited under [UNSAFE-2026-0019](../audits/unsafe-log.md). GICv3 requires `-machine gic-version=3` and is out of scope for v1.
- `bsp-pi4` — Raspberry Pi 4 (BCM2711, legacy + GIC-400, mini-UART or PL011).

The kernel depends on HAL traits. It does not `use` a BSP directly; the BSP is selected at build time.
Expand Down
4 changes: 2 additions & 2 deletions docs/architecture/scheduler.md
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ Three Accepted ADRs jointly fix the scheduler's design:

- [ADR-0019: Scheduler shape](../decisions/0019-scheduler-shape.md) — cooperative single-core FIFO; ready queue is a fixed-capacity bounded `SchedQueue` indexed against a per-task arena. Capacity is `TASK_ARENA_CAPACITY` (currently 16).
- [ADR-0020: `ContextSwitch` trait and `Cpu` v2](../decisions/0020-cpu-trait-v2-context-switch.md) — register save/restore is a HAL primitive; the scheduler holds the per-task context array and never inspects its contents.
- [ADR-0022: Idle task and typed scheduler deadlock error](../decisions/0022-idle-task-and-typed-scheduler-deadlock.md) — the BSP registers an idle task at boot so the FIFO is never structurally empty; `SchedError::Deadlock` survives as a defensive return for preemption / SMP / a misconfigured BSP. ADR-0022's first rider clarifies that the idle task's body uses `core::hint::spin_loop` until [T-012](../analysis/tasks/phase-b/T-012-exception-and-irq-infrastructure.md) wires the timer IRQ.
- [ADR-0022: Idle task and typed scheduler deadlock error](../decisions/0022-idle-task-and-typed-scheduler-deadlock.md) — the BSP registers a single idle task at boot, and per [ADR-0026](../decisions/0026-idle-dispatch-fallback.md) it lives in a dedicated fallback slot consulted only when the ready queue is empty (`ready.dequeue().or(s.idle)`); idle is **not** a FIFO resident. `SchedError::Deadlock` survives as a defensive return when both halves of the dispatch chain resolve to `None` — preemption / SMP / a misconfigured BSP that forgot to call `register_idle`. The idle task's body uses `cpu.wait_for_interrupt()` followed by `yield_now`; the time-source half (T-009) and IRQ-delivery half (T-012) of ADR-0010 are both live, so WFI is the production form. The interim `core::hint::spin_loop()` shape ADR-0022's first rider introduced was retired by T-012 (Done 2026-04-28); see ADR-0022 §Revision notes 2026-04-28 for the closure of the first rider's *Sub-rider* under [UNSAFE-2026-0019](../audits/unsafe-log.md) / [UNSAFE-2026-0020](../audits/unsafe-log.md) / [UNSAFE-2026-0021](../audits/unsafe-log.md).

The IPC bridge from the scheduler into endpoint state is the subject of its own ADR — [ADR-0021: Raw-pointer scheduler IPC-bridge API](../decisions/0021-raw-pointer-scheduler-ipc-bridge.md). The bridge surface is summarised below; the *unsafe* discipline behind it lives in [`ipc.md`](ipc.md) (which crosses into IPC's territory) and the audit log.

Expand Down Expand Up @@ -70,7 +70,7 @@ stateDiagram-v2

### Idle task and structural non-emptiness

ADR-0022 mandates that the BSP register a single, lowest-priority idle task at boot. Its presence makes the FIFO ready queue structurally non-empty for the lifetime of the kernel. The idle task's body in v1 is `core::hint::spin_loop()` followed by `yield_now`, not `wait_for_interrupt`, because no IRQ source is configured before [T-012](../analysis/tasks/phase-b/T-012-exception-and-irq-infrastructure.md). When T-012 lands, the body switches to `cpu.wait_for_interrupt(); yield_now(...)` and the scheduler's behaviour is unchanged from the outside.
ADR-0022 mandates that the BSP register a single, lowest-priority idle task at boot. Per [ADR-0026](../decisions/0026-idle-dispatch-fallback.md) idle lives in a dedicated `Scheduler::idle: Option<TaskHandle>` fallback slot — **not** in the FIFO ready queue — and the dispatcher consults it only when the ready queue is empty (`ready.dequeue().or(s.idle)`). Idle therefore never displaces a real Ready task; it runs only when no other Ready task exists. The idle task's body is `cpu.wait_for_interrupt()` followed by `yield_now` — the production form ADR-0022's *Decision outcome* originally specified. T-012 (Done 2026-04-28) closed ADR-0022's first rider's *Sub-rider* by landing both halves of the wake-source precondition (T-009's `CNTVCT_EL0` time source and T-012's GIC v2 + `VBAR_EL1` IRQ delivery), so WFI is now safe to issue under v1; the interim `core::hint::spin_loop()` shape the first rider introduced is retired. Audit citations: [UNSAFE-2026-0019](../audits/unsafe-log.md) (GIC MMIO), [UNSAFE-2026-0020](../audits/unsafe-log.md) (vector table), [UNSAFE-2026-0021](../audits/unsafe-log.md) (timer compare-register writes). See [`docs/architecture/exceptions.md` §"Idle's `wfi` activation"](exceptions.md) for the cross-cutting picture.

Because idle is always `Ready`, every `yield_now` that would otherwise see an empty queue instead dispatches idle. This collapses the previous "panic on empty ready queue inside yield_now" path into normal scheduling — yield never panics in production. The empty-queue panic survives only inside `start` (where the kernel programmer must register at least one task before booting; structurally required by ADR-0022's idle-at-boot rule).

Expand Down
2 changes: 1 addition & 1 deletion docs/architecture/security-model.md
Original file line number Diff line number Diff line change
Expand Up @@ -327,7 +327,7 @@ Each of these is a future ADR.
- **IOMMU / SMMU policy per target.** Raspberry Pi 4 has no SMMU — do we accept implicit trust of all enabled bus masters, refuse to enable DMA-capable devices and force PIO, or gate DMA-capable devices behind a deployment-time opt-in? QEMU `virt` has SMMUv3 and should be the CI gate that catches driver regressions against IOMMU expectations. Jetson Orin has an SMMU and adopts the same model when its port lands. ADR required before the first driver that enables bus-master DMA.
- **Concrete bounds** for the quotas under *Bounded kernel resources*: numeric defaults for each, per-target tuning policy, and how upgrades change them without invalidating running systems.
- **Cross-table capability derivation tree (CDT).** Whether IPC-transferred capabilities should retain a parent-child link to the sender's entry so that the sender can revoke the copy post-transfer, and — if so — how per-task-table CDT storage scales. seL4's answer is a whole-system CDT; Phase B needs to decide before the first multi-task system uses transfer as a revoke-retained grant. See the v1 qualification on *Revocation is transitive* above.
- **Early IRQ masking in BSP reset vectors.** v1's `boot.s` on QEMU `virt` does not explicitly `msr daifset, #0xf` before stack / BSS setup the reset state happens to leave interrupts effectively masked (no IRQ source is configured and the GIC is untouched), but this is a per-platform accident rather than a guarantee. Future BSPs should adopt "mask DAIF first, everything else after" as a standard reset-vector prologue; add the instruction to the [BSP boot checklist](../standards/bsp-boot-checklist.md) and audit the existing checklist at that time.
- **Early IRQ masking in BSP reset vectors.** ✅ **Closed by [T-013](../analysis/tasks/phase-b/T-013-el-drop-to-el1.md) (Done 2026-04-27, ADR-0024, [UNSAFE-2026-0017](../audits/unsafe-log.md)).** The `_start` symbol in [`bsp-qemu-virt/src/boot.s`](../../bsp-qemu-virt/src/boot.s) now begins with `msr daifset, #0xf` as the **literal first instruction** before stack/BSS setup, and the [BSP boot checklist §1a](../standards/bsp-boot-checklist.md) records "mask DAIF first" as a standard reset-vector prologue every future BSP must observe. The previous "per-platform accident" framing is retired; DAIF masking is now a structural property of every Tyrne reset vector, with the audit trail captured under UNSAFE-2026-0017's first Amendment block. Future BSPs (`bsp-pi4`, etc.) inherit the rule via the boot checklist.

## References

Expand Down
1 change: 1 addition & 0 deletions docs/decisions/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -51,6 +51,7 @@ Each ADR contains:
| 0020 | [`ContextSwitch` trait and `Cpu` v2](0020-cpu-trait-v2-context-switch.md) | Accepted | 2026-04-21 |
| 0021 | [Raw-pointer scheduler IPC-bridge API](0021-raw-pointer-scheduler-ipc-bridge.md) | Accepted | 2026-04-22 |
| 0022 | [Idle task and typed scheduler deadlock error](0022-idle-task-and-typed-scheduler-deadlock.md) | Superseded by 0026 (idle-task-location axis only; typed-error axis stands) | 2026-04-22 |
| 0023 | Cross-table capability revocation policy *(no file at HEAD — accept-deferred per Phase B0 closure; tracked in [`phase-b.md`](../roadmap/phases/phase-b.md) ADR ledger)* | Deferred | 2026-04-27 |
| 0024 | [EL drop to EL1 policy](0024-el-drop-policy.md) | Accepted | 2026-04-27 |
| 0025 | [ADR governance amendments: forward-reference contract, rider hygiene](0025-adr-governance-amendments.md) | Accepted | 2026-04-27 |
| 0026 | [Idle dispatch via separate fallback slot](0026-idle-dispatch-fallback.md) | Accepted | 2026-05-06 |
Expand Down
10 changes: 10 additions & 0 deletions docs/decisions/template.md
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,16 @@
- **Date:** YYYY-MM-DD
- **Deciders:** @cemililik

<!--
Status enum (use one):
- Proposed — drafted, awaiting Accept after careful re-read.
- Accepted — settled; the project follows this decision.
- Deferred — recognised as needed but explicitly postponed; no file body required if filed-but-deferred (see ADR-0018, ADR-0023).
- Deprecated — historical; followed for a time but no longer.
- Superseded by NNNN — overridden by a later ADR; old body preserved for the historical record (per supersede-adr skill).
-->


## Context

<What is the situation, the problem, or the question? What constraints apply? What are the stakes of getting this wrong?>
Expand Down
2 changes: 1 addition & 1 deletion docs/glossary.md
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@ Terminology used throughout Tyrne. Entries are alphabetical. If a term appears i

**Capability transfer.** The IPC operation in which a sender's `ipc_send` atomically removes a capability from its own table, embeds it in the message, and delivers it into the receiver's table on `ipc_recv`. If either half fails, neither table is left in an intermediate state. See [ADR-0017](decisions/0017-ipc-primitive-set.md).

**CDT (Capability Derivation Tree).** The parent/child tree of capabilities derived from one another via `cap_derive`. Revocation is transitive along this tree: revoking a parent revokes every descendant. In v1 the tree is per-table; cross-table transitivity is deferred (see [ADR-0023](decisions/0023-cross-table-capability-revocation-policy.md) when opened).
**CDT (Capability Derivation Tree).** The parent/child tree of capabilities derived from one another via `cap_derive`. Revocation is transitive along this tree: revoking a parent revokes every descendant. In v1 the tree is per-table; cross-table transitivity is deferred see ADR-0023 (accept-deferred per Phase B0 closure; no file at HEAD, tracked in [`phase-b.md`](roadmap/phases/phase-b.md) ADR ledger and the [B0 closure security review](analysis/reviews/security-reviews/2026-04-27-B0-closure.md)).

**`CNTFRQ_EL0`.** ARM aarch64 system register that reports the Generic Timer's counter frequency in Hz. Set by firmware before kernel entry; read at EL0/EL1 (subject to `CNTHCTL_EL2.EL1PCTEN` only in VHE mode, which Tyrne does not use). QEMU virt sets it to 62.5 MHz. On real Pi 4 / BCM2711 the rate is firmware-dependent (mainline Linux configures 54 MHz; older Pi-class boards used 19.2 MHz) — BSPs read the firmware-provided value rather than hard-coding. Tyrne reads `CNTFRQ_EL0` once at `QemuVirtCpu::new` and caches the derived `resolution_ns`.

Expand Down
Loading
Loading