KRN-OBJ requirements¶
Destroying an object with waiters is a kernel fault in checked builds unless the object was created with Rationale: ADR-020: lifecycle bugs are caught; deliberate teardown is explicit. Status: Accepted 2026-10-07 Verification: Test: Trace: SPEC-009 §6; SPEC-004 §6.7; ADR-020 |
After destruction, the object’s generation shall be bumped so stale capabilities fail validation in profiles that check them. Rationale: Use-after-destroy becomes Status: Accepted 2026-10-07 Verification: Test: Trace: SPEC-009 §3.2, §3.3, §6 |
Object storage ownership belongs to whoever provided it; the kernel never frees caller storage. Rationale: No allocator in the kernel path. Status: Accepted 2026-10-07 Verification: Analysis: no free call in Trace: SPEC-009 §5, §6 |
Rationale: uC/OS-III’s safety-critical start; a frozen object set is what a certification argument wants. Status: Accepted 2026-10-07 Verification: Test: Trace: SPEC-009 §6 |
Thread and partition handles shall carry a generation in every profile that checks generations; a wait on a handle whose generation changed because of a restart shall complete with Rationale: ADR-032: restarts are visible to peers. Status: Accepted 2026-10-07 Verification: Isolated-profile test Trace: SPEC-009 §6; ADR-032 |
Every object shall begin with the header of SPEC-009 §2 ( Rationale: One place for validation, registry, binding, and naming; zero cost where not used. Status: Accepted 2026-10-07 Verification: Analysis: Trace: SPEC-009 §2 |
Objects shall move Rationale: Double init and destroy races have defined outcomes. Status: Accepted 2026-10-07 Verification: Test: Trace: SPEC-009 §6 |
Rationale: ADR-006 without mirrored structs or exposed layouts. Status: Accepted 2026-10-07 Verification: Build test: a deliberately stale header fails to build; Analysis: generator review. Trace: SPEC-009 §5.1; ADR-006; BLD-007 |
Rationale: Static objects without hand-written init code, on AVR too (09 §7). Status: Accepted 2026-10-07 Verification: Test: init-table construction during Trace: SPEC-009 §5.2; SPEC-001 §6.4 |
Destroy shall be refused with Rationale: The kernel never leaves a dangling owner. Status: Accepted 2026-10-07 Verification: Test: Trace: SPEC-009 §6, §8 |
With Rationale: Debuggers and statistics enumerate objects without symbols (ADR-011). Status: Accepted 2026-10-07 Verification: Test: debug descriptor consumer lists every object of the conformance run. Trace: SPEC-009 §7; OBS-008 |
Kernel objects shall live in RAM and be constructed at boot; no const-initializer form of an object shall be part of the public API in 1.0. Rationale: A const form would expose the layout the storage type hides. Status: Accepted 2026-10-07 Verification: Analysis: header review. Trace: SPEC-009 §5.3, §12.5 |
Object init and destroy (with the number of waiters flushed), capability changes, and system freeze shall be trace events. Rationale: Lifecycle debugging. Status: Accepted 2026-10-07 Verification: Test: trace decoder. Trace: SPEC-009 §9; OBS-005 |