From 19755ee27a3d24f797336e6e602e2df2f6f75235 Mon Sep 17 00:00:00 2001 From: timohueser Date: Mon, 24 Aug 2026 12:48:11 +0200 Subject: [PATCH 1/4] One CoreMode owns "what may run now"; delete the freeze and link gates MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Before this, four independent things answered "is a route search live?": a `RerouteFreeze` in its own module, a `TransferGate` search flag, the arena's owner, and the board's own `nav_run` handle. They could disagree, and one of them — `link_gate.rs` — had been almost entirely dead since the flat engine took over one-transfer-at-a-time. `CoreMode` (`device_core/core_mode.rs`) holds four levels and nothing else: one search level per plan family (the arm is one block, so a detour's terminal edge must never release a route search's freeze), one transfer level, and the banner's level-to-edge bit. Navigator writes the search levels at the three transitions it already owned; `App::set_map_transfer` and the pass's fact stage write the transfer level. Everything else derives: - the Recalculating freeze and its repaint edge are views over the levels; - `MapQuiesced` and `TransferReady` lose their public two-argument `prove` constructors — `CoreMode` is the only mint, plus one named `recovery_boot()` escape for the card-recovery USB boot path, where no ride loop, renderer or planner exists; - stage 12 reads `CoreMode::admits_heavy()`, so `plan_route`, `plan_detour` and `dfu.install` now withdraw for a live search as well as a live transfer — which is what `DeviceFacts::heavy_operations` already documented; - the board's `nav_take_arena` names the arena's actual holder in its refusal, so a plan offered during a cable transfer is told about the cable rather than about "the scratch arena". `reroute_freeze.rs` and `link_gate.rs` are gone; `PlanFamily` moves to `navigator.rs` and the banner drawing to `screen/vocab/chrome.rs`, where the vocabulary guard now has a landmark for it. The union of both modules' surviving tests lands on `CoreMode`, plus the cancel-window divergence between `live_family()` and the search level that nothing pinned before. Production Rust -87 lines; the banner frame and the 270-frame manifest are byte-identical, `size_of::()` is flat at 50,928 B and board resident is unchanged. `tools/s5_core_mode_soak.py` drives the three on-glass soaks the issue names. It is scaffolding: delete it, and its test, when #1487 closes with A, B and C recorded. Co-Authored-By: Claude Fable 5 --- firmware/obc-app/src/app.rs | 76 ++-- firmware/obc-app/src/arena_gate.rs | 88 ++-- firmware/obc-app/src/device_core/core_mode.rs | 363 +++++++++++++++ firmware/obc-app/src/device_core/mod.rs | 4 + firmware/obc-app/src/device_core/pass.rs | 45 +- firmware/obc-app/src/device_core/shared.rs | 17 +- firmware/obc-app/src/lib.rs | 3 - firmware/obc-app/src/link_gate.rs | 268 ----------- firmware/obc-app/src/navigator.rs | 251 ++++++---- firmware/obc-app/src/reroute_freeze.rs | 297 ------------ firmware/obc-app/src/screen/detour.rs | 10 +- firmware/obc-app/src/screen/vocab/chrome.rs | 81 +++- firmware/obc-app/tests/detour_flow.rs | 37 +- firmware/obc-fw-nrf54l/src/link/mod.rs | 18 - firmware/obc-fw-nrf54l/src/main.rs | 2 +- firmware/obc-fw-nrf54l/src/ride.rs | 41 +- tools/check_screen_vocabulary.py | 1 + tools/s5_core_mode_soak.py | 428 ++++++++++++++++++ tools/tests/test_s5_core_mode_soak.py | 82 ++++ 19 files changed, 1303 insertions(+), 809 deletions(-) create mode 100644 firmware/obc-app/src/device_core/core_mode.rs delete mode 100644 firmware/obc-app/src/link_gate.rs delete mode 100644 firmware/obc-app/src/reroute_freeze.rs create mode 100644 tools/s5_core_mode_soak.py create mode 100644 tools/tests/test_s5_core_mode_soak.py diff --git a/firmware/obc-app/src/app.rs b/firmware/obc-app/src/app.rs index 7054f7dc1..13bcc9648 100644 --- a/firmware/obc-app/src/app.rs +++ b/firmware/obc-app/src/app.rs @@ -11,14 +11,15 @@ use crate::activity::{Activity, Mode}; use crate::card_scheduler::{BootUpdate, DfuLanding, PendingUpload, UploadEvent}; use crate::catalog_state::CatalogState; use crate::device_core::compat::{dfu_row, navigator_row, settings_row, storage_info_row}; +use crate::device_core::core_mode::{CoreMode, ModeState}; use crate::device_core::storage_info::StorageInfo; use crate::dfu::DfuState; use crate::dirty::Dirty; use crate::host::{DrainStatus, HostCommand, HostCommandClass, HostEvent, HostMailbox, HOST_COMMAND_CLASSES}; use crate::input::Gesture; +use crate::navigator::PlanFamily; use crate::navigator::{NavigatorIntent, NavigatorMachine, PlanPhase}; use crate::placement::define_placement_constructors; -use crate::reroute_freeze::PlanFamily; use crate::ride::RideSummary; use crate::ride_engine::RideEngine; use crate::route::RouteSummary; @@ -563,9 +564,15 @@ pub struct App { /// commits between drains is never coalesced into a single missed rescan. store_changed: u32, /// The **Navigator** domain (#1397 S2): the rider's undelivered plan requests, the per-family - /// phase, the operation token every planner answer must carry back, and the Recalculating - /// freeze those transitions drive. The only writer of any of them. + /// phase, and the operation token every planner answer must carry back. The only writer of any + /// of them, and of [`mode`](App::mode)'s two search levels. pub(crate) navigator: NavigatorMachine, + /// **`CoreMode`** (#1397 S5): the one owner of "what heavy work may run now, and what the rider + /// is looking at" — the two search levels Navigator writes, the transfer level + /// [`set_map_transfer`](App::set_map_transfer) writes, and the Recalculating banner's + /// level→edge bit. Every reader of "a search is live" derives from it; nothing keeps a second + /// copy. + pub(crate) mode: CoreMode, /// The **settings-persistence** machine (#810, #1397 S2): the dirty revision, the subtree /// debounce, the retry backoff and the stale-answer rule. pub(crate) settings_ops: crate::settings::SettingsMachine, @@ -644,6 +651,7 @@ impl App { weather: crate::weather::WeatherDomain::new(), store_changed: 0, navigator: NavigatorMachine::new(), + mode: CoreMode::new(), settings_ops: crate::settings::SettingsMachine::new(), dfu: DfuState::new(), storage: StorageInfo::new(), @@ -690,6 +698,7 @@ impl App { weather, store_changed, navigator, + mode, settings_ops, dfu, storage, @@ -723,6 +732,7 @@ impl App { assert_eq!(*store_changed, 0, "no store commit pending"); assert!(settings_ops.is_empty(), "settings Clean at revision 0"); navigator.assert_boot_state(); + assert_eq!(*mode, CoreMode::new(), "nothing searching, nothing streaming, no banner shown"); dfu.assert_boot_state(); storage.assert_boot_state(); assert_eq!(*pass, crate::device_core::pass::PassState::new(), "no connection wired, no pass in flight"); @@ -774,7 +784,7 @@ impl App { self.activity.note_sensor_clock(now_ms); // Read the freeze once, before anything below can move the stack: while a planner run holds // the arena over a map base, this tick must not advance route-match progress (see the fix - // path below for why, and `crate::reroute_freeze` for the whole rule). + // path below for why, and `device_core::core_mode` for the whole rule). let frozen = self.reroute_freeze_active(); // The once-per-load route/session sync — matcher re-lock, session restart (accumulators + // breadcrumb), the route-length mirror, and the climbs/waypoints cache builds — is the @@ -1194,16 +1204,17 @@ impl App { /// [`nav_arena_precondition`](App::nav_arena_precondition) hands to /// [`ArenaGate::claim_nav`](crate::arena_gate::ArenaGate::claim_nav). pub fn reroute_freeze_active(&self) -> bool { - self.navigator.freeze_active(self.ui.base_draws_map()) + self.mode.frozen(self.ui.base_draws_map()) } - /// Whether a host planner run is live at all — including a **menu** plan, where no freeze is - /// engaged because the planning screen is itself the (chrome) base. The "is the arena's nav arm - /// claimed?" fact; hosts that arbitrate a search against something else (the cable transfer - /// gate's search arm, [`TransferGate::begin_search`](crate::TransferGate::begin_search)) read - /// this rather than the freeze. - pub fn plan_in_flight(&self) -> bool { - self.navigator.plan_live() + /// What the device is busy with, ranked and payload-free — [`CoreMode`]'s one public read. + /// (Named apart from [`mode`](App::mode), which is the rider's *activity* — Idle or Riding.) + /// + /// A search outranks a transfer because it is the one the rider is waiting on and the one with + /// a banner. Admission never reads this: it reads the levels, so the ranking cannot hide one + /// behind the other. + pub fn core_mode(&self) -> ModeState { + self.mode.state() } /// The proof that the map plane is quiesced, minted from this app's own state — `None` when a @@ -1211,7 +1222,14 @@ impl App { /// `claim_nav` call site is `app.nav_arena_precondition().ok_or(…)?`, so the gate cannot be /// called without the evidence. pub fn nav_arena_precondition(&self) -> Option { - crate::arena_gate::MapQuiesced::prove(self.reroute_freeze_active(), self.base_draws_map()) + self.mode.nav_precondition(self.base_draws_map()) + } + + /// The proof that a cable upload may take the arena's staging arm: the transfer card is up + /// (`render ⊥ usb`) and no search holds the nav arm (`nav ⊥ usb`). The board's `claim_usb` call + /// site reads this rather than assembling the two facts itself. + pub fn usb_stage_precondition(&self) -> Option { + self.mode.usb_precondition(self.map_transfer_card_up()) } /// Whether the frame needs the streamed-map [`Reader`] built and passed to @@ -1612,7 +1630,7 @@ impl App { /// No production path reaches it. Stands in for a [`Route`](PlanFamily::Route) run, so a stray /// detour edge cannot release it (see [`PlanFamily`]). pub fn debug_set_plan_live(&mut self, live: bool) { - if self.navigator.debug_set_plan_live(live) { + if self.navigator.debug_set_plan_live(live, &mut self.mode) { self.ui.map_dirty = true; } } @@ -1830,7 +1848,7 @@ impl App { if !self.navigator.take_cancel(family) { return false; } - if self.navigator.note_cancel_delivered(family) { + if self.navigator.note_cancel_delivered(family, &mut self.mode) { self.ui.map_dirty = true; } true @@ -1906,7 +1924,7 @@ impl App { /// [`take_dirty`](App::take_dirty) level edge that put it up. Idempotent: several release edges /// can land for one run. fn end_plan(&mut self, family: PlanFamily, phase: PlanPhase) { - if self.navigator.note_answer(family, phase) { + if self.navigator.note_answer(family, phase, &mut self.mode) { self.ui.map_dirty = true; } } @@ -2151,6 +2169,10 @@ impl App { /// ([`MapTransfer::Installed`](crate::screen::MapTransfer::Installed) / /// [`Failed`](crate::screen::MapTransfer::Failed)) stay up to be dismissed. pub fn set_map_transfer(&mut self, state: Option) { + // The one place a streaming map upload becomes `CoreMode`'s transfer level. A terminal card + // (Installed / Failed) is a *report*, not a stream: the store is free again the moment the + // bytes stopped, so heavy work is re-admitted while the rider is still reading the card. + self.mode.note_transfer(state.is_some_and(|s| s.is_receiving())); self.ui.cards.set_map_transfer(state); self.sweep_cards(); } @@ -3228,7 +3250,7 @@ impl App { // a hold charging during a search still bulges over it. if self.reroute_freeze_active() { let text = crate::i18n::t(crate::Msg::MapRecalculating, self.settings.language); - crate::reroute_freeze::draw_banner(target, &color_fn, w, h, text); + crate::screen::vocab::chrome::recalculating_banner(target, &color_fn, w, h, text); } } @@ -3237,7 +3259,7 @@ impl App { /// for a partial-overlay host (the board re-presents overlay *rows*, not whole frames). A host /// that pushes the union of this and the bulge's rows presents exactly what changed. pub fn reroute_banner_rows(&self, h: f32) -> Option<(u16, u16)> { - self.reroute_freeze_active().then(|| crate::reroute_freeze::banner_rows(h)) + self.reroute_freeze_active().then(|| crate::screen::vocab::chrome::recalculating_banner_rows(h)) } /// Whether the overlay plane has live content this frame — a hold bulge charging, popping, or @@ -3266,9 +3288,9 @@ impl App { /// the plan seams on purpose: the freeze is a *level* (a live plan **and** a map base), and /// either half can move without the other. Deriving its repaint edge at the drain is what makes /// the banner appear on the pass a map base lands back under a search that is still running — - /// see [`RerouteFreeze::take_engaged_edge`](crate::reroute_freeze::RerouteFreeze::take_engaged_edge). + /// see [`CoreMode::take_engaged_edge`](crate::device_core::core_mode::CoreMode::take_engaged_edge). pub fn take_dirty(&mut self) -> Dirty { - if self.navigator.take_freeze_edge(self.ui.base_draws_map()) { + if self.mode.take_engaged_edge(self.ui.base_draws_map()) { self.ui.overlay_edge = true; } self.ui.take_dirty() @@ -3497,12 +3519,14 @@ impl App { // The three planner commands are Navigator's own effects, spelled in the old // vocabulary: the domain decides that work is owed and engages the freeze as it hands // the operation over, and `navigator_row` names the command each effect becomes. - HostCommandClass::PlanRoute => { - self.navigator.next_plan_effect(PlanFamily::Route).and_then(|e| navigator_row(e).command()) - } - HostCommandClass::PlanDetour => { - self.navigator.next_plan_effect(PlanFamily::Detour).and_then(|e| navigator_row(e).command()) - } + HostCommandClass::PlanRoute => self + .navigator + .next_plan_effect(PlanFamily::Route, &mut self.mode) + .and_then(|e| navigator_row(e).command()), + HostCommandClass::PlanDetour => self + .navigator + .next_plan_effect(PlanFamily::Detour, &mut self.mode) + .and_then(|e| navigator_row(e).command()), HostCommandClass::CommitDetour => { self.navigator.next_commit_effect().and_then(|e| navigator_row(e).command()) } diff --git a/firmware/obc-app/src/arena_gate.rs b/firmware/obc-app/src/arena_gate.rs index f2b3a0bc9..008364d4f 100644 --- a/firmware/obc-app/src/arena_gate.rs +++ b/firmware/obc-app/src/arena_gate.rs @@ -3,10 +3,9 @@ //! The board time-shares **one** RAM block between three arms that are never live together — the //! per-frame render scratch, the nav block (`NavScratch` + `NavTileCache` + `NavPlanner`), and the //! USB staging buffer. The union itself is device-only (`obc-fw-nrf54l`'s `arena.rs`, the one place -//! `unsafe` lives); *who may hold it, and when* is plain bookkeeping, and it lives here for the same -//! reason [`crate::link_gate`] does: the board crate has no `test` harness in CI, and "a claim while -//! a search is running must be refused" is exactly the kind of statement that should be asserted -//! rather than reviewed. +//! `unsafe` lives); *who may hold it, and when* is plain bookkeeping, and it lives here because the +//! board crate has no `test` harness in CI, and "a claim while a search is running must be refused" +//! is exactly the kind of statement that should be asserted rather than reviewed. //! //! # The arms are disjoint because the product says so //! @@ -20,17 +19,18 @@ //! | nav ⊥ usb | no route search while the cable owns upload scratch | [`TransferReady`] | //! //! A gate that is merely *documented* is a gate that gets skipped, so each precondition is a token -//! only its `prove` constructor can mint: [`claim_nav`](ArenaGate::claim_nav) cannot even be -//! *called* without evidence that the map plane is quiesced. +//! only [`CoreMode`](crate::device_core::core_mode::CoreMode) can mint: +//! [`claim_nav`](ArenaGate::claim_nav) cannot even be *called* without evidence that the map plane +//! is quiesced, and there is exactly one place that decides the token is owed. //! //! # No atomics //! //! [`ArenaGate`] takes `&mut self` because the **ride loop is the sole owner-switcher** — the USB -//! plane never claims directly, it requests through the [`TransferGate`](crate::TransferGate) and -//! the loop grants between frames (the #677 async-frame discipline: guards are `!Send` and never -//! held across an `.await` where another claimant could run). If a second switcher ever appears, -//! this becomes an `AtomicU8` compare-exchange like the transfer gate — and the `&mut` is what -//! makes that a *compile* error to skip rather than a race to debug. +//! plane never claims directly, it raises a request the loop grants between frames (the #677 +//! async-frame discipline: guards are `!Send` and never held across an `.await` where another +//! claimant could run). If a second switcher ever appears, this becomes an `AtomicU8` +//! compare-exchange — and the `&mut` is what makes that a *compile* error to skip rather than a +//! race to debug. //! //! # The bug class this creates //! @@ -61,9 +61,8 @@ pub enum ArenaError { /// refused by a live search is normal and expected; one refused by a transfer is a UI bug). Busy(ArenaOwner), /// A release naming an arm that does not hold the arena. Carries the actual owner. Never a - /// silent no-op — unlike [`TransferGate::release`](crate::TransferGate::release), where two - /// wires legitimately tear down independently, there is exactly one owner-switcher here, so a - /// mismatched release means the caller lost track of its own guard. + /// silent no-op: there is exactly one owner-switcher here, so a mismatched release means the + /// caller lost track of its own guard. NotHeld(ArenaOwner), } @@ -73,27 +72,38 @@ pub enum ArenaError { /// Two ways to be quiesced, and the second is why this is a token rather than a bool: menu planning /// happens on a chrome base (`NavPlanning` is opaque, so there is no map underneath to freeze), and /// a mid-ride detour plan happens over a **map** base — the Recalculating freeze is what makes the -/// second case as safe as the first. See [`App::reroute_freeze_active`](crate::App::reroute_freeze_active). +/// second case as safe as the first. Both are decided in one place, +/// [`CoreMode::nav_precondition`](crate::device_core::core_mode::CoreMode). #[derive(Debug, Clone, Copy)] pub struct MapQuiesced(()); impl MapQuiesced { - /// Mint the proof from the two facts the app reports each pass, or `None` when the map plane - /// would still draw. Compose it straight off the app with + /// The mint, crate-private so [`CoreMode`](crate::device_core::core_mode::CoreMode) is the only + /// thing that decides *when*. Reach it from outside through /// [`App::nav_arena_precondition`](crate::App::nav_arena_precondition). - pub fn prove(freeze_active: bool, base_draws_map: bool) -> Option { - (freeze_active || !base_draws_map).then_some(MapQuiesced(())) + pub(crate) const fn mint() -> MapQuiesced { + MapQuiesced(()) } } -/// Proof that a cable upload may take the arena: its transfer screen is up and no route search is -/// live. Both facts come from the ride loop, the arena's sole owner-switcher. +/// Proof that a cable upload may take the arena: its transfer screen is up (`render ⊥ usb`) and no +/// route search holds the nav arm (`nav ⊥ usb`). #[derive(Debug, Clone, Copy)] pub struct TransferReady(()); impl TransferReady { - pub fn prove(transfer_screen_up: bool, search_live: bool) -> Option { - (transfer_screen_up && !search_live).then_some(Self(())) + /// The mint, crate-private for the same reason [`MapQuiesced::mint`] is. Reach it through + /// [`App::usb_stage_precondition`](crate::App::usb_stage_precondition). + pub(crate) const fn mint() -> TransferReady { + TransferReady(()) + } + + /// The one named escape: the card-recovery USB boot path, where **no ride loop, no renderer and + /// no planner exist**. There is no `App` to ask, and nothing that could draw a map or start a + /// search — the two facts the mint would check are true by the absence of the code that could + /// falsify them. + pub const fn recovery_boot() -> TransferReady { + TransferReady(()) } } @@ -219,19 +229,6 @@ impl ArenaGate { mod tests { use super::*; - /// The proof tokens are the gate. Minting them is the *only* way to call the guarded claims, so - /// pin exactly which facts mint one. - #[test] - fn the_nav_precondition_is_a_quiet_map_plane_however_it_got_quiet() { - assert!(MapQuiesced::prove(false, false).is_some(), "menu planning: chrome base, no map to freeze"); - assert!(MapQuiesced::prove(true, true).is_some(), "mid-ride detour: map base, freeze engaged"); - assert!(MapQuiesced::prove(true, false).is_some(), "belt and braces"); - assert!( - MapQuiesced::prove(false, true).is_none(), - "a map base with no freeze is the regression: the search would eat the scratch the next frame renders from" - ); - } - #[test] fn a_fresh_gate_is_idle_and_a_render_may_take_it() { let mut gate = ArenaGate::new(); @@ -252,7 +249,7 @@ mod tests { #[test] fn a_live_search_refuses_every_render_claim_until_it_finishes() { let mut gate = ArenaGate::new(); - let proof = MapQuiesced::prove(true, true).expect("the freeze is engaged"); + let proof = MapQuiesced::mint(); assert_eq!(gate.claim_nav(proof), Ok(())); for _ in 0..3 { @@ -266,13 +263,11 @@ mod tests { #[test] fn usb_stage_requires_a_visible_transfer_and_excludes_render_and_nav() { - assert!(TransferReady::prove(false, false).is_none()); - assert!(TransferReady::prove(true, true).is_none()); - let ready = TransferReady::prove(true, false).expect("visible transfer, no search"); + let ready = TransferReady::mint(); let mut gate = ArenaGate::new(); assert_eq!(gate.claim_usb(ready), Ok(())); assert_eq!(gate.claim_render(), Err(ArenaError::Busy(ArenaOwner::Usb))); - let quiet = MapQuiesced::prove(true, true).unwrap(); + let quiet = MapQuiesced::mint(); assert_eq!(gate.claim_nav(quiet), Err(ArenaError::Busy(ArenaOwner::Usb))); assert_eq!(gate.release(ArenaOwner::Usb), Ok(())); } @@ -284,7 +279,7 @@ mod tests { let mut gate = ArenaGate::new(); assert_eq!(gate.claim_render(), Ok(ArenaInit::Required)); - let quiesced = MapQuiesced::prove(true, true).unwrap(); + let quiesced = MapQuiesced::mint(); assert_eq!(gate.claim_nav(quiesced), Err(ArenaError::Busy(ArenaOwner::Render))); } @@ -300,12 +295,11 @@ mod tests { /// **The regression** a wrong release would cause: the render frame ends, drops its guard, and /// (with a mismatched arm) hands the arena to nobody while the search still reads it. Loud - /// rather than silent — this is the mirror of `link_gate`'s no-op release, and it differs on - /// purpose: there, two wires tear down independently; here there is one owner-switcher. + /// rather than silent: there is one owner-switcher, so there is no benign mismatched release. #[test] fn releasing_an_arm_that_does_not_hold_the_arena_is_an_error() { let mut gate = ArenaGate::new(); - let proof = MapQuiesced::prove(false, false).unwrap(); + let proof = MapQuiesced::mint(); assert_eq!(gate.claim_nav(proof), Ok(())); assert_eq!(gate.release(ArenaOwner::Render), Err(ArenaError::NotHeld(ArenaOwner::Nav))); @@ -345,7 +339,7 @@ mod tests { // foreign owner while the USB staging arm existed; with two arms the loop is the nav case // written awkwardly, so it is written plainly. If a third arm is ever added, this becomes a // loop again — and the const assert in `arena.rs` is what will say so first. - assert_eq!(gate.claim_nav(MapQuiesced::prove(false, false).unwrap()), Ok(())); + assert_eq!(gate.claim_nav(MapQuiesced::mint()), Ok(())); assert_eq!(gate.release(ArenaOwner::Nav), Ok(())); assert_eq!(gate.claim_render(), Ok(ArenaInit::Required), "the nav arm left its own bytes behind"); assert_eq!(gate.release(ArenaOwner::Render), Ok(())); @@ -361,7 +355,7 @@ mod tests { assert_eq!(gate.claim_render(), Ok(init)); assert_eq!(gate.release(ArenaOwner::Render), Ok(())); } - assert_eq!(gate.claim_nav(MapQuiesced::prove(true, true).unwrap()), Ok(())); + assert_eq!(gate.claim_nav(MapQuiesced::mint()), Ok(())); assert_eq!(gate.release(ArenaOwner::Nav), Ok(())); assert_eq!(gate.claim_render(), Ok(ArenaInit::Required), "the search left its A* table in the block"); assert_eq!(gate.release(ArenaOwner::Render), Ok(())); diff --git a/firmware/obc-app/src/device_core/core_mode.rs b/firmware/obc-app/src/device_core/core_mode.rs new file mode 100644 index 000000000..f19f5a447 --- /dev/null +++ b/firmware/obc-app/src/device_core/core_mode.rs @@ -0,0 +1,363 @@ +//! **`CoreMode`** — the one owner of *what heavy work may run now, and what the rider is looking +//! at* (#1397 S5). +//! +//! Four levels and nothing else. Two of them say a planner run holds the scratch arena's nav arm +//! (one per [`PlanFamily`]), one says a bulk transfer holds the store, and the fourth is the +//! level→edge converter the Recalculating banner's single repaint comes from. +//! +//! Everything that used to answer "is a search live?" reads these levels now: the freeze, the two +//! arena proof tokens, and the pass's admission stage. Before S5 that fact existed four times over +//! — a freeze module, a link gate, the arena's owner and the board's own planner handle — and the +//! four could disagree. +//! +//! # The Recalculating freeze (#1146, P2) +//! +//! A route search and a map render want the same RAM (the arena's `render ⊥ nav` rule), and the +//! product rule that makes them disjoint is the one every commercial bike computer already ships: +//! while it recalculates, the map stops. So a live planner run engages a freeze in which +//! +//! - the host skips map redraws ([`App::reroute_freeze_active`](crate::App::reroute_freeze_active)), +//! leaving the last frame on glass — a reflective panel keeps showing it for free; +//! - [`App::tick`](crate::App::tick) stops advancing route-match progress, so the guidance the +//! frozen frame shows cannot drift away from it (fixes still record — breadcrumb, ride totals, +//! altimeter, sensors — a freeze pauses the *map*, never the ride); +//! - a banner says so. A screen that stops responding without saying why reads as a crash, and the +//! freeze lasts as long as the search does. +//! +//! ## Why the base screen matters +//! +//! The freeze is engaged only when the base screen would actually draw a map. Planning from the +//! menus already renders no map — `NavPlanning` is an opaque chrome screen, so it *is* the base +//! while it is up — and freezing there would put a banner over a spinner that is already saying +//! the same thing in its own words ("Finding a route..." for a route plan, "Planning detour..." for +//! a detour). +//! +//! The window that needs this is the **detour** path (#882), where the planning screen is *pushed +//! over a map base*: Back pops it while the planner is still running, and the next frame would +//! render the map straight into the arena the search still owns. One predicate covers both: a live +//! search plus [`base_draws_map`](crate::App::base_draws_map). +//! +//! # Two search levels, never a family tag +//! +//! The nav arm is **one block**, so it stays out until every family that took it is done. A single +//! tag would have to pick a winner, and every terminal edge — a drained cancel, an answer, a +//! failure tier — fires unconditionally on whatever is live: a detour's edge would release a +//! freeze a *route* search is still holding the arm behind, the map plane would resume, and the +//! next frame's render claim would be refused for the rest of the ride (#1146). +//! +//! # No atomics, no task, no latch +//! +//! `CoreMode` is plain data inside [`App`](crate::App), taken by `&mut` for the same reason +//! [`ArenaGate`](crate::ArenaGate) is: the ride loop is the sole switcher. Every level is exactly +//! that — a level, recomputed from what is true now and never latched. + +use crate::arena_gate::{MapQuiesced, TransferReady}; +use crate::navigator::PlanFamily; + +/// What the device is busy with, as the rider would name it — the ranked, payload-free answer. +/// +/// The ranking decides only what the rider is **told**. It never decides admission: that reads the +/// levels, because a search and a transfer exclude different things. +#[derive(Debug, Clone, Copy, PartialEq, Eq, Default)] +pub enum ModeState { + /// Nothing heavy is holding the device. + #[default] + Free, + /// A planner run holds the nav arm. + Searching, + /// A bulk transfer holds the store. + Transferring, +} + +/// The four levels: two searches, one transfer, and the banner's level→edge bit. +#[derive(Debug, Default, PartialEq, Eq)] +pub(crate) struct CoreMode { + /// A live [`Route`](PlanFamily::Route) planner run. + route_search: bool, + /// A live [`Detour`](PlanFamily::Detour) planner run. + detour_search: bool, + /// A bulk transfer is streaming into the store — the latest level reported, never a count. + transferring: bool, + /// Whether the *engaged* freeze — a search **and** a map base — was already reported to the + /// host by a [`take_engaged_edge`](CoreMode::take_engaged_edge) drain. See that method: this is + /// the difference between a banner that appears and one that is silently swallowed. + engaged_shown: bool, +} + +impl CoreMode { + /// The boot state: nothing searching, nothing streaming, no banner shown. + pub(crate) const fn new() -> CoreMode { + CoreMode { route_search: false, detour_search: false, transferring: false, engaged_shown: false } + } + + /// The level `family` owns. + fn slot(&mut self, family: PlanFamily) -> &mut bool { + match family { + PlanFamily::Route => &mut self.route_search, + PlanFamily::Detour => &mut self.detour_search, + } + } + + /// An executor took `family`'s planner operation: the search holds the nav arm from now on. + /// Returns whether this *changed* whether any search is live at all. + /// + /// Written only from [`NavigatorMachine::next_plan_effect`](crate::navigator::NavigatorMachine). + pub(crate) fn search_started(&mut self, family: PlanFamily) -> bool { + let was = self.searching(); + *self.slot(family) = true; + !was + } + + /// A `family` planner run is over — answered, failed, or its cancellation reached the executor. + /// Returns whether that ended the *last* live search. Idempotent (several of those edges + /// legitimately land for one run: a cancel is delivered and the late answer arrives behind it), + /// and it never touches the other family — see the module docs for the regression that is. + /// + /// Written only from `NavigatorMachine`'s `note_answer` / `note_cancel_delivered`. + pub(crate) fn search_ended(&mut self, family: PlanFamily) -> bool { + let was = self.searching(); + *self.slot(family) = false; + was && !self.searching() + } + + /// Whether a planner run holds the nav arm at all — true through a menu plan too, where no + /// freeze is engaged. Deliberately the **union** of the two families. + pub(crate) fn searching(&self) -> bool { + self.route_search || self.detour_search + } + + /// A bulk transfer started or ended. Written only from + /// [`App::set_map_transfer`](crate::App::set_map_transfer) and from + /// [`ExternalFacts::transfer`](crate::device_core::ExternalFacts) at the pass's fact stage — + /// two reports of the same fact, and the newest one is the truth. + pub(crate) fn note_transfer(&mut self, streaming: bool) { + self.transferring = streaming; + } + + /// What the rider is looking at. A search outranks a transfer: it is the shorter, more + /// urgent-looking wait, and it is the one with a banner. + pub(crate) fn state(&self) -> ModeState { + if self.searching() { + ModeState::Searching + } else if self.transferring { + ModeState::Transferring + } else { + ModeState::Free + } + } + + /// Whether a **new** heavy operation may start — the verdict + /// [`Capabilities::calculate`](crate::device_core::Capabilities::calculate) withdraws + /// `plan_route`, `plan_detour` and `dfu.install` on. + /// + /// Reads the levels, not [`state`](CoreMode::state): a search and a transfer each exclude + /// heavy work on their own, so the ranking must not be able to hide one behind the other. + pub(crate) fn admits_heavy(&self) -> bool { + !self.searching() && !self.transferring + } + + /// Whether the freeze is **engaged**: a live search *and* a base screen that would draw a map. + pub(crate) fn frozen(&self, base_draws_map: bool) -> bool { + self.searching() && base_draws_map + } + + /// The level→edge converter the host's once-per-frame dirty drain runs: `true` on the pass the + /// *engaged* state flips, either way. + /// + /// **This is a level, and the search's own start edge is not it.** The two facts the freeze is + /// made of move independently: a search started under the opaque planning spinner engages + /// nothing (chrome base), and the pass that puts a map base back under that still-running + /// search raises no search edge at all — it is a screen change. A host that keyed its overlay + /// repaint on the start edge would spend it on a chrome frame and then draw *nothing* for the + /// rest of the search: the map plane is frozen, the overlay plane was never asked, and the last + /// frame on glass belongs to a screen that is gone. Deriving the edge from the engaged level + /// here means the banner lands whenever a frozen map is what the rider is actually looking at, + /// however it got that way — and lands exactly **once**, so a freeze that spans hundreds of + /// ride-loop passes costs one overlay repaint, not one per pass. + pub(crate) fn take_engaged_edge(&mut self, base_draws_map: bool) -> bool { + let now = self.frozen(base_draws_map); + now != core::mem::replace(&mut self.engaged_shown, now) + } + + /// Mint the proof that the **map plane will not draw this pass**, or `None` when it still + /// would — the precondition on [`ArenaGate::claim_nav`](crate::ArenaGate::claim_nav). + /// + /// Two ways to be quiesced: menu planning happens on a chrome base (there is no map underneath + /// to freeze), and a mid-ride detour plan happens over a **map** base, where the freeze is what + /// makes the second case as safe as the first. + pub(crate) fn nav_precondition(&self, base_draws_map: bool) -> Option { + (self.frozen(base_draws_map) || !base_draws_map).then(MapQuiesced::mint) + } + + /// Mint the proof that a cable upload may take the arena — its transfer screen is up (`render ⊥ + /// usb`) and no search holds the nav arm (`nav ⊥ usb`), or `None`. + pub(crate) fn usb_precondition(&self, transfer_card_up: bool) -> Option { + (transfer_card_up && !self.searching()).then(TransferReady::mint) + } +} + +#[cfg(test)] +mod tests { + use super::*; + + /// The lifecycle in one test: nothing frozen at rest, engaged only where a map would be drawn, + /// and released by whichever edge lands first. + #[test] + fn the_freeze_follows_the_search_and_the_base_screen() { + let mut m = CoreMode::new(); + assert!(!m.searching()); + assert!(!m.frozen(true), "no search, no freeze — the map renders normally"); + + assert!(m.search_started(PlanFamily::Route), "taking the operation is the engaging edge"); + assert!(!m.search_started(PlanFamily::Route), "…and re-engaging is not an edge"); + assert!(m.searching()); + assert!(!m.frozen(false), "menu planning draws no map: nothing to freeze, no banner"); + assert!(m.frozen(true), "a search over a map base is the freeze"); + + assert!(m.search_ended(PlanFamily::Route), "the answer releases it"); + assert!(!m.frozen(true)); + } + + /// **The regression** a stuck freeze would be: the map never redraws again for the rest of the + /// ride. Every release edge is idempotent, so the delivered cancel and the late answer behind + /// it can both fire, in either order, without leaving the level inconsistent. + #[test] + fn releasing_twice_is_harmless_and_a_new_search_re_engages() { + let mut m = CoreMode::new(); + assert!(!m.search_ended(PlanFamily::Detour), "releasing what was never engaged is not an edge"); + assert!(m.search_started(PlanFamily::Detour)); + assert!(m.search_ended(PlanFamily::Detour)); + assert!(!m.search_ended(PlanFamily::Detour), "the late answer behind the cancel is a no-op"); + assert!(!m.frozen(true)); + assert!(m.search_started(PlanFamily::Detour), "and the next reroute freezes again"); + assert!(m.frozen(true)); + } + + /// **The regression** the families exist for, in both directions: every terminal edge fires + /// unconditionally on whatever is live, so one shared level would let a detour's cancel (or the + /// board's immediate `NoPath` answer for the detour half it has not built) release a freeze a + /// *route* search is still holding the nav arm behind — and the very next frame would claim the + /// render arm the search is mid-way through. + #[test] + fn a_search_is_released_only_by_its_own_familys_terminal_edge() { + let mut m = CoreMode::new(); + m.search_started(PlanFamily::Route); + assert!(!m.search_ended(PlanFamily::Detour), "a detour terminal edge is not this run's"); + assert!(m.searching(), "the route search still holds the arm"); + assert!(m.frozen(true), "…so the map stays frozen"); + assert!(m.search_ended(PlanFamily::Route), "only its own answer releases it"); + assert!(!m.searching()); + + // And the mirror image. + m.search_started(PlanFamily::Detour); + assert!(!m.search_ended(PlanFamily::Route)); + assert!(m.frozen(true)); + assert!(m.search_ended(PlanFamily::Detour)); + assert!(!m.frozen(true)); + } + + /// Two runs live at once is reachable through the legacy drain's cancel window, and the arm is + /// **one block** — so the freeze must hold until the last of them is done, not the first. Two + /// levels give that for free; a single family *tag* would not. + #[test] + fn the_freeze_outlives_the_first_of_two_live_runs() { + let mut m = CoreMode::new(); + assert!(m.search_started(PlanFamily::Route)); + assert!(!m.search_started(PlanFamily::Detour), "already live: not a fresh engaging edge"); + assert!(!m.search_ended(PlanFamily::Route), "one down, one to go — not the releasing edge"); + assert!(m.searching()); + assert!(m.search_ended(PlanFamily::Detour), "the last one out releases the freeze"); + assert!(!m.searching()); + } + + /// **The regression** the engaged edge exists for: the search's own start edge fires under the + /// planning spinner, where nothing freezes — and the pass that puts a map base back under the + /// still-live search raises no search edge at all. A host keyed on the start edge would never + /// be told to paint the banner for the whole of that search. + #[test] + fn the_repaint_edge_follows_the_engaged_level_not_the_search() { + let mut m = CoreMode::new(); + assert!(!m.take_engaged_edge(true), "at rest there is nothing to repaint"); + + m.search_started(PlanFamily::Route); // …under the opaque spinner: a chrome base + assert!(!m.take_engaged_edge(false), "a search with no map under it engages nothing"); + assert!(!m.take_engaged_edge(false), "…and keeps engaging nothing"); + + // The spinner goes and a map base is back — no search edge, but *this* is the freeze. + assert!(m.take_engaged_edge(true), "THE edge: a frozen map the rider is actually looking at"); + assert!(!m.take_engaged_edge(true), "a level, so one repaint — not one per ride-loop pass"); + + m.search_ended(PlanFamily::Route); + assert!(m.take_engaged_edge(true), "and one more to take the banner off"); + assert!(!m.take_engaged_edge(true)); + } + + /// The axis stage 12 did not have before S5: a live search withdraws heavy work exactly as a + /// streaming transfer does, so a second plan is never *started* and then failed. + #[test] + fn a_live_search_withdraws_heavy_work() { + let mut m = CoreMode::new(); + assert!(m.admits_heavy(), "at rest the device may start anything"); + m.search_started(PlanFamily::Detour); + assert!(!m.admits_heavy(), "no second plan, and no install, while the planner has the arm"); + m.search_ended(PlanFamily::Detour); + assert!(m.admits_heavy(), "and it comes straight back when the answer lands"); + } + + /// The other half of the same verdict, and the two levels are independent: a transfer teardown + /// never releases a search, and an answer never ends a transfer. (`link_gate`'s + /// `tearing_down_one_side_never_releases_the_other`, on the levels that replaced it.) + #[test] + fn a_streaming_transfer_withdraws_heavy_work_and_the_two_levels_are_independent() { + let mut m = CoreMode::new(); + m.note_transfer(true); + assert!(!m.admits_heavy(), "no reroute while docked-transferring"); + assert!(!m.frozen(true), "…but a transfer is not a freeze: the map plane is the card's"); + + m.search_started(PlanFamily::Route); + m.note_transfer(false); // the transfer concludes mid-search + assert!(m.searching(), "the search is untouched by a transfer ending"); + assert!(!m.admits_heavy()); + + m.note_transfer(true); + assert!(m.search_ended(PlanFamily::Route), "and the answer releases only the search"); + assert!(!m.admits_heavy(), "the transfer still holds the store"); + m.note_transfer(false); + assert!(m.admits_heavy()); + } + + /// The ranking says what the rider is told and nothing else — with both levels set, admission + /// answers the same as it would for either one alone. + #[test] + fn searching_outranks_transferring_and_the_ranking_never_decides_admission() { + let mut m = CoreMode::new(); + assert_eq!(m.state(), ModeState::Free); + m.note_transfer(true); + assert_eq!(m.state(), ModeState::Transferring); + m.search_started(PlanFamily::Route); + assert_eq!(m.state(), ModeState::Searching, "the search is what the rider is waiting on"); + assert!(!m.admits_heavy(), "and both levels still refuse heavy work"); + + m.search_ended(PlanFamily::Route); + assert_eq!(m.state(), ModeState::Transferring, "the transfer underneath is still there"); + assert!(!m.admits_heavy(), "so the ranking hid nothing"); + } + + /// The proof tokens are the gate, and `CoreMode` is now their only mint. Pin exactly which + /// levels mint one. (`arena_gate`'s two precondition tests, re-pointed at the new mint.) + #[test] + fn the_arena_proofs_can_only_be_minted_from_the_levels() { + let mut m = CoreMode::new(); + assert!(m.nav_precondition(false).is_some(), "menu planning: chrome base, no map to freeze"); + assert!( + m.nav_precondition(true).is_none(), + "a map base with no search is the regression: the search would eat the scratch the next frame renders from" + ); + assert!(m.usb_precondition(true).is_some(), "a visible transfer, nothing searching"); + assert!(m.usb_precondition(false).is_none(), "no transfer screen up: the map plane still owns the glass"); + + m.search_started(PlanFamily::Detour); + assert!(m.nav_precondition(true).is_some(), "mid-ride detour: map base, freeze engaged"); + assert!(m.usb_precondition(true).is_none(), "and the cable waits for the search — `nav ⊥ usb`"); + } +} diff --git a/firmware/obc-app/src/device_core/mod.rs b/firmware/obc-app/src/device_core/mod.rs index 5944ed1a8..8502647ea 100644 --- a/firmware/obc-app/src/device_core/mod.rs +++ b/firmware/obc-app/src/device_core/mod.rs @@ -9,6 +9,8 @@ //! - [`OperationToken`] / [`TokenSource`] — the per-domain stale-result guard. //! - [`Capabilities`] — what this device can actually do, recalculated from platform support, //! mounted data and heavy-operation admission. +//! - [`core_mode`] — `CoreMode`, the single owner of "what heavy work may run now, and what the +//! rider is looking at": two search levels, a transfer level, and the freeze's level→edge bit. //! - [`ExternalFacts`] — the facts that are *not* an answer to an effect, with one documented //! merge rule per field. //! @@ -50,6 +52,7 @@ pub mod compat; pub(crate) mod connections; +pub(crate) mod core_mode; pub mod derived; pub mod feeders; pub mod migration; @@ -63,6 +66,7 @@ pub use derived::{ }; pub use compat::{LegacyAdapter, LegacyInputs, LegacyOwned, LegacyPending, LegacyReply, LegacyReport}; +pub use core_mode::ModeState; pub use pass::{PassClock, PassInputs, PassPlan}; pub use slots::{EffectSlots, OutcomeSlots, Slot, SlotFull}; pub use storage_info::{StorageInfoEffect, StorageInfoError, StorageInfoIntent, StorageInfoOutcome}; diff --git a/firmware/obc-app/src/device_core/pass.rs b/firmware/obc-app/src/device_core/pass.rs index 00aa184d7..4eca2008c 100644 --- a/firmware/obc-app/src/device_core/pass.rs +++ b/firmware/obc-app/src/device_core/pass.rs @@ -225,8 +225,6 @@ pub(crate) struct PassState { announced: Option, /// The newest link state seen, so an unchanged level does not re-run the link's card sweep. link: Option, - /// Whether a bulk transfer is streaming — `CoreMode`'s heavy-work verdict rests on it. - transfer: TransferState, /// The active route's durable identity as of the last pass — Navigator's activation edge. active_route: Option, /// What the device can currently do, recalculated at stage 12. @@ -246,7 +244,6 @@ impl PassState { store: None, announced: None, link: None, - transfer: TransferState::Idle, active_route: None, capabilities: Capabilities::NONE, in_pass: false, @@ -382,7 +379,7 @@ impl App { } } if let Some(state) = facts.transfer() { - self.pass.transfer = state; + self.mode.note_transfer(matches!(state, TransferState::Active)); } if let Some(link) = facts.link() { if self.pass.link != Some(link) { @@ -620,7 +617,7 @@ impl App { } } if effects.navigator.is_empty() { - if let Some(effect) = self.navigator.next_effect() { + if let Some(effect) = self.navigator.next_effect(&mut self.mode) { let _ = effects.navigator.try_put(effect); } } @@ -676,9 +673,11 @@ impl App { /// Stage 12 — `CoreMode`: recalculate what this device can do at all. /// /// A capability is a level, never latched: it is recomputed from what the image implements and - /// what is currently true (a mounted store, a routing graph, a streaming transfer, a recording - /// ride). Heavy work is withdrawn while a transfer holds the store — which is what stops a plan - /// or an install from starting, rather than letting one start and fail. + /// what is currently true (a mounted store, a routing graph, a recording ride) and from + /// [`CoreMode`](crate::device_core::core_mode::CoreMode)'s heavy-work verdict. Heavy work is + /// withdrawn while a transfer holds the store **or a planner run holds the nav arm** — which is + /// what stops a second plan or an install from starting, rather than letting one start and + /// fail. The mode is the only store of either level; this stage re-derives nothing. /// /// **One axis cannot yet come back down.** `store_writable` reads "a store has reported a /// revision", and [`ExternalFacts`] has no unmount fact to retract it with, so a pulled card @@ -692,7 +691,7 @@ impl App { weather_data: self.weather.installed().is_some(), link_connected: matches!(self.state.device.ble_link, crate::ble::BleLink::Connected), ride_recording: self.activity.is_tracking(), - heavy_operations: matches!(self.pass.transfer, TransferState::Idle), + heavy_operations: self.mode.admits_heavy(), }; self.pass.capabilities = Capabilities::calculate(support, facts); } @@ -1210,6 +1209,34 @@ mod tests { assert!(app.pass.capabilities.dfu.install, "and it comes straight back"); } + /// The axis this stage did not have before #1397 S5: a **live search** is heavy too. The nav + /// arm is one block, so a second plan started mid-search could only fail — withdrawing the + /// capability is what stops it being offered rather than offered and refused. + #[test] + fn admission_withdraws_heavy_work_while_a_search_holds_the_nav_arm() { + let mut app = navigating(); + app.state.has_nav_graph = true; // planning needs a graph before admission can be the deciding axis + let mut facts = committed(1); + pass_with(&mut app, 10, &[], &mut OutcomeSlots::new(), &mut facts); + let caps = app.pass.capabilities; + assert!(caps.navigator.plan_route && caps.navigator.plan_detour && caps.dfu.install); + + app.debug_set_plan_live(true); + let mut none = ExternalFacts::NONE; + pass_with(&mut app, 20, &[], &mut OutcomeSlots::new(), &mut none); + let caps = app.pass.capabilities; + assert!(!caps.navigator.plan_route, "a second route plan cannot start while one runs"); + assert!(!caps.navigator.plan_detour, "nor a detour"); + assert!(!caps.dfu.install, "nor an install — it reboots, and the search would go with it"); + assert!(caps.navigator.commit_detour, "but a splice is a write, not a search: still offered"); + assert!(caps.catalog.mutate, "and the store is still writable — this is admission, not a fault"); + + app.debug_set_plan_live(false); + let mut none = ExternalFacts::NONE; + pass_with(&mut app, 30, &[], &mut OutcomeSlots::new(), &mut none); + assert!(app.pass.capabilities.navigator.plan_route, "the answer hands the arm back"); + } + /// A platform callback cannot change DeviceCore in the middle of a pass. `run_pass` holds /// `&mut self` for its whole length, so no safe caller can reach a push door mid-pass at all — /// the flag has to be set by hand here. Reaching one anyway is a caller bug, so it is loud in diff --git a/firmware/obc-app/src/device_core/shared.rs b/firmware/obc-app/src/device_core/shared.rs index 372032c9c..2587c964c 100644 --- a/firmware/obc-app/src/device_core/shared.rs +++ b/firmware/obc-app/src/device_core/shared.rs @@ -209,9 +209,9 @@ pub struct DeviceFacts { /// trusted-clock gate). That stays a domain policy rather than a capability: the device *can* /// delete, it simply waits — and a dimmed menu entry would be the wrong way to say so. pub ride_recording: bool, - /// `CoreMode`'s verdict on heavy work. Today it withdraws admission while a transfer streams or - /// an install is armed, but this field carries the verdict, not that list — read `CoreMode` for - /// the current conditions rather than re-deriving them from this sentence. + /// [`CoreMode`](crate::device_core::core_mode::CoreMode)'s verdict on heavy work — a transfer + /// holding the store, or a planner run holding the nav arm. This field carries the verdict, not + /// that list: read `CoreMode` for the current conditions rather than re-deriving them here. pub heavy_operations: bool, } @@ -426,7 +426,16 @@ pub struct WeatherData { } /// Whether a bulk transfer is streaming. Producer: the link and USB control planes. Consumer: -/// `CoreMode`, which withdraws heavy-operation admission while one is in flight. +/// [`CoreMode`](crate::device_core::core_mode::CoreMode), which withdraws heavy-operation admission +/// while one is in flight. +/// +/// **The known gap, stated rather than papered over:** today the only transfer that reports itself +/// is the **map** upload, through +/// [`App::set_map_transfer`](crate::App::set_map_transfer)'s card level. A route, trip or weather +/// upload streams without one, so `CoreMode`'s transfer level does not see it. That is a gap in the +/// *fact* — the flat engine knows the truth — and #1397 S6 closes it by feeding +/// [`note_transfer`](ExternalFacts::note_transfer) from the engine. A fourth derivation here would +/// be a second copy of the level, which is exactly what S5 deleted. #[derive(Debug, Clone, Copy, PartialEq, Eq)] pub enum TransferState { /// No transfer holds the store. diff --git a/firmware/obc-app/src/lib.rs b/firmware/obc-app/src/lib.rs index 7871b8625..4dc799c34 100644 --- a/firmware/obc-app/src/lib.rs +++ b/firmware/obc-app/src/lib.rs @@ -46,14 +46,12 @@ pub mod host; pub mod i18n; pub mod input; pub mod input_plane; -pub mod link_gate; pub mod map_catalog; pub mod nav_profiles; pub mod navigator; pub mod next_ahead; pub(crate) mod placement; pub mod recorder; -pub mod reroute_freeze; pub mod retention; pub mod ride; pub(crate) mod ride_engine; @@ -90,7 +88,6 @@ pub use host::{DetourPreview, DrainStatus, HostCommand, HostEvent, HostMailbox, pub use i18n::{t, Msg}; pub use input::{Gesture, Gestures, DEFAULT_HOLD_MS, DEFAULT_TAP_MS}; pub use input_plane::InputPlane; -pub use link_gate::{GateOwner, TransferGate}; pub use map_catalog::{ boot_fault, choose_map, classify_map_entry, flat_boot_fault, is_superseded_upload, newest_set, set_retirement_keeper, MapChoice, MapEntry, diff --git a/firmware/obc-app/src/link_gate.rs b/firmware/obc-app/src/link_gate.rs deleted file mode 100644 index 35cdfb58a..000000000 --- a/firmware/obc-app/src/link_gate.rs +++ /dev/null @@ -1,268 +0,0 @@ -//! The one-transfer-at-a-time gate, and **which wire holds it** (issue #1039). -//! -//! The companion link arbitrates one transfer across every transport, because the resource being -//! arbitrated is the store rather than the wire: there is one upload handle and one open download -//! source, so two simultaneous uploads would interleave into the same file. A single flag says that -//! much, and for a long time a single flag was enough. -//! -//! It stopped being enough when the transfers grew: **one transfer at a time is not one transport -//! at a time**. Both links can be *connected* while only one is transferring, and each clears its -//! own state when it drops — so a phone walking out of range released the gate the cable was -//! holding, and the next descriptor on the radio was answered `busy`-free while a multi-gigabyte -//! volume set was still streaming. A flag cannot tell whose it is; an owner can. -//! -//! The rule lives here rather than on the board for the reason every pure rule in this crate does: -//! board crate has no `test` harness in CI, and "a teardown releases only its own claim" is exactly -//! the kind of statement that should be asserted rather than reviewed. -//! -//! # The search arm (issue #1146, P2) -//! -//! The gate arbitrates a second resource now: the scratch arena's `nav ⊥ usb` rule (no reroute -//! while docked-transferring). A route search and a cable transfer want the same RAM, and neither -//! belongs to a wire, so the gate carries a **search flag** beside the transfer owner — -//! [`begin_search`](TransferGate::begin_search) / [`end_search`](TransferGate::end_search) — and the -//! two exclude each other: a live search refuses [`claim`](TransferGate::claim), a held transfer -//! refuses `begin_search`. -//! -//! Deliberately a second flag rather than a third [`GateOwner`]: `GateOwner` answers *which wire*, -//! and a search is on no wire. Folding it in would have made [`holder`](TransferGate::holder) — -//! which routes an `Abort` to the data plane actually transferring — answer with something no -//! transport can equal, quietly turning aborts during a search into `busy`. So the split predicates -//! stay honest: [`in_flight`](TransferGate::in_flight) means *a transfer is streaming* (unchanged), -//! and [`busy`](TransferGate::busy) is the "may a new transfer start?" test a control plane answers -//! `busy` from. A control plane that still tests `in_flight` is not *wrong* — [`claim`](TransferGate::claim) -//! is the hard gate and refuses regardless — it is merely late and impolite, arming a transfer that -//! then cannot take the gate. - -use core::sync::atomic::{AtomicBool, AtomicU8, Ordering}; - -/// Which wire holds the transfer gate. -#[derive(Debug, Clone, Copy, PartialEq, Eq)] -pub enum GateOwner { - /// The BLE control plane armed it. - Ble, - /// The USB control plane armed it. - Usb, -} - -impl GateOwner { - const fn tag(self) -> u8 { - match self { - GateOwner::Ble => 1, - GateOwner::Usb => 2, - } - } - - const fn from_tag(tag: u8) -> Option { - match tag { - 1 => Some(GateOwner::Ble), - 2 => Some(GateOwner::Usb), - _ => None, - } - } -} - -/// The gate: idle, or held by one wire. -/// -/// Every plane runs as a cooperative future on one executor, so `Relaxed` is the honest ordering — -/// there is no second core to publish to and no data being handed over, only a flag two futures -/// read between their own await points. [`claim`](Self::claim) is nonetheless a compare-exchange -/// rather than a store, so the gate cannot be taken twice even if that ever changes. -pub struct TransferGate { - owner: AtomicU8, - searching: AtomicBool, -} - -impl TransferGate { - /// An idle gate. - pub const fn new() -> TransferGate { - TransferGate { owner: AtomicU8::new(0), searching: AtomicBool::new(false) } - } - - /// Take the gate for `owner`. `false` = someone already holds it **or a route search is - /// running**, and the caller must answer `busy` rather than arm. - pub fn claim(&self, owner: GateOwner) -> bool { - if self.search_live() { - return false; - } - self.owner.compare_exchange(0, owner.tag(), Ordering::Relaxed, Ordering::Relaxed).is_ok() - } - - /// Release the gate — **only if `owner` is the one holding it**. A teardown on the wire that - /// is not transferring is a no-op, which is the whole point: it must not open the door on a - /// transfer the other wire is still running. - pub fn release(&self, owner: GateOwner) { - let _ = self.owner.compare_exchange(owner.tag(), 0, Ordering::Relaxed, Ordering::Relaxed); - } - - /// Whether any transfer is in flight — the `busy` test, and it is deliberately wire-blind: - /// a second transfer is refused whichever wire offers it. - pub fn in_flight(&self) -> bool { - self.owner.load(Ordering::Relaxed) != 0 - } - - /// Who holds it, if anyone. Lets a control plane tell "my own transfer" from "the other wire's" - /// — an abort aimed at a transfer this wire is not running cannot be forwarded to a data plane - /// that is not listening. - pub fn holder(&self) -> Option { - GateOwner::from_tag(self.owner.load(Ordering::Relaxed)) - } - - /// Take the **search** side of the gate (issue #1146: the nav arm of the scratch arena). - /// `false` = a transfer is streaming, so the search must not start — the rider's reroute waits - /// for the cable, because the alternative is a planner writing its A* table over the bytes the - /// USB data plane is staging into. - /// - /// Not owner-tracked: there is exactly one searcher (the ride loop), whereas transfers arrive on - /// two independent wires. - #[must_use = "a refused search must not start planning — the arena belongs to the transfer"] - pub fn begin_search(&self) -> bool { - if self.in_flight() { - return false; - } - self.searching.compare_exchange(false, true, Ordering::Relaxed, Ordering::Relaxed).is_ok() - } - - /// End the search (the plan answered, failed, or was cancelled). Idempotent, and it releases - /// **only** the search — a transfer that started after it is untouched, exactly as - /// [`release`](TransferGate::release) leaves the other wire's claim alone. - pub fn end_search(&self) { - self.searching.store(false, Ordering::Relaxed); - } - - /// Whether a route search holds the gate's search side. The - /// [`TransferReady`](crate::arena_gate::TransferReady) precondition reads this. - pub fn search_live(&self) -> bool { - self.searching.load(Ordering::Relaxed) - } - - /// Whether a **new transfer** would be refused — a transfer already streaming *or* a live - /// search. The `busy` test a `transferControl` open should answer from; [`in_flight`](TransferGate::in_flight) - /// stays the narrower "is a transfer streaming" fact that abort routing and the data planes use. - pub fn busy(&self) -> bool { - self.in_flight() || self.search_live() - } -} - -impl Default for TransferGate { - fn default() -> Self { - TransferGate::new() - } -} - -#[cfg(test)] -mod tests { - use super::*; - - #[test] - fn a_claimed_gate_refuses_a_second_claim_from_either_wire() { - let gate = TransferGate::new(); - assert!(!gate.in_flight()); - assert_eq!(gate.holder(), None); - - assert!(gate.claim(GateOwner::Usb)); - assert!(gate.in_flight(), "the busy test is wire-blind"); - assert_eq!(gate.holder(), Some(GateOwner::Usb)); - assert!(!gate.claim(GateOwner::Ble), "the radio cannot start a second transfer"); - assert!(!gate.claim(GateOwner::Usb), "and neither can the cable"); - } - - /// **The regression.** A BLE teardown mid-USB-transfer used to clear the shared flag, which - /// re-opened the gate on a transfer that was still streaming — so the next `transferControl` - /// on the radio armed a second one into the same store. - #[test] - fn a_teardown_on_the_idle_wire_does_not_release_the_other_wires_transfer() { - let gate = TransferGate::new(); - assert!(gate.claim(GateOwner::Usb), "the cable is uploading a volume set"); - - gate.release(GateOwner::Ble); // the phone walked out of range - assert!(gate.in_flight(), "the cable still holds it"); - assert_eq!(gate.holder(), Some(GateOwner::Usb)); - assert!(!gate.claim(GateOwner::Ble), "so the radio is still answered busy"); - - gate.release(GateOwner::Usb); // the transfer concludes - assert!(!gate.in_flight()); - assert!(gate.claim(GateOwner::Ble), "and now the radio may have it"); - } - - /// Releasing an idle gate, or releasing twice, is a no-op rather than an underflow — both - /// happen for real: a transfer that answered clears the gate, and the link teardown right - /// behind it clears it again. - #[test] - fn releasing_what_you_do_not_hold_is_a_no_op() { - let gate = TransferGate::new(); - gate.release(GateOwner::Usb); - assert!(!gate.in_flight()); - - assert!(gate.claim(GateOwner::Ble)); - gate.release(GateOwner::Ble); - gate.release(GateOwner::Ble); - assert!(!gate.in_flight()); - assert!(gate.claim(GateOwner::Usb), "and the gate is usable afterwards"); - } - - // --- The `search ⊕ transfer` arm (issue #1146, P2) --- - - /// **The regression** the arm prevents: the rider reroutes while docked and the phone (or the - /// cable) opens a transfer a moment later. Both want the scratch arena, and the transfer's - /// staging buffer would land on the planner's live A* table. - #[test] - fn a_live_search_refuses_transfers_on_both_wires() { - let gate = TransferGate::new(); - assert!(gate.begin_search(), "nothing streaming — the reroute may plan"); - assert!(gate.search_live()); - assert!(gate.busy(), "…and the gate answers busy to a new transfer"); - assert!(!gate.in_flight(), "though no transfer is streaming — the two facts stay distinct"); - - assert!(!gate.claim(GateOwner::Usb), "the cable waits for the search"); - assert!(!gate.claim(GateOwner::Ble), "and so does the radio"); - assert_eq!(gate.holder(), None, "a refused claim leaves the gate unowned, so an abort still routes"); - - gate.end_search(); - assert!(!gate.busy()); - assert!(gate.claim(GateOwner::Usb), "the transfer arms the moment the plan answers"); - } - - /// The mirror: a multi-gigabyte volume set is streaming and the rider asks for a detour. The - /// search is refused (the UI answers "not while transferring"), never started half-owned. - #[test] - fn a_held_transfer_refuses_a_search() { - let gate = TransferGate::new(); - assert!(gate.claim(GateOwner::Usb)); - assert!(!gate.begin_search(), "no reroute while docked-transferring"); - assert!(!gate.search_live(), "and the refusal left no half-set flag behind"); - - gate.release(GateOwner::Usb); - assert!(gate.begin_search(), "the transfer concluded — now it may plan"); - } - - /// Each side releases only itself. The two teardowns run on different clocks (a plan answers - /// while a transfer streams, a link drops while a plan runs), so a release that cleared "the - /// gate" wholesale would re-open the door on work still in flight — the #1039 lesson, applied - /// to the second resource. - #[test] - fn tearing_down_one_side_never_releases_the_other() { - let gate = TransferGate::new(); - assert!(gate.begin_search()); - gate.release(GateOwner::Usb); // a cable teardown arriving mid-search - gate.release(GateOwner::Ble); - assert!(gate.search_live(), "the search is untouched by a transfer teardown"); - - gate.end_search(); - assert!(gate.claim(GateOwner::Ble), "the radio takes the gate once the search ends"); - gate.end_search(); // a stray second end_search behind the answer - assert_eq!(gate.holder(), Some(GateOwner::Ble), "…and it does not release the radio's transfer"); - assert!(!gate.begin_search(), "which still refuses a new search"); - } - - /// `begin_search` twice is a bug, not a nesting: there is one searcher, and the second call - /// would pair with an `end_search` that releases the first search's arena. - #[test] - fn a_second_search_claim_is_refused() { - let gate = TransferGate::new(); - assert!(gate.begin_search()); - assert!(!gate.begin_search(), "one searcher, one claim"); - gate.end_search(); - assert!(gate.begin_search(), "and a fresh search after it ends is fine"); - } -} diff --git a/firmware/obc-app/src/navigator.rs b/firmware/obc-app/src/navigator.rs index 29c55d5fc..5afd4e211 100644 --- a/firmware/obc-app/src/navigator.rs +++ b/firmware/obc-app/src/navigator.rs @@ -7,8 +7,9 @@ //! workspace, run **one** planner step, commit a route, commit a detour, give the resources back. //! //! [`NavigatorMachine`] is that owner. It holds the rider's request until an executor takes it, the -//! [`OperationToken`] the answer must come back with, the per-family phase, and — since #1397 S2 — -//! the [`RerouteFreeze`] the planner's liveness drives. Nothing else may write any of them. +//! [`OperationToken`] the answer must come back with, and the per-family phase. It is also the only +//! writer of [`CoreMode`]'s two **search levels** — the fact "the executor holds the nav arm" — which +//! it sets and clears at the three transitions below and nowhere else. //! //! Bulk stays out: the emitted OBCR bytes, the corridor blacklist and the detour preview *polyline* //! never ride an effect or an outcome. What crosses is an identity, a bounded request, and the @@ -17,11 +18,29 @@ use obc_route::nav::NavError; use crate::activity::{DetourRequest, NavRequest}; +use crate::device_core::core_mode::CoreMode; use crate::device_core::{NavigatorTag, OperationToken, TokenSource}; use crate::host::DetourPreview; -use crate::reroute_freeze::{PlanFamily, RerouteFreeze}; use crate::CatalogObjectId; +/// Which of the two planner flows a start/end edge belongs to. +/// +/// They are **typed apart because their terminal edges are not interchangeable.** Both families +/// engage the same freeze and both take the same nav arm, but each has its own cancel command, its +/// own answer event and its own failure tier — and every one of those fires unconditionally, on +/// whatever is live. Shared as one flag, a detour's terminal edge (a drained `CancelDetour`, or the +/// board's immediate `NoPath` answer for the detour half it has not built yet) would release a +/// freeze a **route** search is still holding the arena behind: the map plane resumes, the next +/// frame claims the render arm, and the gate answers `Busy(Nav)` — a `debug_assert` panic in debug, +/// and in release a map that never redraws again with an unfrozen matcher drifting under it. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub(crate) enum PlanFamily { + /// The route planner (#499): `PlanRoute` → `NavPlanned`, cancelled by `CancelRoutePlan`. + Route, + /// The detour planner (#882): `PlanDetour` → `DetourPlanned`, cancelled by `CancelDetour`. + Detour, +} + /// What the rider (through `UiRuntime`) asks navigation to do. An intent is a *product request*: /// Navigator decides whether it is admissible, what physical work it implies, and what the rider /// then sees. @@ -194,8 +213,8 @@ pub(crate) enum PlanPhase { /// The domain that owns route planning, detour planning, preview and commit. /// /// Everything one rider request passes through lives here and nowhere else: the undelivered -/// request, the cancel that annihilates it, the phase, the operation token, and the freeze the -/// planner's liveness engages. Both compositions reach it through the same three-method seam — +/// request, the cancel that annihilates it, the phase, the operation token, and the [`CoreMode`] +/// search level the planner's liveness drives. Both compositions reach it through the same three-method seam — /// [`admit_intent`](Self::admit_intent), [`next_effect`](Self::next_effect), /// `App::apply_navigator_outcome` — so the legacy drain and the pass cannot disagree about what /// the rider asked for. @@ -205,14 +224,14 @@ pub struct NavigatorMachine { /// [`TokenSource::issue`](crate::device_core::TokenSource::issue) bumps a single generation, so /// only the newest operation is ever current *across both families*. A second concurrent /// operation would therefore make the first one's answer stale, `accepts` would refuse it, and - /// its family's freeze flag would never be released — the "map that never redraws again" - /// [`RerouteFreeze`] names. That is why [`next_plan_effect`](Self::next_plan_effect) and + /// its family's search level would never be released — a map that never redraws again. + /// That is why [`next_plan_effect`](Self::next_plan_effect) and /// [`next_commit_effect`](Self::next_commit_effect) hand out **at most one operation at a /// time**: the constraint is enforced where the token is minted, not assumed. /// - /// `RerouteFreeze`'s two flags are not the same question. They track *edges* — which family's - /// terminal edge may release what — and they stay per-family (#1146) whatever the token layer - /// allows. + /// [`CoreMode`]'s two search levels are not the same question. They track *edges* — which + /// family's terminal edge may release what — and they stay per-family (#1146) whatever the + /// token layer allows. ops: TokenSource, /// The family whose operation an executor is currently holding, if any. `Some` is what makes /// [`next_plan_effect`](Self::next_plan_effect) refuse a second one; it is cleared by the @@ -221,11 +240,6 @@ pub struct NavigatorMachine { /// A [`Release`](NavigatorEffect::Release) never sets it: handing the workspace back owes no /// product answer, so it is not an operation anyone is waiting on. live: Option, - /// The **Recalculating freeze** (#1146): a live planner run over a map base stops map redraws, - /// pauses the matcher and raises the banner. Navigator is its only writer — the four scattered - /// edge calls the drain used to make are the transitions below. S5 derives it from `CoreMode` - /// and deletes the module. - freeze: RerouteFreeze, /// The route family's phase. route: PlanPhase, /// The detour family's phase. @@ -248,7 +262,6 @@ impl NavigatorMachine { NavigatorMachine { ops: TokenSource::new(), live: None, - freeze: RerouteFreeze::new(), route: PlanPhase::Idle, detour: PlanPhase::Idle, route_request: None, @@ -272,10 +285,12 @@ impl NavigatorMachine { /// - **Late-answer refusal**: the operation's token stops being current the instant the rider /// walks away, so the search's eventual answer commits nothing. /// - /// The **freeze is not touched here**. A cancellation the executor has not been handed yet has - /// not stopped anything: the search still owns the nav arm, and resuming the map plane on the - /// rider's keypress is the arena race #1146 exists to prevent. It releases at - /// [`note_cancel_delivered`](Self::note_cancel_delivered). + /// The **search level is not touched here**. A cancellation the executor has not been handed + /// yet has not stopped anything: the search still owns the nav arm, and resuming the map plane + /// on the rider's keypress is the arena race #1146 exists to prevent. It releases at + /// [`note_cancel_delivered`](Self::note_cancel_delivered) — which is why + /// [`live_family`](Self::live_family) and the mode's search level diverge across the whole + /// cancel window, deliberately. pub(crate) fn admit_intent(&mut self, intent: NavigatorIntent) { match intent { NavigatorIntent::PlanRoute(request) => { @@ -326,11 +341,11 @@ impl NavigatorMachine { /// /// Offered in the drain's order — cancellations before new work — so the pass and the legacy /// protocol ask the executor for the same thing in the same sequence. - pub(crate) fn next_effect(&mut self) -> Option { - self.next_release(PlanFamily::Route) - .or_else(|| self.next_release(PlanFamily::Detour)) - .or_else(|| self.next_plan_effect(PlanFamily::Route)) - .or_else(|| self.next_plan_effect(PlanFamily::Detour)) + pub(crate) fn next_effect(&mut self, mode: &mut CoreMode) -> Option { + self.next_release(PlanFamily::Route, mode) + .or_else(|| self.next_release(PlanFamily::Detour, mode)) + .or_else(|| self.next_plan_effect(PlanFamily::Route, mode)) + .or_else(|| self.next_plan_effect(PlanFamily::Detour, mode)) .or_else(|| self.next_commit_effect()) } @@ -355,26 +370,26 @@ impl NavigatorMachine { /// with nothing running is a host-side no-op — and minting a token for it while *another* /// family's search is live would supersede that search's answer, which is the failure /// [`ops`](Self::ops) describes. - fn next_release(&mut self, family: PlanFamily) -> Option { + fn next_release(&mut self, family: PlanFamily, mode: &mut CoreMode) -> Option { if !self.take_cancel(family) { return None; } - self.note_cancel_delivered(family); + self.note_cancel_delivered(family, mode); // `admit_intent` already invalidated this family's operation, so `live` is clear exactly // when the cancellation had something of its own to stop. self.live.is_none().then(|| NavigatorEffect::Release { token: self.ops.issue() }) } /// Hand `family`'s undelivered request to an executor: the operation the search runs under, and - /// the moment the freeze engages. **The engaging edge is here, not at admission** — a request - /// the rider cancelled before anyone took it froze nothing, so nothing needs releasing. + /// the moment the search level engages. **The engaging edge is here, not at admission** — a + /// request the rider cancelled before anyone took it froze nothing, so nothing needs releasing. /// /// Refused while an executor already holds an operation, whichever family's. The request stays /// queued and goes out on a later pass — backpressure, never a loss, and the same shape /// [`CatalogState`](crate::catalog_state::CatalogState) uses. Handing out a second one would /// mint a token that supersedes the first, so the running search's genuine answer would be - /// refused and its freeze flag would be stuck forever (see [`ops`](Self::ops)). - pub(crate) fn next_plan_effect(&mut self, family: PlanFamily) -> Option { + /// refused and its search level would be stuck forever (see [`ops`](Self::ops)). + pub(crate) fn next_plan_effect(&mut self, family: PlanFamily, mode: &mut CoreMode) -> Option { if self.live.is_some() { return None; } @@ -386,12 +401,12 @@ impl NavigatorMachine { PlanFamily::Route => self.route = PlanPhase::Planning, PlanFamily::Detour => self.detour = PlanPhase::Planning, } - self.freeze.plan_started(family); + mode.search_started(family); self.live = Some(family); Some(NavigatorEffect::Acquire { token: self.ops.issue(), work }) } - /// Hand the previewed detour's splice to an executor. No freeze edge: a commit is a write, not + /// Hand the previewed detour's splice to an executor. No search edge: a commit is a write, not /// a search, and it does not take the nav arm. Refused while another operation is in flight, /// for the same reason [`next_plan_effect`](Self::next_plan_effect) is. pub(crate) fn next_commit_effect(&mut self) -> Option { @@ -412,19 +427,19 @@ impl NavigatorMachine { } /// Record a terminal planner answer for `family`: the run is over, so the token stops being - /// current and the freeze releases. Returns whether the freeze changed. + /// current and the search level releases. Returns whether that ended the last live search. /// /// Reached from both answer paths — a typed [`NavigatorOutcome`] at the pass's first stage, and /// a legacy `HostEvent` at [`App::apply_event`](crate::App::apply_event) — so there is one /// definition of "the run ended" whatever spoke. - pub(crate) fn note_answer(&mut self, family: PlanFamily, phase: PlanPhase) -> bool { + pub(crate) fn note_answer(&mut self, family: PlanFamily, phase: PlanPhase, mode: &mut CoreMode) -> bool { self.ops.invalidate(); self.live = None; match family { PlanFamily::Route => self.route = phase, PlanFamily::Detour => self.detour = phase, } - self.freeze.plan_ended(family) + mode.search_ended(family) } /// Whether a detour plan exists at all — requested, running, previewed, committing or adopted. @@ -484,43 +499,26 @@ impl NavigatorMachine { } } - /// The executor has been told to drop `family`'s search: **now** the run is over, so the freeze - /// releases and the map plane may resume. Returns whether that changed the freeze, so the - /// caller can repaint the frame that held still for it. + /// The executor has been told to drop `family`'s search: **now** the run is over, so the search + /// level releases and the map plane may resume. Returns whether that ended the last live + /// search, so the caller can repaint the frame that held still for it. /// /// **Per-family** (#1146): a detour's cancellation must never resume the map while a route /// search still holds the nav arm — the very next frame would claim the render arm out from /// under it. - pub(crate) fn note_cancel_delivered(&mut self, family: PlanFamily) -> bool { - self.freeze.plan_ended(family) - } - - // ---- the freeze, read-only to everyone else ---- - - /// Whether a planner run is live at all — the arena's "is the nav arm claimed?" fact. - pub(crate) fn plan_live(&self) -> bool { - self.freeze.plan_live() - } - - /// Whether the freeze is engaged: a live plan **and** a base screen that would draw the map. - pub(crate) fn freeze_active(&self, base_draws_map: bool) -> bool { - self.freeze.active(base_draws_map) - } - - /// The banner's repaint edge — see [`RerouteFreeze::take_engaged_edge`]. - pub(crate) fn take_freeze_edge(&mut self, base_draws_map: bool) -> bool { - self.freeze.take_engaged_edge(base_draws_map) + pub(crate) fn note_cancel_delivered(&mut self, family: PlanFamily, mode: &mut CoreMode) -> bool { + mode.search_ended(family) } /// Engage or release a `Route` run without a real planner — the simulator's `--freeze` flag and /// the snapshot harness. No production path reaches it. - pub(crate) fn debug_set_plan_live(&mut self, live: bool) -> bool { + pub(crate) fn debug_set_plan_live(&mut self, live: bool, mode: &mut CoreMode) -> bool { if live { - self.freeze.plan_started(PlanFamily::Route); + mode.search_started(PlanFamily::Route); self.route = PlanPhase::Planning; false } else { - self.note_answer(PlanFamily::Route, PlanPhase::Idle) + self.note_answer(PlanFamily::Route, PlanPhase::Idle, mode) } } @@ -535,7 +533,7 @@ impl NavigatorMachine { /// A fresh tracking session starts with no detour in flight. /// - /// Dropping the pair cannot strand the freeze's `Detour` level: an **undelivered** request never + /// Dropping the pair cannot strand the mode's `Detour` search level: an **undelivered** request never /// engaged it (the effect is the engaging edge), and a dropped **cancel** only forfeits one of /// two release edges — the executor is still running the plan that cancel would have aborted, /// and it answers every plan it was given, so the answer's own release lands anyway. @@ -570,7 +568,6 @@ impl NavigatorMachine { let NavigatorMachine { ops, live, - freeze, route, detour, route_request, @@ -581,7 +578,6 @@ impl NavigatorMachine { } = self; assert_eq!(format!("{ops:?}"), "TokenSource(0)", "no navigation operation has been issued"); assert!(live.is_none(), "no operation is in flight"); - assert!(!freeze.plan_live() && !freeze.active(true), "no planner running, no freeze banner"); assert!(*route == PlanPhase::Idle && *detour == PlanPhase::Idle, "neither family has been asked"); assert!(route_request.is_none() && detour_request.is_none(), "no request waiting"); assert!(!*route_cancel && !*detour_cancel && !*detour_commit, "no one-shot latched"); @@ -597,6 +593,61 @@ mod machine_tests { use super::*; use obc_route::nav::NavError; + /// Navigator writes the search levels; `App` owns the `CoreMode` they live in. These tests own + /// one directly so the pair can be driven without an `App`. + struct Nav { + machine: NavigatorMachine, + mode: CoreMode, + } + + impl Nav { + fn new() -> Nav { + Nav { machine: NavigatorMachine::new(), mode: CoreMode::new() } + } + + fn admit_intent(&mut self, intent: NavigatorIntent) { + self.machine.admit_intent(intent); + } + + fn next_effect(&mut self) -> Option { + self.machine.next_effect(&mut self.mode) + } + + fn next_plan_effect(&mut self, family: PlanFamily) -> Option { + self.machine.next_plan_effect(family, &mut self.mode) + } + + fn next_commit_effect(&mut self) -> Option { + self.machine.next_commit_effect() + } + + fn note_answer(&mut self, family: PlanFamily, phase: PlanPhase) -> bool { + self.machine.note_answer(family, phase, &mut self.mode) + } + + fn frozen(&self) -> bool { + self.mode.frozen(true) + } + + fn searching(&self) -> bool { + self.mode.searching() + } + } + + impl core::ops::Deref for Nav { + type Target = NavigatorMachine; + + fn deref(&self) -> &NavigatorMachine { + &self.machine + } + } + + impl core::ops::DerefMut for Nav { + fn deref_mut(&mut self) -> &mut NavigatorMachine { + &mut self.machine + } + } + fn route_request(name: &str) -> NavRequest { NavRequest::new((0, 0), (1_000, 1_000), name) } @@ -623,13 +674,13 @@ mod machine_tests { (NavigatorIntent::PlanRoute(route_request("col")), NavigatorIntent::CancelPlan, PlanFamily::Route), (NavigatorIntent::PlanDetour(detour_request()), NavigatorIntent::CancelDetour, PlanFamily::Detour), ] { - let mut nav = NavigatorMachine::new(); + let mut nav = Nav::new(); nav.admit_intent(plan); nav.admit_intent(cancel); assert!(!nav.request_pending(family), "the undelivered request nets out"); assert!(nav.next_plan_effect(family).is_none(), "so no executor is ever asked to plan it"); assert!(nav.cancel_pending(family), "and the cancel still reaches one"); - assert!(!nav.plan_live(), "nothing froze the map for a plan that never started"); + assert!(!nav.searching(), "nothing froze the map for a plan that never started"); } } @@ -644,16 +695,16 @@ mod machine_tests { /// its flag. The machine refuses the second operation instead, so both halves hold. #[test] fn a_detours_terminal_edge_never_releases_a_route_freeze() { - let mut nav = NavigatorMachine::new(); + let mut nav = Nav::new(); nav.admit_intent(NavigatorIntent::PlanRoute(route_request("col"))); let route = nav.next_plan_effect(PlanFamily::Route).expect("the route search starts"); - assert!(nav.freeze_active(true), "a search over a map base is the freeze"); + assert!(nav.frozen(), "a search over a map base is the freeze"); // A detour cancellation while the route search runs. It is not this run's edge, and it // mints no token — a `Release` here would supersede the search that is still going. nav.admit_intent(NavigatorIntent::CancelDetour); assert!(nav.next_effect().is_none(), "a cancellation with nothing of its own to stop asks for no work"); - assert!(nav.freeze_active(true), "the route search still holds the nav arm"); + assert!(nav.frozen(), "the route search still holds the nav arm"); // A detour *request* while it runs: refused, and the request waits rather than being lost. nav.admit_intent(NavigatorIntent::PlanDetour(detour_request())); @@ -665,24 +716,24 @@ mod machine_tests { let answer = NavigatorOutcome::PlanFinished { token: route.token(), route: 9 }; assert!(nav.accepts(&answer), "the running search's answer is accepted"); assert!(nav.note_answer(PlanFamily::Route, PlanPhase::Active), "and it is what releases the freeze"); - assert!(!nav.freeze_active(true)); + assert!(!nav.frozen()); // Only now does the queued detour go out, and it freezes on its own account. assert!(matches!(acquired(nav.next_effect()), Some(PlannerWork::Detour(_))), "nothing was lost"); - assert!(nav.freeze_active(true)); + assert!(nav.frozen()); assert!(nav.note_answer(PlanFamily::Detour, PlanPhase::PreviewReady), "released by its own edge"); - assert!(!nav.freeze_active(true)); + assert!(!nav.frozen()); } - /// The freeze's own two-flag rule, kept where the machine cannot reach it: two runs live at + /// The mode's own two-level rule, kept where the machine cannot reach it: two runs live at /// once is not a state today's UI can produce — and `next_plan_effect` now refuses to create /// one — but the arm is a single block, so if it ever becomes reachable the freeze must hold - /// until the *last* run is done, not the first. `RerouteFreeze`'s own tests pin that; - /// Navigator's contribution is that it never hands out the second operation that would strand - /// the first one's answer. + /// until the *last* run is done, not the first. [`CoreMode`]'s own tests pin that; Navigator's + /// contribution is that it never hands out the second operation that would strand the first + /// one's answer. #[test] fn a_second_operation_is_refused_rather_than_superseding_the_first() { - let mut nav = NavigatorMachine::new(); + let mut nav = Nav::new(); nav.admit_intent(NavigatorIntent::PlanDetour(detour_request())); let detour = nav.next_plan_effect(PlanFamily::Detour).expect("the detour search starts"); @@ -701,7 +752,7 @@ mod machine_tests { /// current the instant they walked away, so the search's eventual result commits no route. #[test] fn an_answer_after_a_cancellation_is_refused() { - let mut nav = NavigatorMachine::new(); + let mut nav = Nav::new(); nav.admit_intent(NavigatorIntent::PlanRoute(route_request("col"))); let effect = nav.next_plan_effect(PlanFamily::Route).expect("the search starts"); @@ -714,7 +765,7 @@ mod machine_tests { /// older one's answer belongs to nothing. #[test] fn an_answer_after_a_replacement_is_refused() { - let mut nav = NavigatorMachine::new(); + let mut nav = Nav::new(); nav.admit_intent(NavigatorIntent::PlanRoute(route_request("first"))); let first = nav.next_plan_effect(PlanFamily::Route).expect("the first search starts"); @@ -737,7 +788,7 @@ mod machine_tests { /// UI's Detour station is not offered, so no intent is ever admitted. #[test] fn a_detour_without_a_path_is_a_failure_and_not_an_absent_capability() { - let mut nav = NavigatorMachine::new(); + let mut nav = Nav::new(); assert_eq!(nav.detour_phase(), PlanPhase::Idle, "a device that never planned is idle"); nav.admit_intent(NavigatorIntent::PlanDetour(detour_request())); @@ -753,7 +804,7 @@ mod machine_tests { /// which is what makes a failed commit retryable. #[test] fn the_detour_walks_plan_preview_commit_and_a_failure_returns_to_the_preview() { - let mut nav = NavigatorMachine::new(); + let mut nav = Nav::new(); nav.admit_intent(NavigatorIntent::PlanDetour(detour_request())); assert_eq!(nav.detour_phase(), PlanPhase::Requested); assert!(acquired(nav.next_plan_effect(PlanFamily::Detour)).is_some()); @@ -764,13 +815,13 @@ mod machine_tests { assert!(nav.commit_pending()); assert!(matches!(nav.next_commit_effect(), Some(NavigatorEffect::CommitDetour { .. }))); assert_eq!(nav.detour_phase(), PlanPhase::Committing); - assert!(!nav.plan_live(), "a splice is a write, not a search — it takes no nav arm"); + assert!(!nav.searching(), "a splice is a write, not a search — it takes no nav arm"); - nav.note_commit(false); + nav.machine.note_commit(false); assert_eq!(nav.detour_phase(), PlanPhase::PreviewReady, "a failed commit can be retried"); nav.admit_intent(NavigatorIntent::CommitDetour); nav.next_commit_effect().expect("…and the retry goes out"); - nav.note_commit(true); + nav.machine.note_commit(true); assert_eq!(nav.detour_phase(), PlanPhase::Active); } @@ -779,14 +830,14 @@ mod machine_tests { /// preview or a splice the session reset just threw away. #[test] fn a_session_reset_leaves_nothing_describing_the_dropped_detour() { - let mut nav = NavigatorMachine::new(); + let mut nav = Nav::new(); nav.admit_intent(NavigatorIntent::PlanDetour(detour_request())); nav.next_plan_effect(PlanFamily::Detour).expect("the search starts"); nav.note_answer(PlanFamily::Detour, PlanPhase::PreviewReady); nav.admit_intent(NavigatorIntent::CommitDetour); assert!(nav.detour_planned() && nav.commit_pending()); - nav.reset_detour(); + nav.machine.reset_detour(); assert!(!nav.detour_planned(), "no plan"); assert!(!nav.detour_committing(), "no splice"); assert!(!nav.commit_pending() && !nav.request_pending(PlanFamily::Detour)); @@ -798,15 +849,39 @@ mod machine_tests { /// an executor for the same thing in the same sequence. #[test] fn the_pass_offers_a_cancellation_before_new_work() { - let mut nav = NavigatorMachine::new(); + let mut nav = Nav::new(); nav.admit_intent(NavigatorIntent::PlanDetour(detour_request())); nav.next_plan_effect(PlanFamily::Detour).expect("a search is running"); nav.admit_intent(NavigatorIntent::CancelDetour); nav.admit_intent(NavigatorIntent::PlanRoute(route_request("col"))); assert!(matches!(nav.next_effect(), Some(NavigatorEffect::Release { .. })), "the cancellation first"); - assert!(!nav.freeze_active(true), "and delivering it is what releases the detour's freeze"); + assert!(!nav.frozen(), "and delivering it is what releases the detour's freeze"); assert!(matches!(acquired(nav.next_effect()), Some(PlannerWork::Route(_))), "then the new search"); assert!(nav.next_effect().is_none(), "and nothing else is owed"); } + + /// **The cancel window**, and the reason `live_family()` is not the mode's search level. + /// + /// `live` answers "is an operation current?" — a cancellation clears it the instant the rider + /// presses Back. The mode's level answers "does the executor still hold the nav arm?", and that + /// stays true until the `Release` actually reaches it. Across that window the two disagree on + /// purpose: resuming the map plane on the keypress is the arena race #1146 exists to prevent. + #[test] + fn the_live_operation_and_the_search_level_diverge_across_the_cancel_window() { + let mut nav = Nav::new(); + nav.admit_intent(NavigatorIntent::PlanDetour(detour_request())); + nav.next_plan_effect(PlanFamily::Detour).expect("the search starts"); + assert_eq!(nav.live_family(), Some(PlanFamily::Detour)); + assert!(nav.searching(), "and the executor holds the arm"); + + nav.admit_intent(NavigatorIntent::CancelDetour); + assert!(nav.live_family().is_none(), "the operation stopped being current at the keypress"); + assert!(nav.searching(), "…but the executor has not been told yet — the arm is still out"); + assert!(nav.frozen(), "so the map stays frozen through the whole window"); + + assert!(matches!(nav.next_effect(), Some(NavigatorEffect::Release { .. })), "the cancellation goes out"); + assert!(!nav.searching(), "and delivering it is what releases the arm"); + assert!(!nav.frozen()); + } } diff --git a/firmware/obc-app/src/reroute_freeze.rs b/firmware/obc-app/src/reroute_freeze.rs deleted file mode 100644 index 2337f46a7..000000000 --- a/firmware/obc-app/src/reroute_freeze.rs +++ /dev/null @@ -1,297 +0,0 @@ -//! The **Recalculating freeze** (issue #1146, P2): the map plane holds still while the host plans. -//! -//! A route search and a map render want the same RAM (the scratch arena's `render ⊥ nav` rule), and -//! the product rule that makes them disjoint is the one every commercial bike computer already -//! ships: while it recalculates, the map stops. So a live planner run engages a freeze in which -//! -//! - the host skips map redraws ([`App::reroute_freeze_active`](crate::App::reroute_freeze_active)), -//! leaving the last frame on glass — a reflective panel keeps showing it for free; -//! - [`App::tick`](crate::App::tick) stops advancing route-match progress, so the guidance the -//! frozen frame shows cannot drift away from it (fixes still record — breadcrumb, ride totals, -//! altimeter, sensors — a freeze pauses the *map*, never the ride); -//! - a banner says so. A screen that stops responding without saying why reads as a crash, and the -//! freeze lasts as long as the search does. -//! -//! # Why the base screen matters -//! -//! The freeze is engaged only when the base screen would actually draw a map. Planning from the -//! menus already renders no map — `NavPlanning` is an opaque chrome screen, so it *is* the base -//! while it is up — and freezing there would put a banner over a spinner that is already saying -//! the same thing in its own words ("Finding a route..." for a route plan, "Planning detour..." for -//! a detour). -//! -//! The window that needs this is the **detour** path (#882), where the planning screen is *pushed -//! over a map base*: Back pops it while the host's planner is still running, and the next frame -//! would render the map straight into the arena the search still owns. One predicate covers both: -//! a live plan plus [`base_draws_map`](crate::App::base_draws_map). -//! -//! # The banner lives on the overlay plane -//! -//! Drawing it on the map plane would mean rendering the map — the exact thing the freeze forbids. -//! It is painted by [`App::render_overlay`](crate::App::render_overlay) instead, the cheap half that -//! composites over the still-visible frame, beside the long-press bulge. - -use embedded_graphics::{draw_target::DrawTarget, prelude::Point}; -use obc_render::{ - rect, - text::{text_width, Font, TextAlign}, - Canvas, Surface, -}; - -use crate::screen::palette; - -/// Banner height (px) — the map's status-chip height, so the two chrome pills read as one family. -const BANNER_H: i32 = 36; -/// Horizontal padding (px) around the copy, split either side — tighter than the status chip's 28, -/// because the copy is one long word: at 240 px the longest catalogued string ("Neuberechnung...") -/// would otherwise leave under 10 px of frame either side and read as a full-width bar. -const BANNER_PAD_X: i32 = 20; -/// Corner radius (px) — the shared pill radius. -const BANNER_RADIUS: u32 = 9; -/// Where the banner's top sits, as a fraction of frame height. A third of the way down: clear of -/// the top-centre clock, and well above the centred rider marker the rider is looking at (the map -/// under the banner is frozen, not gone — covering the marker would read as "lost"). -const BANNER_Y_FRAC: f32 = 0.3; - -/// Which of the two planner flows a start/end edge belongs to. -/// -/// They are **typed apart because their terminal edges are not interchangeable.** Both families -/// engage the same freeze and both take the same nav arm, but each has its own cancel command, its -/// own answer event and its own failure tier — and every one of those fires unconditionally, on -/// whatever is live. Shared as one flag, a detour's terminal edge (a drained `CancelDetour`, or the -/// board's immediate `NoPath` answer for the detour half it has not built yet) would release a -/// freeze a **route** search is still holding the arena behind: the map plane resumes, the next -/// frame claims the render arm, and the gate answers `Busy(Nav)` — a `debug_assert` panic in debug, -/// and in release a map that never redraws again with an unfrozen matcher drifting under it. -#[derive(Debug, Clone, Copy, PartialEq, Eq)] -pub(crate) enum PlanFamily { - /// The route planner (#499): `PlanRoute` → `NavPlanned`, cancelled by `CancelRoutePlan`. - Route, - /// The detour planner (#882): `PlanDetour` → `DetourPlanned`, cancelled by `CancelDetour`. - Detour, -} - -/// Whether a host planner run is live — the freeze's whole state — plus the one bit that turns that -/// *level* into the repaint *edge* a render-on-demand host can act on. -/// -/// The interesting part is where the plan flags are set and cleared: the app engages one when a plan -/// command is actually drained (the host will begin planning this pass) and releases it on the -/// answer, on the failure, and on a cancel drain — **matched by [`PlanFamily`]**. Anything else — a -/// plan the rider cancelled before the host ever saw it, a late answer whose screen is gone — must -/// not leave it stuck, since a stuck freeze is a map that never redraws again. -#[derive(Debug, Default)] -pub(crate) struct RerouteFreeze { - /// A live [`Route`](PlanFamily::Route) run. - route_live: bool, - /// A live [`Detour`](PlanFamily::Detour) run. One flag each rather than a family *tag*: two runs - /// live at once is not a state the UI can reach today, and a tag would have to pick a winner if - /// it ever did — two levels simply hold the freeze until both are done. - detour_live: bool, - /// Whether the *engaged* freeze — plan **and** map base — was already reported to the host by a - /// [`take_engaged_edge`](RerouteFreeze::take_engaged_edge) drain. See that method: this is the - /// difference between a banner that appears and one that is silently swallowed. - engaged_shown: bool, -} - -impl RerouteFreeze { - pub(crate) const fn new() -> RerouteFreeze { - RerouteFreeze { route_live: false, detour_live: false, engaged_shown: false } - } - - /// The flag `family` owns. - fn slot(&mut self, family: PlanFamily) -> &mut bool { - match family { - PlanFamily::Route => &mut self.route_live, - PlanFamily::Detour => &mut self.detour_live, - } - } - - /// A plan command was drained: the host begins a `family` planner run this pass. Returns whether - /// this *changed* whether any run is live at all. - pub(crate) fn plan_started(&mut self, family: PlanFamily) -> bool { - let was = self.plan_live(); - *self.slot(family) = true; - !was - } - - /// A `family` planner run is over — answered, failed, or cancelled. Returns whether that ended - /// the *last* live run. Idempotent (several of those edges legitimately land for one run: a - /// cancel drains and the late answer arrives behind it), and it never touches the other family: - /// see [`PlanFamily`] for the regression that is. - pub(crate) fn plan_ended(&mut self, family: PlanFamily) -> bool { - let was = self.plan_live(); - *self.slot(family) = false; - was && !self.plan_live() - } - - /// Whether a planner run is live at all — true through a menu plan too, where no freeze is - /// engaged. This is the "is the arena's nav arm claimed?" fact, and it is deliberately the - /// **union**: the arm is one block, so it stays out until every family that took it is done. - pub(crate) fn plan_live(&self) -> bool { - self.route_live || self.detour_live - } - - /// Whether the freeze is **engaged**: a live plan *and* a base screen that would draw the map. - pub(crate) fn active(&self, base_draws_map: bool) -> bool { - self.plan_live() && base_draws_map - } - - /// The level→edge converter the host's once-per-frame dirty drain runs: `true` on the pass the - /// *engaged* state flips, either way. - /// - /// **This is a level, and the plan flag alone is not it.** The plan's own start edge is useless - /// to the banner, because the two facts the freeze is made of move independently: a plan drained - /// under the opaque planning spinner engages nothing (chrome base), and the pass that puts a map - /// base back under that still-running search raises no plan edge at all — it is a screen change. - /// A host that keyed its overlay repaint on the plan edge would spend it on a chrome frame and - /// then draw *nothing* for the rest of the search: the map plane is frozen, the overlay plane was - /// never asked, and the last frame on glass belongs to a screen that is gone. Deriving the edge - /// from the engaged level here means the banner lands whenever a frozen map is what the rider is - /// actually looking at, however it got that way — and lands exactly **once**, so a freeze that - /// spans hundreds of ride-loop passes costs one overlay repaint, not one per pass. - pub(crate) fn take_engaged_edge(&mut self, base_draws_map: bool) -> bool { - let now = self.active(base_draws_map); - now != core::mem::replace(&mut self.engaged_shown, now) - } -} - -/// The banner's bounding rows `[y0, y0 + rows)` in a `h`-high frame — what a partial-overlay host -/// re-presents (the board pushes overlay rows, not whole frames). -pub(crate) fn banner_rows(h: f32) -> (u16, u16) { - let y0 = (h * BANNER_Y_FRAC) as i32; - let y0 = y0.clamp(0, (h as i32 - BANNER_H).max(0)); - (y0 as u16, BANNER_H.min(h as i32).max(0) as u16) -} - -/// Draw the "Recalculating..." banner: a centred parchment pill with an ink outline and the copy in -/// ink — the calm chip idiom (the alert orange stays reserved for the No-GPS / off-route chip, which -/// is *below* on the frozen map plane and never collides with this band). -pub(crate) fn draw_banner(target: &mut D, color_fn: &F, w: f32, h: f32, text: &str) -where - D: DrawTarget, - F: Fn(u16) -> D::Color, -{ - let (w, h) = (w as i32, h as i32); - // [`Font::Label`], not the status chip's Body: the copy is a long word in every language - // ("Neuberechnung...", "Recalculando..."), and the pill must keep a margin at 240 px. - let font = Font::Label; - let (y0, _) = banner_rows(h as f32); - let pw = (text_width(text, font) as i32 + BANNER_PAD_X).min(w - 8); - let px = (w - pw) / 2; - let py = y0 as i32; - let mut cv = Canvas::new(target, color_fn); - cv.round(rect(px, py, pw, BANNER_H), BANNER_RADIUS, palette::PARCHMENT); - cv.round_outline(rect(px, py, pw, BANNER_H), BANNER_RADIUS, palette::INK); - cv.text(text, Point::new(w / 2, py + 5), font, TextAlign::Center, palette::INK); -} - -#[cfg(test)] -mod tests { - use super::*; - - /// The lifecycle in one test: nothing frozen at rest, engaged only where a map would be drawn, - /// and released by whichever edge lands first. - #[test] - fn the_freeze_follows_the_plan_and_the_base_screen() { - let mut f = RerouteFreeze::new(); - assert!(!f.plan_live()); - assert!(!f.active(true), "no plan, no freeze — the map renders normally"); - - assert!(f.plan_started(PlanFamily::Route), "the drain is the engaging edge"); - assert!(!f.plan_started(PlanFamily::Route), "…and re-engaging is not an edge"); - assert!(f.plan_live()); - assert!(!f.active(false), "menu planning draws no map: nothing to freeze, no banner"); - assert!(f.active(true), "a plan over a map base is the freeze"); - - assert!(f.plan_ended(PlanFamily::Route), "the answer releases it"); - assert!(!f.active(true)); - } - - /// **The regression** a stuck freeze would be: the map never redraws again for the rest of the - /// ride. Every release edge is idempotent, so the cancel drain and the late answer behind it can - /// both fire, in either order, without leaving the flag inconsistent. - #[test] - fn releasing_twice_is_harmless_and_a_new_plan_re_engages() { - let mut f = RerouteFreeze::new(); - assert!(!f.plan_ended(PlanFamily::Detour), "releasing what was never engaged is not an edge"); - assert!(f.plan_started(PlanFamily::Detour)); - assert!(f.plan_ended(PlanFamily::Detour)); - assert!(!f.plan_ended(PlanFamily::Detour), "the late answer behind the cancel is a no-op"); - assert!(!f.active(true)); - assert!(f.plan_started(PlanFamily::Detour), "and the next reroute freezes again"); - assert!(f.active(true)); - } - - /// **The regression** the families exist for, in both directions: every terminal edge fires - /// unconditionally on whatever is live, so one shared flag would let a detour's cancel (or the - /// board's immediate `NoPath` answer for the detour half it has not built) release a freeze a - /// *route* search is still holding the nav arm behind — and the very next frame would claim the - /// render arm the search is mid-way through. - #[test] - fn a_plan_is_released_only_by_its_own_familys_terminal_edge() { - let mut f = RerouteFreeze::new(); - f.plan_started(PlanFamily::Route); - assert!(!f.plan_ended(PlanFamily::Detour), "a detour terminal edge is not this run's"); - assert!(f.plan_live(), "the route search still holds the arm"); - assert!(f.active(true), "…so the map stays frozen"); - assert!(f.plan_ended(PlanFamily::Route), "only its own answer releases it"); - assert!(!f.plan_live()); - - // And the mirror image. - f.plan_started(PlanFamily::Detour); - assert!(!f.plan_ended(PlanFamily::Route)); - assert!(f.active(true)); - assert!(f.plan_ended(PlanFamily::Detour)); - assert!(!f.active(true)); - } - - /// Two runs live at once is not reachable through today's UI, but the arm is **one block** — so - /// if it ever becomes reachable the freeze must hold until the last of them is done, not the - /// first. Two levels give that for free; a single family *tag* would not. - #[test] - fn the_freeze_outlives_the_first_of_two_live_runs() { - let mut f = RerouteFreeze::new(); - assert!(f.plan_started(PlanFamily::Route)); - assert!(!f.plan_started(PlanFamily::Detour), "already live: not a fresh engaging edge"); - assert!(!f.plan_ended(PlanFamily::Route), "one down, one to go — not the releasing edge"); - assert!(f.plan_live()); - assert!(f.plan_ended(PlanFamily::Detour), "the last one out releases the freeze"); - assert!(!f.plan_live()); - } - - /// **The regression** the engaged edge exists for: the plan's own start edge fires under the - /// planning spinner, where nothing freezes — and the pass that puts a map base back under the - /// still-live search raises no plan edge at all. A host keyed on the start edge would never be - /// told to paint the banner for the whole of that search. - #[test] - fn the_repaint_edge_follows_the_engaged_level_not_the_plan() { - let mut f = RerouteFreeze::new(); - assert!(!f.take_engaged_edge(true), "at rest there is nothing to repaint"); - - f.plan_started(PlanFamily::Route); // …under the opaque spinner: a chrome base - assert!(!f.take_engaged_edge(false), "a plan with no map under it engages nothing"); - assert!(!f.take_engaged_edge(false), "…and keeps engaging nothing"); - - // The spinner goes and a map base is back — no plan edge, but *this* is the freeze. - assert!(f.take_engaged_edge(true), "THE edge: a frozen map the rider is actually looking at"); - assert!(!f.take_engaged_edge(true), "a level, so one repaint — not one per ride-loop pass"); - - f.plan_ended(PlanFamily::Route); - assert!(f.take_engaged_edge(true), "and one more to take the banner off"); - assert!(!f.take_engaged_edge(true)); - } - - /// The banner sits in its own band: below the top-centre clock, above the centred rider marker, - /// and always fully on-panel. - #[test] - fn the_banner_band_stays_on_panel_and_clear_of_the_marker() { - let (y0, rows) = banner_rows(320.0); - assert_eq!((y0, rows), (96, 36)); - assert!(y0 as i32 + rows as i32 <= 320); - assert!((y0 + rows) < 160, "clear of the centred user marker"); - - let (y0, rows) = banner_rows(20.0); // a frame shorter than the banner (the test harnesses') - assert_eq!(y0, 0, "clamped to the top rather than drawn off-panel"); - assert_eq!(rows, 20); - } -} diff --git a/firmware/obc-app/src/screen/detour.rs b/firmware/obc-app/src/screen/detour.rs index 7e5d5aade..f3bf575e8 100644 --- a/firmware/obc-app/src/screen/detour.rs +++ b/firmware/obc-app/src/screen/detour.rs @@ -562,8 +562,8 @@ fn inspect_viewport(w: i32, h: i32, candidate: (i32, i32), overview_zoom: f32, f #[cfg(test)] mod tests { use super::*; - use crate::navigator::{NavigatorEffect, NavigatorMachine, PlannerWork}; - use crate::reroute_freeze::PlanFamily; + use crate::device_core::core_mode::CoreMode; + use crate::navigator::{NavigatorEffect, NavigatorMachine, PlanFamily, PlannerWork}; use crate::screen::test_ctx; use crate::{AppState, Settings}; use obc_ports::Fix; @@ -585,9 +585,11 @@ mod tests { f(&mut cx) } - /// The detour-plan request Navigator holds, taken as an executor would. + /// The detour-plan request Navigator holds, taken as an executor would. The search level rides + /// on the app's `CoreMode`; these tests read the request, not the mode, so a scratch one is + /// enough. fn drained_detour(nav: &mut NavigatorMachine) -> Option { - match nav.next_plan_effect(PlanFamily::Detour) { + match nav.next_plan_effect(PlanFamily::Detour, &mut CoreMode::new()) { Some(NavigatorEffect::Acquire { work: PlannerWork::Detour(req), .. }) => Some(req), other => { assert!(other.is_none(), "the detour arm only ever acquires a detour: {other:?}"); diff --git a/firmware/obc-app/src/screen/vocab/chrome.rs b/firmware/obc-app/src/screen/vocab/chrome.rs index 4b6893cd8..eb64f9e59 100644 --- a/firmware/obc-app/src/screen/vocab/chrome.rs +++ b/firmware/obc-app/src/screen/vocab/chrome.rs @@ -1,11 +1,12 @@ -//! The screen **chrome** — the framed page header every screen draws through, the card glyphs, and -//! the small shared text/stroke helpers the bodies below it are assembled from. +//! The screen **chrome** — the framed page header every screen draws through, the card glyphs, the +//! Recalculating banner, and the small shared text/stroke helpers the bodies below it are assembled +//! from. -use embedded_graphics::prelude::Point; +use embedded_graphics::{draw_target::DrawTarget, prelude::Point}; use obc_render::{ rect, - text::{Font, TextAlign}, - Surface, + text::{text_width, Font, TextAlign}, + Canvas, Surface, }; use crate::screen::palette; @@ -167,9 +168,79 @@ pub(crate) fn stroke2(cv: &mut impl Surface, a: Point, b: Point, color: u16) { cv.line(a + off, b + off, color); } +// ==================== the Recalculating banner (issue #1146, P2) ==================== +// +// The overlay chrome the freeze raises. Drawing it on the map plane would mean rendering the map — +// the exact thing the freeze forbids — so it is painted by +// [`App::render_overlay`](crate::App::render_overlay) instead, the cheap half that composites over +// the still-visible frame, beside the long-press bulge. Whether it is up at all is +// [`CoreMode`](crate::device_core::core_mode::CoreMode)'s answer; this is only how it looks. + +/// Banner height (px) — the map's status-chip height, so the two chrome pills read as one family. +const BANNER_H: i32 = 36; +/// Horizontal padding (px) around the copy, split either side — tighter than the status chip's 28, +/// because the copy is one long word: at 240 px the longest catalogued string ("Neuberechnung...") +/// would otherwise leave under 10 px of frame either side and read as a full-width bar. +const BANNER_PAD_X: i32 = 20; +/// Corner radius (px) — the shared pill radius. +const BANNER_RADIUS: u32 = 9; +/// Where the banner's top sits, as a fraction of frame height. A third of the way down: clear of +/// the top-centre clock, and well above the centred rider marker the rider is looking at (the map +/// under the banner is frozen, not gone — covering the marker would read as "lost"). +const BANNER_Y_FRAC: f32 = 0.3; + +/// The banner's bounding rows `[y0, y0 + rows)` in a `h`-high frame — what a partial-overlay host +/// re-presents (the board pushes overlay rows, not whole frames). +pub(crate) fn recalculating_banner_rows(h: f32) -> (u16, u16) { + let y0 = (h * BANNER_Y_FRAC) as i32; + let y0 = y0.clamp(0, (h as i32 - BANNER_H).max(0)); + (y0 as u16, BANNER_H.min(h as i32).max(0) as u16) +} + +/// Draw the "Recalculating..." banner: a centred parchment pill with an ink outline and the copy in +/// ink — the calm chip idiom (the alert orange stays reserved for the No-GPS / off-route chip, which +/// is *below* on the frozen map plane and never collides with this band). +pub(crate) fn recalculating_banner(target: &mut D, color_fn: &F, w: f32, h: f32, text: &str) +where + D: DrawTarget, + F: Fn(u16) -> D::Color, +{ + let (w, h) = (w as i32, h as i32); + // [`Font::Label`], not the status chip's Body: the copy is a long word in every language + // ("Neuberechnung...", "Recalculando..."), and the pill must keep a margin at 240 px. + let font = Font::Label; + let (y0, _) = recalculating_banner_rows(h as f32); + let pw = (text_width(text, font) as i32 + BANNER_PAD_X).min(w - 8); + let px = (w - pw) / 2; + let py = y0 as i32; + let mut cv = Canvas::new(target, color_fn); + cv.round(rect(px, py, pw, BANNER_H), BANNER_RADIUS, palette::PARCHMENT); + cv.round_outline(rect(px, py, pw, BANNER_H), BANNER_RADIUS, palette::INK); + cv.text(text, Point::new(w / 2, py + 5), font, TextAlign::Center, palette::INK); +} + /// Draw a centered two-line empty state — a bold `title` over a muted `hint` — the shared /// "nothing to show yet" body the Route menu and Statistics draw under their header. pub(crate) fn empty_state(cv: &mut impl Surface, w: i32, h: i32, title: &str, hint: &str) { cv.text(title, Point::new(w / 2, h / 2 - 28), Font::Body, TextAlign::Center, palette::INK); cv.text(hint, Point::new(w / 2, h / 2 + 8), Font::Label, TextAlign::Center, palette::SUBTEXT); } + +#[cfg(test)] +mod tests { + use super::*; + + /// The banner sits in its own band: below the top-centre clock, above the centred rider marker, + /// and always fully on-panel. + #[test] + fn the_recalculating_banner_band_stays_on_panel_and_clear_of_the_marker() { + let (y0, rows) = recalculating_banner_rows(320.0); + assert_eq!((y0, rows), (96, 36)); + assert!(y0 as i32 + rows as i32 <= 320); + assert!((y0 + rows) < 160, "clear of the centred user marker"); + + let (y0, rows) = recalculating_banner_rows(20.0); // a frame shorter than the banner (the test harnesses') + assert_eq!(y0, 0, "clamped to the top rather than drawn off-panel"); + assert_eq!(rows, 20); + } +} diff --git a/firmware/obc-app/tests/detour_flow.rs b/firmware/obc-app/tests/detour_flow.rs index ba1a65c64..c982adb4e 100644 --- a/firmware/obc-app/tests/detour_flow.rs +++ b/firmware/obc-app/tests/detour_flow.rs @@ -16,6 +16,7 @@ //! engages, pauses the matcher, raises its banner, and — on every exit the flow has — releases. use embedded_graphics::pixelcolor::Rgb888; +use obc_app::device_core::ModeState; use obc_app::screen::{palette, Screen}; use obc_app::{ App, AppState, DetourPreview, DetourRequest, Gesture, HostCommand, HostEvent, HostMailbox, RouteSummary, @@ -270,6 +271,12 @@ fn frozen_over_the_chooser(app: &mut App) { assert!(matches!(app.top_screen(), Screen::Detour(_))); } +/// Whether a planner run holds the nav arm — `CoreMode`'s search level, read through the one public +/// mode. No transfer streams in this file, so `Searching` is exactly "a search is live". +fn searching(app: &App) -> bool { + app.core_mode() == ModeState::Searching +} + fn rgb(c: u16) -> Rgb888 { let (r, g, b) = rgb565_to_rgb888(c); Rgb888::new(r, g, b) @@ -284,25 +291,25 @@ fn rgb(c: u16) -> Rgb888 { fn the_freeze_covers_a_live_search_exactly_while_a_map_base_would_draw() { let (mut app, _obcr) = riding_app(); assert!(app.base_draws_map(), "riding on the Map"); - assert!(!app.plan_in_flight()); + assert!(!searching(&app)); assert!(!app.reroute_freeze_active(), "no plan, no freeze"); assert!(app.nav_arena_precondition().is_none(), "…so a search may not take the arena yet"); open_chooser(&mut app); app.apply_gesture(Gesture::Press); assert!(drained(&mut app).iter().any(|c| matches!(c, HostCommand::PlanDetour(_)))); - assert!(app.plan_in_flight(), "the drained command is what says the host began planning"); + assert!(searching(&app), "the drained command is what says the host began planning"); assert!(!app.base_draws_map(), "the spinner is an opaque chrome base — no map underneath to freeze"); assert!(!app.reroute_freeze_active(), "menu-shaped planning needs no freeze"); assert!(app.nav_arena_precondition().is_some(), "…and the arena is claimable: nothing will draw a map"); app.apply_gesture(Gesture::Back); assert!(app.base_draws_map(), "the chooser is a map base again"); - assert!(app.plan_in_flight(), "…while the host has not been told to stop yet"); + assert!(searching(&app), "…while the host has not been told to stop yet"); assert!(app.reroute_freeze_active(), "THE window — the freeze covers it"); assert!(drained(&mut app).iter().any(|c| matches!(c, HostCommand::CancelDetour))); - assert!(!app.plan_in_flight(), "the cancel reaching the host ends the run"); + assert!(!searching(&app), "the cancel reaching the host ends the run"); assert!(!app.reroute_freeze_active()); assert!(app.nav_arena_precondition().is_none(), "a map base with no freeze refuses the nav claim again"); } @@ -420,7 +427,7 @@ fn the_banner_lands_when_a_map_base_returns_under_a_search_that_already_started( app.apply_gesture(Gesture::BackHold); // the ride menu: an opaque chrome base assert!(!app.base_draws_map(), "no map underneath the menu"); app.debug_set_plan_live(true); // the host begins a planner run - assert!(app.plan_in_flight()); + assert!(searching(&app)); assert!(!app.reroute_freeze_active(), "a chrome base freezes nothing — and needs no banner"); assert_eq!(board.pass(&mut app), Painted::Frame, "the menu frame renders normally"); @@ -449,7 +456,7 @@ fn a_detour_terminal_edge_leaves_a_live_route_search_frozen() { // A detour answer lands anyway — a stray event, or #882's board half answering its own request. app.apply_event(HostEvent::DetourPlanned(Err(NavError::NoPath))); - assert!(app.plan_in_flight(), "the route search is untouched by another family's answer"); + assert!(searching(&app), "the route search is untouched by another family's answer"); assert!(app.reroute_freeze_active(), "so the map stays frozen"); app.apply_event(HostEvent::DetourCommitted(Err(NavError::NoPath))); assert!(app.reroute_freeze_active(), "…and by its commit failure too"); @@ -457,7 +464,7 @@ fn a_detour_terminal_edge_leaves_a_live_route_search_frozen() { // Only the route family's own terminal edge releases it. app.debug_set_plan_live(false); assert!(!app.reroute_freeze_active()); - assert!(!app.plan_in_flight()); + assert!(!searching(&app)); } /// And the mirror: a live **detour** plan is not released by the route family's cancel drain. Same @@ -473,7 +480,7 @@ fn a_route_cancel_leaves_a_live_detour_plan_frozen() { // A route answer for a run that isn't this one (a late `NavPlanned` behind a cancelled plan). app.apply_event(HostEvent::NavPlanned(Err(NavError::NoPath))); - assert!(app.plan_in_flight(), "the detour search is still the arm's holder"); + assert!(searching(&app), "the detour search is still the arm's holder"); assert!(app.reroute_freeze_active()); assert!(drained(&mut app).iter().any(|c| matches!(c, HostCommand::CancelDetour))); @@ -493,12 +500,12 @@ fn the_board_loop_renders_the_map_again_the_pass_a_cancel_lands() { assert_eq!(board.pass(&mut app), Painted::Frame, "the chooser is a map base"); app.apply_gesture(Gesture::Press); // → the spinner, and the request assert_eq!(board.pass(&mut app), Painted::Frame, "the spinner renders; the plan drains with it"); - assert!(app.plan_in_flight()); + assert!(searching(&app)); app.apply_gesture(Gesture::Back); // pops the spinner *and* pends the cancel assert!(app.reroute_freeze_active(), "frozen until the cancel actually reaches the host"); assert_eq!(board.pass(&mut app), Painted::Frame, "which it does on this pass — so the map redraws"); - assert!(!app.plan_in_flight()); + assert!(!searching(&app)); assert_eq!(board.pass(&mut app), Painted::Nothing, "and nothing is left demanding a repaint"); } @@ -573,7 +580,7 @@ fn every_way_a_plan_ends_releases_the_freeze() { open_chooser(&mut app); app.apply_gesture(Gesture::Press); let _ = drained(&mut app); - assert!(app.plan_in_flight()); + assert!(searching(&app)); app.apply_event(HostEvent::DetourPlanned(Ok(DetourPreview { cost_delta_m: 420, total_distance_m: 1_020, @@ -582,7 +589,7 @@ fn every_way_a_plan_ends_releases_the_freeze() { }))); assert!(matches!(app.top_screen(), Screen::DetourPreview(_))); assert!(app.base_draws_map(), "the preview is a map base"); - assert!(!app.plan_in_flight(), "the answer ended the run"); + assert!(!searching(&app), "the answer ended the run"); assert!(!app.reroute_freeze_active(), "so the preview's first frame renders"); // The failure tier: same release, on a card that isn't a map base at all. @@ -591,16 +598,16 @@ fn every_way_a_plan_ends_releases_the_freeze() { app.apply_gesture(Gesture::Press); let _ = drained(&mut app); app.apply_event(HostEvent::DetourPlanned(Err(NavError::Exhausted))); - assert!(!app.plan_in_flight(), "a failed run is still a finished run"); + assert!(!searching(&app), "a failed run is still a finished run"); // A late answer behind a cancel: the run already ended, and the stray event must not re-engage // (or leave) anything. let (mut app, _obcr) = riding_app(); frozen_over_the_chooser(&mut app); let _ = drained(&mut app); - assert!(!app.plan_in_flight()); + assert!(!searching(&app)); app.apply_event(HostEvent::DetourPlanned(Err(NavError::NoPath))); - assert!(!app.plan_in_flight()); + assert!(!searching(&app)); assert!(!app.reroute_freeze_active(), "the map keeps rendering through a late answer"); } diff --git a/firmware/obc-fw-nrf54l/src/link/mod.rs b/firmware/obc-fw-nrf54l/src/link/mod.rs index 356405fa4..a0209591d 100644 --- a/firmware/obc-fw-nrf54l/src/link/mod.rs +++ b/firmware/obc-fw-nrf54l/src/link/mod.rs @@ -10,7 +10,6 @@ //! - [`command::run_command`] — the §4.4 imperatives (`deleteObject`, `ackRides`, `installFw`, //! `forgetBond`, `setClock`, `setRouteRetention`). Takes the store, returns a typed outcome; it //! has never had a radio in it. -//! - [`Armed`] + [`TRANSFER_ACTIVE`] — the one-transfer-at-a-time gate. **Deliberately shared //! - [`identity`] — the FICR-derived serial/name, the DIS strings, and the Config / //! `protocolVersion` blob codecs, in plain bytes. BLE's GATT table wraps them into its //! attribute-value types; USB writes the same bytes into a control frame. @@ -132,8 +131,6 @@ pub fn publish_stack_high_water(bytes: usize) { STACK_HIGH_WATER.store(bytes as u32, Ordering::Relaxed); } -// ============================ Data-plane arming ============================ - // ============================ Map-transfer progress mirror (issue #927) ============================ // // A map upload writes for **minutes**. The ride loop owns the `App` and is the only task that may @@ -241,21 +238,6 @@ pub fn clear_map_transfer() { } } -/// One transfer at a time, **across every transport**: claimed by whichever control plane armed it, -/// released by that transport's data plane when the transfer concludes (answered, aborted, or the -/// channel dropped). -/// -/// Shared rather than per-transport because the resource being arbitrated is the store, not the -/// wire: [`ObjectStore`] holds exactly one upload handle and one open download source. Two -/// simultaneous uploads would interleave into the same file and commit a corrupt object. -/// -/// It carries **who holds it** rather than merely whether it is held (issue #1039), because one -/// transfer at a time is not one transport at a time: both links can be connected at once, and each -/// tears its own state down when it drops. A bare flag meant a phone walking out of range released -/// a gate the cable was holding mid-set. The rule — and the regression — live in -/// [`obc_app::link_gate`], where they can be tested. -pub(crate) static TRANSFER_ACTIVE: obc_app::TransferGate = obc_app::TransferGate::new(); - // ============================ Status-message vocabulary ============================ /// A `status` message's bytes, ready to hand to a transport (`&buf[..len]`). Each plane keeps one diff --git a/firmware/obc-fw-nrf54l/src/main.rs b/firmware/obc-fw-nrf54l/src/main.rs index 88d9c245c..3fbbacde9 100644 --- a/firmware/obc-fw-nrf54l/src/main.rs +++ b/firmware/obc-fw-nrf54l/src/main.rs @@ -800,7 +800,7 @@ async fn spawn_map_recovery_usb( // No ride loop, map render or route search exists on this boot path. Retain the arena guard in // the caller's diverging fault scope and pre-grant it, so the first post-FORMAT map upload gets // the same double-buffer DMA path as an ordinary mounted boot. - let stage = obc_app::TransferReady::prove(true, false).and_then(|ready| arena::claim_usb(ready).ok()); + let stage = arena::claim_usb(obc_app::TransferReady::recovery_boot()).ok(); usb::set_stage_granted(stage.is_some()); spawner.spawn(defmt::unwrap!(spawn_usb_stack(spawner, usb_p))); defmt::warn!("usb: card-recovery plane active — format if needed, then upload a map and reboot"); diff --git a/firmware/obc-fw-nrf54l/src/ride.rs b/firmware/obc-fw-nrf54l/src/ride.rs index efbec7bc8..63ad1d255 100644 --- a/firmware/obc-fw-nrf54l/src/ride.rs +++ b/firmware/obc-fw-nrf54l/src/ride.rs @@ -354,28 +354,28 @@ fn nav_begin(nav: &mut NavBuffers, req: &obc_app::NavRequest, profile_idx: u8) { ); } -/// Take everything a fresh route search needs, in the order that leaves nothing half-held: the -/// transfer gate's **search arm** first (a cable transfer streaming into the same store must win — -/// the arena's `nav ⊥ usb` rule), then the scratch arena's **nav arm** against the app's own +/// Take the scratch arena's **nav arm** for a fresh route search, against the app's own /// quiesced-map proof. /// -/// `Err(why)` = the caller must answer the failure tier now rather than arm a plan; every refusal -/// path has already given back whatever it took, so no spinner can hang behind a half-claim. A -/// request arriving while a plan is still in flight is *not* a refusal: we already hold both, and -/// the drain overwrites the planner slot for the new plan exactly as it did before. +/// `Err(why)` = the caller must answer the failure tier now rather than arm a plan; a refused claim +/// took nothing, so no spinner can hang behind a half-claim. A request arriving while a plan is +/// still in flight is *not* a refusal: we already hold the arm, and the drain overwrites the +/// planner slot for the new plan exactly as it did before. +/// +/// The arena's own owner is what enforces `nav ⊥ usb` — a cable transfer streaming into the same +/// store holds the block, so the claim is refused by ownership rather than by a second gate +/// tracking the same fact. The refusal *names* that holder, because "wait for the cable" is +/// something the rider can act on and "the scratch arena is busy" is not. #[cfg(has_nav)] fn nav_take_arena(app: &App, guard: &mut Option) -> Result<(), &'static str> { + use obc_app::{ArenaError, ArenaOwner}; if guard.is_some() { return Ok(()); } - if !crate::link::TRANSFER_ACTIVE.begin_search() { - return Err("a cable transfer holds the store"); - } let Some(quiesced) = app.nav_arena_precondition() else { // Unreachable by construction: draining a plan command is what engages the Recalculating // freeze, so by the time we are here the map plane is already quiet over a map base — and // menu planning has no map base to quiet. Loud in debug, handled in release. - crate::link::TRANSFER_ACTIVE.end_search(); debug_assert!(false, "a plan drained with the map plane still drawing — the freeze did not engage"); return Err("the map plane is not quiesced"); }; @@ -384,10 +384,8 @@ fn nav_take_arena(app: &App, guard: &mut Option) -> Resu *guard = Some(g); Ok(()) } - Err(_) => { - crate::link::TRANSFER_ACTIVE.end_search(); - Err("the scratch arena is busy") - } + Err(ArenaError::Busy(ArenaOwner::Usb)) => Err("a cable transfer holds the store"), + Err(_) => Err("the scratch arena is busy"), } } @@ -1059,11 +1057,7 @@ pub(crate) async fn run_app( let wants_stage = crate::usb::stage_requested(); if wants_stage && usb_stage_guard.is_none() { - #[cfg(has_nav)] - let search_live = nav_run.is_some(); - #[cfg(not(has_nav))] - let search_live = false; - if let Some(ready) = obc_app::TransferReady::prove(app.map_transfer_card_up(), search_live) { + if let Some(ready) = app.usb_stage_precondition() { if let Ok(guard) = crate::arena::claim_usb(ready) { usb_stage_guard = Some(guard); crate::usb::set_stage_granted(true); @@ -1823,11 +1817,10 @@ pub(crate) async fn run_app( search_ended = true; } if search_ended { - // Drop the guard (releasing the arena so the next frame can render the map - // again), then the gate's search arm — in that order, because a transfer that - // arms the instant the search arm opens must find the arena free. + // Drop the guard, releasing the arena so the next frame can render the map + // again — and so a transfer waiting on it finds the block free. The app's own + // search level was released by the answer that set `search_ended`. nav_guard = None; - crate::link::TRANSFER_ACTIVE.end_search(); } } #[cfg(not(has_nav))] diff --git a/tools/check_screen_vocabulary.py b/tools/check_screen_vocabulary.py index 7c1182e1a..f088e6d66 100644 --- a/tools/check_screen_vocabulary.py +++ b/tools/check_screen_vocabulary.py @@ -27,6 +27,7 @@ LANDMARKS = [ "title_frame", "card_triangle", + "recalculating_banner", "ledger_row", "draw_guarded_rows", "tile", diff --git a/tools/s5_core_mode_soak.py b/tools/s5_core_mode_soak.py new file mode 100644 index 000000000..f2cc010b6 --- /dev/null +++ b/tools/s5_core_mode_soak.py @@ -0,0 +1,428 @@ +#!/usr/bin/env python3 +"""Drive the three `CoreMode` on-glass soaks (#1397 S5, #1487) over the DK's VCOM harness. + +**Death trigger: delete this file when #1487 closes with soaks A, B and C recorded.** It exists to +produce one piece of evidence a host test cannot: on a shipping build a refused arena claim degrades +*silently* — the frame skips its map redraw and tries again — so "the map never redraws again" is a +failure only a running board can show. Once that run is recorded, the mechanism is covered by +`CoreMode`'s host tests and git history is the archive for this rig. + + # one shell: the RTT log this script reads + cd firmware/obc-fw-nrf54l + DEFMT_LOG=debug cargo rtt --release --features debug-uart | tee /tmp/s5-rtt.log + + # another: the driver + python3 tools/s5_core_mode_soak.py A --rtt-log /tmp/s5-rtt.log --cycles 50 + python3 tools/s5_core_mode_soak.py B --rtt-log /tmp/s5-rtt.log + python3 tools/s5_core_mode_soak.py C --rtt-log /tmp/s5-rtt.log --minutes 60 + +## The rig, and the two ways it lies to you + +* Build `--release --features debug-uart` — the sensors are swapped for the VCOM feed so a ride can + be driven headlessly. **HWFC must be OFF** in the Board Configurator or host→device injection is + silently ignored; `stty` + `printf` does not work, which is why this is pyserial at 115200 with + `rtscts=False`. +* **The J-Link CDC wedges silently**: `write()` succeeds, RTT keeps flowing, and nothing lands — a + blind script then "passes" every step. [`liveness_probe`] runs before every scenario and between + scenario A's cycles: snapshot the RTT log size, send six taps, wait, re-check. Zero growth means + wedged, and only a physical DK power-cycle clears it. +* `nav plan: start` is a `defmt::debug!`, so the RTT shell needs `DEFMT_LOG=debug`. Without it every + cycle reports a missing start line and the run is worthless. + +Everything above `Link` is pure log/plan analysis with no pyserial in it, which is what +`tools/tests/test_s5_core_mode_soak.py` drives against recorded RTT text. +""" + +from __future__ import annotations + +import argparse +from dataclasses import dataclass, field +import glob +import os +from pathlib import Path +import sys +import time + +# ── the RTT vocabulary this soak reads (mirrors `firmware/obc-fw-nrf54l/src/ride.rs`) ──────────── + +PLAN_START = "nav plan: start" +MAP_FRAME = "map frame:" +UI_FRAME = "ui frame:" +PLAN_REFUSED = "nav: cannot start a plan" +USB_GRANTED = "arena: 64 KiB USB write-combining arm granted" +USB_RECLAIMED = "arena: USB write-combining arm reclaimed" +ARENA_REFUSED = "claim refused" +ARENA_RELEASE_REFUSED = "release refused" +STACK_PEAK = "stack high-water" +BOOT_FAULT = "boot fault" + +# The refusal string `nav_take_arena` answers a live cable transfer with. Scenario B's whole point: +# the rider must be told about the cable, not about "the scratch arena". +REFUSAL_TRANSFER = "a cable transfer holds the store" +REFUSAL_ARENA = "the scratch arena is busy" + +# `deep_ride_margin_min` from `firmware/tools/resource_baseline.json` — scenario C fails if a +# reported stack peak eats into it. +STACK_RESERVE = 65_536 +DEEP_RIDE_MARGIN_MIN = 8_704 + + +@dataclass +class Cycle: + """What one plan cycle produced, as read back out of the RTT log.""" + + started: bool = False + banner_frames: int = 0 + map_frames: int = 0 + arena_refusals: list[str] = field(default_factory=list) + refusals: list[str] = field(default_factory=list) + + def verdict(self) -> str | None: + """`None` when the cycle passed, else why it did not.""" + if not self.started: + return f"no `{PLAN_START}` line — the plan never armed (or DEFMT_LOG is not debug)" + if self.banner_frames == 0: + return "the freeze raised no banner frame — the rider saw a map that simply stopped" + if self.banner_frames > 1: + return f"{self.banner_frames} banner frames for one freeze — the edge is repainting per pass" + if self.map_frames != 1: + return f"{self.map_frames} full map repaints after the answer — expected exactly one catch-up" + if self.arena_refusals: + return f"the arena refused a claim: {'; '.join(self.arena_refusals)}" + return None + + +def read_cycle(lines: list[str]) -> Cycle: + """Fold one cycle's RTT lines into a [`Cycle`]. Ordering is not asserted here — `verdict` is + about counts, and `assert_sequence` below is what pins the order.""" + cycle = Cycle() + for line in lines: + if PLAN_START in line: + cycle.started = True + elif UI_FRAME in line and cycle.started: + cycle.banner_frames += 1 + elif MAP_FRAME in line and cycle.started: + cycle.map_frames += 1 + elif ARENA_REFUSED in line or ARENA_RELEASE_REFUSED in line: + cycle.arena_refusals.append(line.strip()) + elif PLAN_REFUSED in line: + cycle.refusals.append(line.strip()) + return cycle + + +def assert_sequence(lines: list[str]) -> str | None: + """The order scenario A pins: start → banner → the catch-up repaint. A map frame *before* the + banner means the map plane drew while the nav arm was out, which is the whole regression.""" + order = [ + kind + for line in lines + for kind in ( + ["start"] + if PLAN_START in line + else ["banner"] + if UI_FRAME in line + else ["map"] + if MAP_FRAME in line + else [] + ) + ] + if "start" not in order: + return "no plan start in this window" + after = order[order.index("start") :] + if "banner" not in after: + return "no banner after the start" + if "map" in after and after.index("map") < after.index("banner"): + return "a full map repaint landed between the start and the banner — the freeze did not hold" + return None + + +def stack_peaks(lines: list[str]) -> list[int]: + """Every `stack high-water N / M B` peak in the window, in bytes.""" + peaks = [] + for line in lines: + if STACK_PEAK not in line: + continue + tail = line.split(STACK_PEAK, 1)[1].split("/")[0] + digits = "".join(c for c in tail if c.isdigit()) + if digits: + peaks.append(int(digits)) + return peaks + + +def margin_verdict(peaks: list[int]) -> str | None: + """Scenario C's stack gate: the deepest reported peak must leave `deep_ride_margin_min` free.""" + if not peaks: + return None + worst = max(peaks) + margin = STACK_RESERVE - worst + if margin < DEEP_RIDE_MARGIN_MIN: + return f"stack peak {worst} B leaves {margin} B, under the {DEEP_RIDE_MARGIN_MIN} B floor" + return None + + +def faults(lines: list[str]) -> list[str]: + """Boot faults and WDT resets seen in the window — either one ends a soak.""" + return [line.strip() for line in lines if BOOT_FAULT in line.lower() or "watchdog" in line.lower()] + + +# ── the wire ───────────────────────────────────────────────────────────────────────────────────── + + +class Link: + """The VCOM line, and the RTT log beside it. Every `send` is one `\\n`-terminated debug-link + message (`obc_platform::debug_link`'s wire).""" + + def __init__(self, port: str, rtt_log: Path, baud: int = 115_200) -> None: + import serial # imported here so the analysis half above stays importable without pyserial + + self.port = serial.Serial(port, baud, timeout=1, rtscts=False) + self.rtt_log = rtt_log + + def send(self, line: str) -> None: + self.port.write((line + "\n").encode()) + self.port.flush() + + def mark(self) -> int: + """The RTT log's current size — the cursor `since` reads from.""" + return self.rtt_log.stat().st_size if self.rtt_log.exists() else 0 + + def since(self, mark: int) -> list[str]: + """Every RTT line written since `mark`.""" + if not self.rtt_log.exists(): + return [] + with self.rtt_log.open("r", errors="replace") as fh: + fh.seek(mark) + return fh.readlines() + + # -- the gestures, in the debug-link vocabulary -- + + def press(self) -> None: + self.send("K s d") + time.sleep(0.05) + self.send("K s u") + + def back(self) -> None: + self.send("K b d") + time.sleep(0.05) + self.send("K b u") + + def back_hold(self, ms: int = 900) -> None: + self.send("K b d") + time.sleep(ms / 1000) + self.send("K b u") + + def step(self, n: int) -> None: + self.send(f"K t {n}") + + def fix(self, lat_ud: int, lon_ud: int) -> None: + self.send(f"F {lat_ud} {lon_ud}") + + def zoom(self, mpp: float) -> None: + self.send(f"Z {mpp}") + + +def liveness_probe(link: Link) -> None: + """**Run this before trusting a single assertion.** The J-Link CDC wedges with `write()` still + succeeding and RTT still flowing, and a blind script then passes every step against a board that + heard nothing. Six taps must move the RTT log; zero growth is a wedge, and only a physical DK + power-cycle clears it.""" + mark = link.mark() + for _ in range(6): + link.step(1) + time.sleep(0.1) + time.sleep(2.0) + if link.mark() == mark: + raise SystemExit( + "VCOM is wedged: six injected taps produced no RTT output at all.\n" + "Power-cycle the DK physically (a re-flash does not clear it) and start again." + ) + + +# ── the scenarios ──────────────────────────────────────────────────────────────────────────────── + + +def ride_to_map(link: Link) -> None: + """Fresh boot → Home → RouteMenu → RouteOverview → Map; the ride starts.""" + for _ in range(3): + link.press() + time.sleep(0.4) + + +def stream_fixes(link: Link, base: tuple[int, int], steps: int, delay: float = 1.0) -> None: + """`F` fixes at ~1 Hz in small increments — teleport rejection drops anything larger.""" + lat, lon = base + for i in range(steps): + link.fix(lat + i * 40, lon + i * 40) + time.sleep(delay) + + +def scenario_a(link: Link, cycles: int, base: tuple[int, int]) -> int: + """**A — the freeze window over a map base (`render ⊥ nav`).** + + The only way a map base lands under a live search: back out of the planning spinner while the + planner is still running. Each cycle must show start → banner → answer → exactly one full + repaint, with no arena refusal anywhere.""" + print(f"A: {cycles} freeze cycles over a map base") + ride_to_map(link) + stream_fixes(link, base, 3) + failures = 0 + for i in range(cycles): + if i % 10 == 0: + liveness_probe(link) + mark = link.mark() + link.back_hold() # the ride menu + time.sleep(0.4) + link.step(1) # → Detour + time.sleep(0.2) + link.press() # the rejoin chooser + time.sleep(0.4) + link.press() # posts the plan and pushes the spinner + time.sleep(0.15) + link.back() # …and pop it *while the planner runs* — THE window + stream_fixes(link, (base[0] + i, base[1] + i), 3) + lines = link.since(mark) + cycle = read_cycle(lines) + why = cycle.verdict() or assert_sequence(lines) + if why: + failures += 1 + print(f" cycle {i}: FAIL — {why}") + elif i % 10 == 0: + print(f" cycle {i}: ok") + print(f"A: {cycles - failures}/{cycles} cycles passed") + return failures + + +def scenario_b(link: Link) -> int: + """**B — `nav ⊥ usb` and `render ⊥ usb`.** Semi-automatic: a hand on the cable. + + The plan offered during an upload must be refused *before* the planner arms, and the refusal + must name the transfer — not "the scratch arena is busy", and not a `NoPath`.""" + print("B: plug the cable into J3, load a route, and start a map upload; press Enter when the") + print(" transfer card is up.") + input() + mark = link.mark() + link.back_hold() + time.sleep(0.4) + link.step(1) + time.sleep(0.2) + link.press() + time.sleep(0.4) + link.press() + time.sleep(1.0) + lines = link.since(mark) + refusals = [line for line in lines if PLAN_REFUSED in line] + failures = 0 + if not refusals: + print(" FAIL — the plan was not refused during the upload") + failures += 1 + elif not any(REFUSAL_TRANSFER in line for line in refusals): + print(f" FAIL — refused, but not by name: {refusals[0].strip()}") + failures += 1 + elif any(REFUSAL_ARENA in line for line in refusals): + print(" FAIL — the rider was told the arena is busy; the cable is the actionable fact") + failures += 1 + else: + print(" refusal names the transfer: ok") + + print("B: end the upload, then press Enter.") + input() + mark = link.mark() + link.back_hold() + time.sleep(0.4) + link.step(1) + time.sleep(0.2) + link.press() + time.sleep(0.4) + link.press() + time.sleep(1.0) + lines = link.since(mark) + if any(PLAN_REFUSED in line for line in lines): + print(" FAIL — the same input is still refused after the upload ended") + failures += 1 + elif not any(PLAN_START in line for line in lines): + print(" FAIL — no plan started after the upload ended") + failures += 1 + else: + print(" the plan arms normally afterwards: ok") + + grants = sum(1 for line in lines if USB_GRANTED in line) + reclaims = sum(1 for line in lines if USB_RECLAIMED in line) + print(f" arena arm: {grants} granted / {reclaims} reclaimed (expect one each per upload)") + return failures + + +def scenario_c(link: Link, minutes: int, base: tuple[int, int]) -> int: + """**C — the stuck-freeze soak.** A continuous ride with a plan cycle every ~60 s and a periodic + zoom nudge. Every freeze release must be followed by a map render within two wakes, and the + stack must never eat into `deep_ride_margin_min`.""" + print(f"C: {minutes} minutes of continuous riding with a plan cycle every 60 s") + ride_to_map(link) + deadline = time.time() + minutes * 60 + failures = 0 + cycle_no = 0 + while time.time() < deadline: + mark = link.mark() + link.zoom(30.0 if cycle_no % 2 else 20.0) + stream_fixes(link, (base[0] + cycle_no * 10, base[1]), 25) + link.back_hold() + time.sleep(0.4) + link.step(1) + time.sleep(0.2) + link.press() + time.sleep(0.4) + link.press() + time.sleep(0.15) + link.back() + stream_fixes(link, (base[0] + cycle_no * 10, base[1]), 20) + lines = link.since(mark) + why = read_cycle(lines).verdict() + fault_lines = faults(lines) + margin = margin_verdict(stack_peaks(lines)) + for problem in [why, margin] + fault_lines: + if problem: + failures += 1 + print(f" cycle {cycle_no}: FAIL — {problem}") + cycle_no += 1 + print(f"C: {cycle_no} cycles over {minutes} min, {failures} failures") + return failures + + +def resolve_port(explicit: str | None) -> str: + if explicit: + return explicit + matches = sorted(glob.glob("/dev/cu.usbmodem*133")) + if not matches: + raise SystemExit("no /dev/cu.usbmodem*133 — is the DK plugged in?") + return matches[0] + + +def main() -> int: + parser = argparse.ArgumentParser(description=__doc__, formatter_class=argparse.RawDescriptionHelpFormatter) + parser.add_argument("scenario", choices=["A", "B", "C"]) + parser.add_argument("--port", help="VCOM device (default: the first /dev/cu.usbmodem*133)") + parser.add_argument("--rtt-log", required=True, type=Path, help="the file `cargo rtt` is tee'd into") + parser.add_argument("--cycles", type=int, default=50, help="scenario A plan cycles (>=50 is the gate)") + parser.add_argument("--minutes", type=int, default=60, help="scenario C duration (60 is the gate)") + parser.add_argument("--lat", type=int, default=47_990_000, help="starting fix latitude, microdegrees") + parser.add_argument("--lon", type=int, default=7_850_000, help="starting fix longitude, microdegrees") + args = parser.parse_args() + + if not args.rtt_log.exists(): + raise SystemExit(f"{args.rtt_log} does not exist — start `DEFMT_LOG=debug cargo rtt … | tee` first") + + link = Link(resolve_port(args.port), args.rtt_log) + liveness_probe(link) + base = (args.lat, args.lon) + if args.scenario == "A": + failures = scenario_a(link, args.cycles, base) + elif args.scenario == "B": + failures = scenario_b(link) + else: + failures = scenario_c(link, args.minutes, base) + + print("PASS" if failures == 0 else f"FAIL ({failures})") + return 0 if failures == 0 else 1 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/tools/tests/test_s5_core_mode_soak.py b/tools/tests/test_s5_core_mode_soak.py new file mode 100644 index 000000000..3a189d756 --- /dev/null +++ b/tools/tests/test_s5_core_mode_soak.py @@ -0,0 +1,82 @@ +"""The `CoreMode` soak driver's log analysis, against recorded RTT text. + +**Death trigger: delete with `tools/s5_core_mode_soak.py` when #1487 closes.** The script's whole +value is that a blind driver "passes" everything — a wedged VCOM, a `DEFMT_LOG` that swallows the +plan-start line, a map frame that lands *before* the banner. These pin the verdicts that catch each +of those, off recorded lines, so the rig is not itself the thing under test on the board. +""" + +import unittest + +from tools.s5_core_mode_soak import ( + DEEP_RIDE_MARGIN_MIN, + STACK_RESERVE, + assert_sequence, + faults, + margin_verdict, + read_cycle, + stack_peaks, +) + +START = "0.100 DEBUG nav plan: start planner=0x2000a000 scratch=0x2000b000 tiles=0x2000c000" +BANNER = "0.150 INFO ui frame: render 900 us + push 300 us (screen redraw, no map)" +MAP = "0.900 INFO map frame: render 41000 us + push 3000 us | lod 2 | feat 900/1200 | chunks 8" +BUSY = "0.400 ERROR arena: render claim refused — held by Nav" + + +class CycleVerdicts(unittest.TestCase): + def test_a_clean_cycle_passes(self): + self.assertIsNone(read_cycle([START, BANNER, MAP]).verdict()) + self.assertIsNone(assert_sequence([START, BANNER, MAP])) + + def test_a_missing_plan_start_is_the_defmt_level_trap(self): + """No `nav plan: start` means either the plan never armed or RTT is not at debug — and a + driver that ignored it would report a clean run against a board that planned nothing.""" + why = read_cycle([BANNER, MAP]).verdict() + self.assertIn("never armed", why) + + def test_a_freeze_with_no_banner_is_a_map_that_simply_stopped(self): + why = read_cycle([START, MAP]).verdict() + self.assertIn("no banner", why) + + def test_the_banner_is_one_repaint_per_freeze_not_one_per_pass(self): + """The level→edge converter's whole point. Hundreds of ride-loop passes, one overlay + repaint.""" + why = read_cycle([START, BANNER, BANNER, MAP]).verdict() + self.assertIn("repainting per pass", why) + + def test_exactly_one_catch_up_repaint_after_the_answer(self): + self.assertIn("0 full map repaints", read_cycle([START, BANNER]).verdict()) + self.assertIn("2 full map repaints", read_cycle([START, BANNER, MAP, MAP]).verdict()) + + def test_an_arena_refusal_fails_the_cycle_however_it_ends(self): + """**The failure this soak exists for**: a refused claim degrades silently on a shipping + build, so the log line is the only witness.""" + why = read_cycle([START, BANNER, BUSY, MAP]).verdict() + self.assertIn("arena refused", why) + + def test_a_map_frame_before_the_banner_means_the_freeze_did_not_hold(self): + """Counts alone would pass this: one start, one banner, one map frame. The *order* is what + says the map plane drew while the nav arm was still out.""" + self.assertIsNone(read_cycle([START, MAP, BANNER]).verdict()) + self.assertIn("freeze did not hold", assert_sequence([START, MAP, BANNER])) + + +class StackAndFaults(unittest.TestCase): + def test_peaks_are_read_and_the_margin_floor_is_enforced(self): + deep = STACK_RESERVE - DEEP_RIDE_MARGIN_MIN + 1 + lines = [f"1.0 INFO stack high-water {deep} / {STACK_RESERVE} B (new peak)"] + self.assertEqual(stack_peaks(lines), [deep]) + self.assertIn("under the", margin_verdict(stack_peaks(lines))) + self.assertIsNone(margin_verdict([37_016]), "the pinned deep-ride peak still has its margin") + + def test_no_peak_reported_is_not_a_failure(self): + self.assertIsNone(margin_verdict([])) + + def test_a_boot_fault_or_a_watchdog_reset_ends_a_soak(self): + self.assertEqual(len(faults(["2.0 ERROR boot fault: MAP UNREADABLE", "3.0 INFO watchdog reset"])), 2) + self.assertEqual(faults([START, BANNER, MAP]), []) + + +if __name__ == "__main__": + unittest.main() From cf4061e6a5899da1b33d8550e6bf53b08f683b96 Mon Sep 17 00:00:00 2001 From: timohueser Date: Mon, 24 Aug 2026 13:18:49 +0200 Subject: [PATCH 2/4] Drive the soak with the flow the board actually plans MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Review found the soak driver could not pass on a healthy board, twice over. Scenarios A and B pressed through to the **Detour** menu, but the board has no detour half: it answers `DetourPlanned(Err(NoPath))` at the drain and never calls `nav_take_arena`, so `nav plan: start` is never logged and the transfer-named refusal is never reachable. Every plan now goes through the debug link's `N` line, which is a real `PlanRoute` — the one flow that arms the planner, claims the nav arm for the whole search and gives it back. Scenario B additionally requires the USB write-combining arm to have been granted before it asserts the refusal; without that the arena is free and the step tests nothing, so it says so rather than blaming the board. The banner was counted off `ui frame:`, which every non-map redraw shares — the menus, the station steps, the spinner — so one healthy cycle reported three banner repaints and the ordering check behind it never ran. The frozen-overlay repaint gets its own `freeze: banner repaint` line (debug-uart only; the harness is its only reader) and the driver keys on that. While there: the on-glass banner is not reachable by any gesture, because the only one that puts a map base under a running search also posts the cancellation the ride loop drains in the same pass. The module docs say so and the driver counts banners without requiring them, instead of asserting something no board can produce. The last place the board derived "a search is live" from `nav_run` — the wake cadence — now reads `App::core_mode()`, and three comments that described the deleted gate are corrected. Co-Authored-By: Claude Fable 5 --- firmware/obc-app/src/arena_gate.rs | 11 +- firmware/obc-app/src/device_core/core_mode.rs | 5 +- firmware/obc-app/src/ui_runtime.rs | 6 +- firmware/obc-fw-nrf54l/src/ble/state.rs | 2 +- firmware/obc-fw-nrf54l/src/main.rs | 7 +- firmware/obc-fw-nrf54l/src/ride.rs | 32 +- tools/s5_core_mode_soak.py | 335 +++++++++++------- tools/tests/test_s5_core_mode_soak.py | 83 +++-- 8 files changed, 305 insertions(+), 176 deletions(-) diff --git a/firmware/obc-app/src/arena_gate.rs b/firmware/obc-app/src/arena_gate.rs index 008364d4f..4307e33e3 100644 --- a/firmware/obc-app/src/arena_gate.rs +++ b/firmware/obc-app/src/arena_gate.rs @@ -19,9 +19,14 @@ //! | nav ⊥ usb | no route search while the cable owns upload scratch | [`TransferReady`] | //! //! A gate that is merely *documented* is a gate that gets skipped, so each precondition is a token -//! only [`CoreMode`](crate::device_core::core_mode::CoreMode) can mint: -//! [`claim_nav`](ArenaGate::claim_nav) cannot even be *called* without evidence that the map plane -//! is quiesced, and there is exactly one place that decides the token is owed. +//! [`CoreMode`](crate::device_core::core_mode::CoreMode) mints: [`claim_nav`](ArenaGate::claim_nav) +//! cannot even be *called* without evidence that the map plane is quiesced, and there is exactly one +//! place that decides the token is owed. +//! +//! How far that goes, precisely: the `mint` constructors are `pub(crate)`, not private, because this +//! module's own tests need them — so another `obc-app` module *could* assemble a proof without +//! asking `CoreMode`. Nothing does, and the point of the tightening is that doing so would be a +//! visible edit to a named constructor rather than a one-line re-derivation of the facts. //! //! # No atomics //! diff --git a/firmware/obc-app/src/device_core/core_mode.rs b/firmware/obc-app/src/device_core/core_mode.rs index f19f5a447..664e3ff9b 100644 --- a/firmware/obc-app/src/device_core/core_mode.rs +++ b/firmware/obc-app/src/device_core/core_mode.rs @@ -58,10 +58,9 @@ use crate::navigator::PlanFamily; /// /// The ranking decides only what the rider is **told**. It never decides admission: that reads the /// levels, because a search and a transfer exclude different things. -#[derive(Debug, Clone, Copy, PartialEq, Eq, Default)] +#[derive(Debug, Clone, Copy, PartialEq, Eq)] pub enum ModeState { /// Nothing heavy is holding the device. - #[default] Free, /// A planner run holds the nav arm. Searching, @@ -70,7 +69,7 @@ pub enum ModeState { } /// The four levels: two searches, one transfer, and the banner's level→edge bit. -#[derive(Debug, Default, PartialEq, Eq)] +#[derive(Debug, PartialEq, Eq)] pub(crate) struct CoreMode { /// A live [`Route`](PlanFamily::Route) planner run. route_search: bool, diff --git a/firmware/obc-app/src/ui_runtime.rs b/firmware/obc-app/src/ui_runtime.rs index ab28431b5..2769b554e 100644 --- a/firmware/obc-app/src/ui_runtime.rs +++ b/firmware/obc-app/src/ui_runtime.rs @@ -495,9 +495,9 @@ impl UiRuntime { self.stack.iter().any(|s| matches!(s, Screen::Passkey(_))) } - /// Whether the **map-transfer card** is on the stack (issue #927) — what - /// [`App::map_transfer_card_up`](crate::App::map_transfer_card_up) exposes to the board's - /// transfer gate. + /// Whether the **map-transfer card** is on the stack (issue #927) — the `render ⊥ usb` half of + /// [`App::usb_stage_precondition`](crate::App::usb_stage_precondition), reached through + /// [`App::map_transfer_card_up`](crate::App::map_transfer_card_up). pub(crate) fn map_transfer_card_up(&self) -> bool { self.stack.iter().any(|s| matches!(s, Screen::MapTransfer(_))) } diff --git a/firmware/obc-fw-nrf54l/src/ble/state.rs b/firmware/obc-fw-nrf54l/src/ble/state.rs index 5f74494ea..6f830ef47 100644 --- a/firmware/obc-fw-nrf54l/src/ble/state.rs +++ b/firmware/obc-fw-nrf54l/src/ble/state.rs @@ -4,7 +4,7 @@ //! lives entirely within the `ble` module tree, read/written across the four planes but never wider. //! //! Anything a *second transport* would also need — the command handler, descriptor classification, -//! the cross-transport one-transfer gate, the identity blobs — lives in [`crate::link`] instead. +//! the identity blobs — lives in [`crate::link`] instead. use core::cell::Cell; use core::sync::atomic::{AtomicBool, AtomicU8, Ordering}; diff --git a/firmware/obc-fw-nrf54l/src/main.rs b/firmware/obc-fw-nrf54l/src/main.rs index 3fbbacde9..d82589b12 100644 --- a/firmware/obc-fw-nrf54l/src/main.rs +++ b/firmware/obc-fw-nrf54l/src/main.rs @@ -111,9 +111,10 @@ mod ble; // not an option of it. Spawned beside the ride loop (see `spawn_usb_stack`). mod usb; // The transport-free companion-link core: the §4.4 command handler, descriptor classification, the -// cross-transport one-transfer gate, the identity blobs, and the one shared `ObjectStore`. Both the -// radio and the USB plane call into it, which is what keeps "USB is a second transport, not a second -// protocol" true in the code rather than only in the spec. +// identity blobs, and the one shared `ObjectStore`. Both the radio and the USB plane call into it, +// which is what keeps "USB is a second transport, not a second protocol" true in the code rather than +// only in the spec. (One transfer at a time is the flat engine's, scoped per wire by +// `Engine::on_link_up` / `on_link_lost`.) #[cfg(feature = "ble")] mod link; // The device object store: object ids / revision / upload state over the SD catalog, and the Config ↔ diff --git a/firmware/obc-fw-nrf54l/src/ride.rs b/firmware/obc-fw-nrf54l/src/ride.rs index 63ad1d255..f11ea63a4 100644 --- a/firmware/obc-fw-nrf54l/src/ride.rs +++ b/firmware/obc-fw-nrf54l/src/ride.rs @@ -1106,11 +1106,11 @@ pub(crate) async fn run_app( // router, so it answers the failure tier here instead of arming. // // Since #1146 P2 the slot lives in the scratch arena, so the search must - // *take* the arena first — and the gate's search arm before it, because a - // cable transfer streaming into the same store outranks a reroute. Either - // refusal answers the app immediately (the polite failure path): a plan whose - // spinner never resolves would now also hold the Recalculating freeze, i.e. a - // map that never redraws again. + // *take* the arena first — and a cable transfer streaming into the same store + // outranks a reroute, which `nav_take_arena` enforces by asking the arena who + // holds it. A refusal answers the app immediately (the polite failure path): + // a plan whose spinner never resolves would now also hold the Recalculating + // freeze, i.e. a map that never redraws again. #[cfg(has_nav)] match nav_take_arena(app, &mut nav_guard) { Ok(()) => { @@ -1529,9 +1529,9 @@ pub(crate) async fn run_app( let nav_cancel = host_pass.cancel_plan; #[cfg(has_nav)] { - // Whether this pass ended the search — the one place the arena's nav arm and the - // gate's search arm are given back. A flag rather than an inline release because the - // guard is borrowed by the step view below and must die first. + // Whether this pass ended the search — the one place the arena's nav arm is given + // back. A flag rather than an inline release because the guard is borrowed by the + // step view below and must die first. let mut search_ended = false; if host_pass.plan_armed { // The planner slot was already written from the request at the pass-top drain @@ -2240,6 +2240,13 @@ pub(crate) async fn run_app( app.render_overlay(&mut fbdev, FRAME_W as f32, FRAME_H as f32, color_fn); obc_render::RenderStats::default() }); + // Named apart from the `ui frame:` line every other non-map redraw shares: + // the menus, the station steps and the planning spinner all take this same + // branch, so a log reader (and the #1487 soak driver) cannot tell a banner + // repaint from a menu repaint without it. `debug-uart` only — the harness is + // its only reader and the shipping image should not carry the string. + #[cfg(feature = "debug-uart")] + defmt::info!("freeze: banner repaint rows {=u16}..{=u16}", y0, y0 + rows); Some(RenderedFrame { needs_map: false, stats, render_us }) } // Mid-freeze with no edge: nothing changed on either plane, so nothing to push. @@ -2533,10 +2540,11 @@ pub(crate) async fn run_app( // it stays fluid; otherwise arm the app's single next-wake deadline, or sleep indefinitely // until input/sensor. let charging = hold_p > 0.0 || display.hold_charging(); - #[cfg(has_nav)] - let planning = nav_run.is_some(); - #[cfg(not(has_nav))] - let planning = false; + // "A search is live" is the app's fact, never the board's run handle: `CoreMode` is set when + // the plan command drains and cleared by the answer, which brackets `nav_run` on both sides. + // It costs a hot loop rather than an exclusion if it is wrong, and it is the last place the + // board derived this a second way. + let planning = app.core_mode() == obc_app::device_core::ModeState::Searching; let animating = charging || planning || pending_map_redraw || overlay_dirty || overlay_span.is_some(); let next_ms = if animating { Some(LOOP_MS as u32) } else { app.ms_until_next_wake(now) }; // debug-uart host build: keep a ~2 Hz floor so streamed telemetry / `Z` zoom commands stay diff --git a/tools/s5_core_mode_soak.py b/tools/s5_core_mode_soak.py index f2cc010b6..bb06e4629 100644 --- a/tools/s5_core_mode_soak.py +++ b/tools/s5_core_mode_soak.py @@ -16,6 +16,33 @@ python3 tools/s5_core_mode_soak.py B --rtt-log /tmp/s5-rtt.log python3 tools/s5_core_mode_soak.py C --rtt-log /tmp/s5-rtt.log --minutes 60 +## Which flow the scenarios drive, and why it is `N` and not the Detour menu + +Every plan below is posted with the debug link's `N ` line +(`obc-platform/src/debug_link.rs`, consumed by `ride.rs`'s `debug_start_nav` arm), which is a real +`PlanRoute`. **The Detour menu cannot drive this soak**: the board has no detour half yet and answers +`DetourPlanned(Err(NoPath))` the moment the command drains (`ride.rs`'s `PlanDetour` arm), so +`nav_take_arena` is never called, `nav_begin` never runs, and neither `nav plan: start` nor any arena +claim ever happens. A detour-driven run reports failure on a perfectly healthy board. + +`N` is the one flow that actually arms the planner, claims the arena's nav arm for the whole search, +and gives it back — which is the `render ⊥ nav` cycle these soaks exist to stress. + +## What is *not* automatable here, stated rather than discovered + +**The banner's on-glass appearance is not reachable by any gesture.** The freeze needs a live search +*and* a map base, and on the board the only gesture that puts a map base back under a running search +— Back on the planning screen — also posts the cancellation, which the ride loop drains **in the same +pass**: gestures are taken at the top of the loop body and `drain_host_commands` runs below them, +both before the render. `obc-app`'s own `the_board_loop_renders_the_map_again_the_pass_a_cancel_lands` +pins that ordering, and `App::debug_set_plan_live` exists precisely because of it. + +So [`Cycle`] **counts** banner repaints and fails on more than one (a level repainting per pass is a +real regression), but does not require one. The banner's pixels are proven off-device by +`obc-sim --freeze --png`, and its legibility on the reflective panel is the human check #1487 already +flags. If a board detour half or a deferred drain ever makes the window real, the +`freeze: banner repaint` line is there and the ordering check picks it up. + ## The rig, and the two ways it lies to you * Build `--release --features debug-uart` — the sensors are swapped for the VCOM feed so a ride can @@ -23,13 +50,13 @@ silently ignored; `stty` + `printf` does not work, which is why this is pyserial at 115200 with `rtscts=False`. * **The J-Link CDC wedges silently**: `write()` succeeds, RTT keeps flowing, and nothing lands — a - blind script then "passes" every step. [`liveness_probe`] runs before every scenario and between - scenario A's cycles: snapshot the RTT log size, send six taps, wait, re-check. Zero growth means - wedged, and only a physical DK power-cycle clears it. + blind script then "passes" every step against a board that heard nothing. [`liveness_probe`] runs + before every scenario and between scenario A's cycles: snapshot the RTT log size, send six taps, + wait, re-check. Zero growth means wedged, and only a physical DK power-cycle clears it. * `nav plan: start` is a `defmt::debug!`, so the RTT shell needs `DEFMT_LOG=debug`. Without it every cycle reports a missing start line and the run is worthless. -Everything above `Link` is pure log/plan analysis with no pyserial in it, which is what +Everything above `Link` is pure log analysis with no pyserial in it, which is what `tools/tests/test_s5_core_mode_soak.py` drives against recorded RTT text. """ @@ -38,7 +65,6 @@ import argparse from dataclasses import dataclass, field import glob -import os from pathlib import Path import sys import time @@ -46,9 +72,13 @@ # ── the RTT vocabulary this soak reads (mirrors `firmware/obc-fw-nrf54l/src/ride.rs`) ──────────── PLAN_START = "nav plan: start" -MAP_FRAME = "map frame:" -UI_FRAME = "ui frame:" +PLAN_ANSWER = "nav route:" PLAN_REFUSED = "nav: cannot start a plan" +MAP_FRAME = "map frame:" +# The frozen-overlay repaint's **own** line. Deliberately not `ui frame:` — the menus, the station +# steps and the planning spinner all take that same non-map branch, so counting `ui frame:` as a +# banner reports three banners for one healthy cycle and masks the ordering check behind it. +BANNER = "freeze: banner repaint" USB_GRANTED = "arena: 64 KiB USB write-combining arm granted" USB_RECLAIMED = "arena: USB write-combining arm reclaimed" ARENA_REFUSED = "claim refused" @@ -61,17 +91,19 @@ REFUSAL_TRANSFER = "a cable transfer holds the store" REFUSAL_ARENA = "the scratch arena is busy" -# `deep_ride_margin_min` from `firmware/tools/resource_baseline.json` — scenario C fails if a -# reported stack peak eats into it. +# `stack_reserve` / `deep_ride_margin_min` from `firmware/tools/resource_baseline.json` — scenario C +# fails if a reported stack peak eats into the margin. STACK_RESERVE = 65_536 DEEP_RIDE_MARGIN_MIN = 8_704 @dataclass class Cycle: - """What one plan cycle produced, as read back out of the RTT log.""" + """What one `N` plan cycle produced, as read back out of the RTT log.""" started: bool = False + answered: bool = False + outcome: str = "" banner_frames: int = 0 map_frames: int = 0 arena_refusals: list[str] = field(default_factory=list) @@ -80,15 +112,19 @@ class Cycle: def verdict(self) -> str | None: """`None` when the cycle passed, else why it did not.""" if not self.started: + if self.refusals: + return f"the plan was refused: {self.refusals[0]}" return f"no `{PLAN_START}` line — the plan never armed (or DEFMT_LOG is not debug)" - if self.banner_frames == 0: - return "the freeze raised no banner frame — the rider saw a map that simply stopped" - if self.banner_frames > 1: - return f"{self.banner_frames} banner frames for one freeze — the edge is repainting per pass" - if self.map_frames != 1: - return f"{self.map_frames} full map repaints after the answer — expected exactly one catch-up" + if not self.answered: + return "the search never answered — a spinner that never resolves holds the nav arm forever" if self.arena_refusals: return f"the arena refused a claim: {'; '.join(self.arena_refusals)}" + if self.map_frames == 0: + # **The regression this whole soak exists for.** A refused claim degrades silently: the + # frame skips its map redraw and tries again, so the only witness is a map that stops. + return "no map frame after the answer — the arm came back but the map never caught up" + if self.banner_frames > 1: + return f"{self.banner_frames} banner repaints for one freeze — the edge is repainting per pass" return None @@ -99,9 +135,13 @@ def read_cycle(lines: list[str]) -> Cycle: for line in lines: if PLAN_START in line: cycle.started = True - elif UI_FRAME in line and cycle.started: + elif PLAN_ANSWER in line: + cycle.answered = True + tail = line.split(PLAN_ANSWER, 1)[1].split() + cycle.outcome = tail[0] if tail else "" + elif BANNER in line: cycle.banner_frames += 1 - elif MAP_FRAME in line and cycle.started: + elif MAP_FRAME in line and cycle.answered: cycle.map_frames += 1 elif ARENA_REFUSED in line or ARENA_RELEASE_REFUSED in line: cycle.arena_refusals.append(line.strip()) @@ -111,16 +151,21 @@ def read_cycle(lines: list[str]) -> Cycle: def assert_sequence(lines: list[str]) -> str | None: - """The order scenario A pins: start → banner → the catch-up repaint. A map frame *before* the - banner means the map plane drew while the nav arm was out, which is the whole regression.""" + """The order a cycle must walk: start → answer → the map catches up, with any banner repaint + strictly between the start and that catch-up. + + Counts alone pass a transcript where the map frame landed *first*, which is exactly the + regression: the map plane drawing while the nav arm is still out.""" order = [ kind for line in lines for kind in ( ["start"] if PLAN_START in line + else ["answer"] + if PLAN_ANSWER in line else ["banner"] - if UI_FRAME in line + if BANNER in line else ["map"] if MAP_FRAME in line else [] @@ -129,10 +174,16 @@ def assert_sequence(lines: list[str]) -> str | None: if "start" not in order: return "no plan start in this window" after = order[order.index("start") :] - if "banner" not in after: - return "no banner after the start" - if "map" in after and after.index("map") < after.index("banner"): - return "a full map repaint landed between the start and the banner — the freeze did not hold" + if "answer" not in after: + return "no plan answer after the start" + answer_at = after.index("answer") + if "map" in after[:answer_at]: + return "a full map repaint landed while the search still held the arm — the arena was not exclusive" + if "map" not in after[answer_at:]: + return "no map frame after the answer — the map did not catch up" + catch_up_at = answer_at + after[answer_at:].index("map") + if "banner" in after and after.index("banner") > catch_up_at: + return "a banner repaint after the catch-up — the freeze outlived its search" return None @@ -194,7 +245,18 @@ def since(self, mark: int) -> list[str]: fh.seek(mark) return fh.readlines() - # -- the gestures, in the debug-link vocabulary -- + def wait_for(self, mark: int, needle: str, timeout: float) -> bool: + """Poll the log until `needle` appears after `mark`, or give up. The plan phases run for + hundreds of ms to seconds, so every step waits on its own landmark rather than on a sleep + long enough to cover the worst case.""" + deadline = time.time() + timeout + while time.time() < deadline: + if any(needle in line for line in self.since(mark)): + return True + time.sleep(0.1) + return False + + # -- the gestures and commands, in the debug-link vocabulary -- def press(self) -> None: self.send("K s d") @@ -206,11 +268,6 @@ def back(self) -> None: time.sleep(0.05) self.send("K b u") - def back_hold(self, ms: int = 900) -> None: - self.send("K b d") - time.sleep(ms / 1000) - self.send("K b u") - def step(self, n: int) -> None: self.send(f"K t {n}") @@ -220,6 +277,10 @@ def fix(self, lat_ud: int, lon_ud: int) -> None: def zoom(self, mpp: float) -> None: self.send(f"Z {mpp}") + def plan(self, frm: tuple[int, int], to: tuple[int, int]) -> None: + """`N ` — **LON FIRST**, unlike the lat-first `F`.""" + self.send(f"N {frm[0]} {frm[1]} {to[0]} {to[1]}") + def liveness_probe(link: Link) -> None: """**Run this before trusting a single assertion.** The J-Link CDC wedges with `write()` still @@ -256,137 +317,163 @@ def stream_fixes(link: Link, base: tuple[int, int], steps: int, delay: float = 1 time.sleep(delay) -def scenario_a(link: Link, cycles: int, base: tuple[int, int]) -> int: - """**A — the freeze window over a map base (`render ⊥ nav`).** +def plan_cycle( + link: Link, frm: tuple[int, int], to: tuple[int, int], base: tuple[int, int] +) -> tuple[Cycle, list[str]]: + """One whole `N` plan: post it, wait for the arm, let it search under a live ride, wait for the + answer, then Back off the result screen so the map base is what catches up. - The only way a map base lands under a live search: back out of the planning spinner while the - planner is still running. Each cycle must show start → banner → answer → exactly one full - repaint, with no arena refusal anywhere.""" - print(f"A: {cycles} freeze cycles over a map base") + The Back is exactly one press: `land_route_plan` **replaces** the `NavPlanning` entry in place + (with `RouteOverview` on success, `NavFail` on either failure tier), so the stack is + `[…, Map, ]` and one Back leaves the Map on top.""" + mark = link.mark() + link.plan(frm, to) + if link.wait_for(mark, PLAN_START, timeout=4.0): + # A live ride under the search: fixes keep landing (a freeze pauses the map, never the ride) + # and the planner steps between frames. + stream_fixes(link, base, 3) + link.wait_for(mark, PLAN_ANSWER, timeout=20.0) + link.back() # off the result screen, back onto the map base + time.sleep(0.3) + stream_fixes(link, base, 3) + lines = link.since(mark) + return read_cycle(lines), lines + + +def report(prefix: str, cycle: Cycle, lines: list[str]) -> int: + """Print a cycle's verdict; return 1 when it failed. A failure prints its landmark tally, because + the usual cause is the key sequence drifting, not the firmware.""" + why = cycle.verdict() or assert_sequence(lines) + if not why: + return 0 + print(f" {prefix}: FAIL — {why}") + print( + f" landmarks: start={cycle.started} answer={cycle.outcome or '-'} " + f"banner={cycle.banner_frames} map={cycle.map_frames} " + f"arena_refusals={len(cycle.arena_refusals)} plan_refusals={len(cycle.refusals)}" + ) + return 1 + + +def scenario_a(link: Link, cycles: int, frm: tuple[int, int], to: tuple[int, int], base: tuple[int, int]) -> int: + """**A — the `render ⊥ nav` claim/release cycle**, ≥50 times. + + Each cycle must arm the planner, answer, give the arm back and let the map catch up, with zero + arena refusals in between. The failure it hunts is a map that stops redrawing — silent on a + shipping build, which is why it is only visible here.""" + print(f"A: {cycles} plan cycles (render ⊥ nav claim/release)") ride_to_map(link) stream_fixes(link, base, 3) failures = 0 + banners = 0 for i in range(cycles): if i % 10 == 0: liveness_probe(link) - mark = link.mark() - link.back_hold() # the ride menu - time.sleep(0.4) - link.step(1) # → Detour - time.sleep(0.2) - link.press() # the rejoin chooser - time.sleep(0.4) - link.press() # posts the plan and pushes the spinner - time.sleep(0.15) - link.back() # …and pop it *while the planner runs* — THE window - stream_fixes(link, (base[0] + i, base[1] + i), 3) - lines = link.since(mark) - cycle = read_cycle(lines) - why = cycle.verdict() or assert_sequence(lines) - if why: - failures += 1 - print(f" cycle {i}: FAIL — {why}") - elif i % 10 == 0: - print(f" cycle {i}: ok") - print(f"A: {cycles - failures}/{cycles} cycles passed") + cycle, lines = plan_cycle(link, frm, to, (base[0] + i, base[1] + i)) + banners += cycle.banner_frames + failed = report(f"cycle {i}", cycle, lines) + failures += failed + if i % 10 == 0 and not failed: + print(f" cycle {i}: ok ({cycle.outcome})") + print(f"A: {cycles - failures}/{cycles} cycles passed; {banners} banner repaints observed") + print(" (0 banner repaints is expected — see the module docs on why no gesture engages the freeze)") return failures -def scenario_b(link: Link) -> int: +def scenario_b(link: Link, frm: tuple[int, int], to: tuple[int, int]) -> int: """**B — `nav ⊥ usb` and `render ⊥ usb`.** Semi-automatic: a hand on the cable. - The plan offered during an upload must be refused *before* the planner arms, and the refusal - must name the transfer — not "the scratch arena is busy", and not a `NoPath`.""" + The plan offered during an upload must be refused *before* the planner arms, and the refusal must + name the transfer — not "the scratch arena is busy", and not a `NoPath`. + + **The precondition, and it is the whole basis of the claim:** the refusal is reachable only while + the USB **write-combining arm** is actually held, which the ride loop takes on + `usb::stage_requested()` and announces as `arena: 64 KiB USB write-combining arm granted`. Without + that grant the arena is free and the plan proceeds beside the upload exactly as it did before this + slice — so the step below checks for the grant first and says so rather than failing the board.""" print("B: plug the cable into J3, load a route, and start a map upload; press Enter when the") print(" transfer card is up.") input() mark = link.mark() - link.back_hold() - time.sleep(0.4) - link.step(1) - time.sleep(0.2) - link.press() - time.sleep(0.4) - link.press() - time.sleep(1.0) + if not link.wait_for(mark, USB_GRANTED, timeout=10.0): + print(" SKIP — the USB write-combining arm was never granted, so the arena is free and this") + print(" step tests nothing. Re-run with an upload large enough to request it.") + return 0 + + mark = link.mark() + link.plan(frm, to) + time.sleep(2.0) lines = link.since(mark) - refusals = [line for line in lines if PLAN_REFUSED in line] + refusals = [line.strip() for line in lines if PLAN_REFUSED in line] failures = 0 - if not refusals: - print(" FAIL — the plan was not refused during the upload") + if any(PLAN_START in line for line in lines): + print(" FAIL — the planner armed during the upload; `nav ⊥ usb` did not hold") failures += 1 - elif not any(REFUSAL_TRANSFER in line for line in refusals): - print(f" FAIL — refused, but not by name: {refusals[0].strip()}") + elif not refusals: + print(" FAIL — the plan was neither armed nor refused") failures += 1 elif any(REFUSAL_ARENA in line for line in refusals): - print(" FAIL — the rider was told the arena is busy; the cable is the actionable fact") + print(f" FAIL — the rider was told the arena is busy; the cable is the actionable fact: {refusals[0]}") + failures += 1 + elif not any(REFUSAL_TRANSFER in line for line in refusals): + print(f" FAIL — refused, but not by name: {refusals[0]}") failures += 1 else: - print(" refusal names the transfer: ok") + print(" refused before the planner armed, and the refusal names the transfer: ok") print("B: end the upload, then press Enter.") input() mark = link.mark() - link.back_hold() - time.sleep(0.4) - link.step(1) - time.sleep(0.2) - link.press() - time.sleep(0.4) - link.press() - time.sleep(1.0) - lines = link.since(mark) - if any(PLAN_REFUSED in line for line in lines): - print(" FAIL — the same input is still refused after the upload ended") + link.plan(frm, to) + if not link.wait_for(mark, PLAN_START, timeout=5.0): + print(" FAIL — no plan armed after the upload ended") failures += 1 - elif not any(PLAN_START in line for line in lines): - print(" FAIL — no plan started after the upload ended") + elif any(PLAN_REFUSED in line for line in link.since(mark)): + print(" FAIL — the same input is still refused after the upload ended") failures += 1 else: print(" the plan arms normally afterwards: ok") + link.wait_for(mark, PLAN_ANSWER, timeout=20.0) + link.back() - grants = sum(1 for line in lines if USB_GRANTED in line) - reclaims = sum(1 for line in lines if USB_RECLAIMED in line) - print(f" arena arm: {grants} granted / {reclaims} reclaimed (expect one each per upload)") + whole = link.since(0) + granted = sum(USB_GRANTED in line for line in whole) + reclaimed = sum(USB_RECLAIMED in line for line in whole) + print(f" arena arm: {granted} granted / {reclaimed} reclaimed (expect one each per upload)") return failures -def scenario_c(link: Link, minutes: int, base: tuple[int, int]) -> int: - """**C — the stuck-freeze soak.** A continuous ride with a plan cycle every ~60 s and a periodic - zoom nudge. Every freeze release must be followed by a map render within two wakes, and the - stack must never eat into `deep_ride_margin_min`.""" - print(f"C: {minutes} minutes of continuous riding with a plan cycle every 60 s") +def scenario_c(link: Link, minutes: int, frm: tuple[int, int], to: tuple[int, int], base: tuple[int, int]) -> int: + """**C — the stuck-arm soak.** A continuous ride with a plan cycle every ~60 s and a periodic + zoom nudge. Every released nav arm must be followed by a map render, and the stack must never eat + into `deep_ride_margin_min`.""" + print(f"C: {minutes} minutes of continuous riding with a plan cycle every ~60 s") ride_to_map(link) deadline = time.time() + minutes * 60 failures = 0 - cycle_no = 0 + n = 0 while time.time() < deadline: mark = link.mark() - link.zoom(30.0 if cycle_no % 2 else 20.0) - stream_fixes(link, (base[0] + cycle_no * 10, base[1]), 25) - link.back_hold() - time.sleep(0.4) - link.step(1) - time.sleep(0.2) - link.press() - time.sleep(0.4) - link.press() - time.sleep(0.15) - link.back() - stream_fixes(link, (base[0] + cycle_no * 10, base[1]), 20) - lines = link.since(mark) - why = read_cycle(lines).verdict() - fault_lines = faults(lines) - margin = margin_verdict(stack_peaks(lines)) - for problem in [why, margin] + fault_lines: + link.zoom(30.0 if n % 2 else 20.0) + stream_fixes(link, (base[0] + n * 10, base[1]), 25) + cycle, lines = plan_cycle(link, frm, to, (base[0] + n * 10, base[1])) + failures += report(f"cycle {n}", cycle, lines) + window = link.since(mark) + for problem in [margin_verdict(stack_peaks(window))] + faults(window): if problem: failures += 1 - print(f" cycle {cycle_no}: FAIL — {problem}") - cycle_no += 1 - print(f"C: {cycle_no} cycles over {minutes} min, {failures} failures") + print(f" cycle {n}: FAIL — {problem}") + n += 1 + print(f"C: {n} cycles over {minutes} min, {failures} failures") return failures +def coord(raw: str) -> tuple[int, int]: + """`LON,LAT` in integer microdegrees — the `N` line's own order.""" + lon, lat = raw.split(",") + return int(lon), int(lat) + + def resolve_port(explicit: str | None) -> str: if explicit: return explicit @@ -403,8 +490,12 @@ def main() -> int: parser.add_argument("--rtt-log", required=True, type=Path, help="the file `cargo rtt` is tee'd into") parser.add_argument("--cycles", type=int, default=50, help="scenario A plan cycles (>=50 is the gate)") parser.add_argument("--minutes", type=int, default=60, help="scenario C duration (60 is the gate)") - parser.add_argument("--lat", type=int, default=47_990_000, help="starting fix latitude, microdegrees") - parser.add_argument("--lon", type=int, default=7_850_000, help="starting fix longitude, microdegrees") + # Grimsel defaults, on the map the fixture registry ships. Both ends must lie on the mounted + # map's routing graph or every cycle answers `no-path` — which the run reports as its outcome. + parser.add_argument("--nav-from", type=coord, default=(8_337_000, 46_562_000), help="LON,LAT µdeg") + parser.add_argument("--nav-to", type=coord, default=(8_248_000, 46_570_000), help="LON,LAT µdeg") + parser.add_argument("--lat", type=int, default=46_562_000, help="streamed fix latitude, µdeg") + parser.add_argument("--lon", type=int, default=8_337_000, help="streamed fix longitude, µdeg") args = parser.parse_args() if not args.rtt_log.exists(): @@ -414,11 +505,11 @@ def main() -> int: liveness_probe(link) base = (args.lat, args.lon) if args.scenario == "A": - failures = scenario_a(link, args.cycles, base) + failures = scenario_a(link, args.cycles, args.nav_from, args.nav_to, base) elif args.scenario == "B": - failures = scenario_b(link) + failures = scenario_b(link, args.nav_from, args.nav_to) else: - failures = scenario_c(link, args.minutes, base) + failures = scenario_c(link, args.minutes, args.nav_from, args.nav_to, base) print("PASS" if failures == 0 else f"FAIL ({failures})") return 0 if failures == 0 else 1 diff --git a/tools/tests/test_s5_core_mode_soak.py b/tools/tests/test_s5_core_mode_soak.py index 3a189d756..a6c994588 100644 --- a/tools/tests/test_s5_core_mode_soak.py +++ b/tools/tests/test_s5_core_mode_soak.py @@ -2,8 +2,13 @@ **Death trigger: delete with `tools/s5_core_mode_soak.py` when #1487 closes.** The script's whole value is that a blind driver "passes" everything — a wedged VCOM, a `DEFMT_LOG` that swallows the -plan-start line, a map frame that lands *before* the banner. These pin the verdicts that catch each -of those, off recorded lines, so the rig is not itself the thing under test on the board. +plan-start line, a map frame that lands while the nav arm is still out. These pin the verdicts that +catch each of those, off recorded lines, so the rig is not itself the thing under test on the board. + +Every transcript below is **realistic**: it carries the `ui frame:` lines a real cycle emits for the +planning spinner and the menus. An earlier revision keyed the banner on `ui frame:` and so reported +three banner repaints for a healthy cycle; the fixtures are noisy on purpose so that cannot come +back. """ import unittest @@ -19,47 +24,67 @@ ) START = "0.100 DEBUG nav plan: start planner=0x2000a000 scratch=0x2000b000 tiles=0x2000c000" -BANNER = "0.150 INFO ui frame: render 900 us + push 300 us (screen redraw, no map)" +# The spinner and the menus take the same non-map render branch as the banner and share this line. +SPINNER = "0.150 INFO ui frame: render 900 us + push 300 us (screen redraw, no map)" +BANNER = "0.200 INFO freeze: banner repaint rows 96..132" +ANSWER = "0.800 INFO nav route: ok len=4210 total_ms=690 snap_ms=12 search_ms=540 emit_ms=90" MAP = "0.900 INFO map frame: render 41000 us + push 3000 us | lod 2 | feat 900/1200 | chunks 8" BUSY = "0.400 ERROR arena: render claim refused — held by Nav" +REFUSED = "0.120 WARN nav: cannot start a plan (a cable transfer holds the store) — answering the failure tier" + +# What a healthy `N` cycle actually looks like: the spinner repaints several times while the planner +# steps, and no banner appears at all (no gesture engages the freeze on today's board). +HEALTHY = [START, SPINNER, SPINNER, SPINNER, ANSWER, SPINNER, MAP] class CycleVerdicts(unittest.TestCase): - def test_a_clean_cycle_passes(self): - self.assertIsNone(read_cycle([START, BANNER, MAP]).verdict()) - self.assertIsNone(assert_sequence([START, BANNER, MAP])) + def test_a_healthy_cycle_passes_with_its_spinner_repaints(self): + """**The regression in the rig itself.** Three `ui frame:` lines are what a real cycle emits; + counting them as banners failed every healthy cycle and hid the ordering check behind it.""" + cycle = read_cycle(HEALTHY) + self.assertEqual(cycle.banner_frames, 0) + self.assertEqual(cycle.outcome, "ok") + self.assertIsNone(cycle.verdict()) + self.assertIsNone(assert_sequence(HEALTHY)) def test_a_missing_plan_start_is_the_defmt_level_trap(self): """No `nav plan: start` means either the plan never armed or RTT is not at debug — and a driver that ignored it would report a clean run against a board that planned nothing.""" - why = read_cycle([BANNER, MAP]).verdict() - self.assertIn("never armed", why) + self.assertIn("never armed", read_cycle([SPINNER, ANSWER, MAP]).verdict()) - def test_a_freeze_with_no_banner_is_a_map_that_simply_stopped(self): - why = read_cycle([START, MAP]).verdict() - self.assertIn("no banner", why) + def test_a_refused_plan_is_reported_as_the_refusal_not_as_a_missing_start(self): + why = read_cycle([REFUSED]).verdict() + self.assertIn("refused", why) + self.assertIn("cable transfer", why) - def test_the_banner_is_one_repaint_per_freeze_not_one_per_pass(self): - """The level→edge converter's whole point. Hundreds of ride-loop passes, one overlay - repaint.""" - why = read_cycle([START, BANNER, BANNER, MAP]).verdict() - self.assertIn("repainting per pass", why) + def test_a_search_that_never_answers_holds_the_arm_forever(self): + self.assertIn("never answered", read_cycle([START, SPINNER]).verdict()) - def test_exactly_one_catch_up_repaint_after_the_answer(self): - self.assertIn("0 full map repaints", read_cycle([START, BANNER]).verdict()) - self.assertIn("2 full map repaints", read_cycle([START, BANNER, MAP, MAP]).verdict()) + def test_no_map_frame_after_the_answer_is_the_map_that_stopped(self): + """**The failure this soak exists for**: the arm came back and nothing redrew.""" + self.assertIn("never caught up", read_cycle([START, SPINNER, ANSWER]).verdict()) def test_an_arena_refusal_fails_the_cycle_however_it_ends(self): - """**The failure this soak exists for**: a refused claim degrades silently on a shipping - build, so the log line is the only witness.""" - why = read_cycle([START, BANNER, BUSY, MAP]).verdict() - self.assertIn("arena refused", why) + """A refused claim degrades silently on a shipping build, so the log line is the only + witness.""" + self.assertIn("arena refused", read_cycle([START, BUSY, ANSWER, MAP]).verdict()) + + def test_the_banner_is_one_repaint_per_freeze_not_one_per_pass(self): + """The level→edge converter's whole point. Hundreds of ride-loop passes, one repaint — so a + banner that *is* observed must be observed once.""" + self.assertIsNone(read_cycle([START, BANNER, ANSWER, MAP]).verdict()) + self.assertIn("repainting per pass", read_cycle([START, BANNER, BANNER, ANSWER, MAP]).verdict()) + + def test_a_map_frame_while_the_arm_is_out_means_the_arena_was_not_exclusive(self): + """Counts alone pass this — a start, an answer, and a catch-up repaint after it, all + present. The *order* is what says a second map frame drew while the search still held the + arm, which is the `render ⊥ nav` violation the soak is for.""" + torn = [START, SPINNER, MAP, ANSWER, MAP] + self.assertIsNone(read_cycle(torn).verdict(), "counts see nothing wrong") + self.assertIn("not exclusive", assert_sequence(torn)) - def test_a_map_frame_before_the_banner_means_the_freeze_did_not_hold(self): - """Counts alone would pass this: one start, one banner, one map frame. The *order* is what - says the map plane drew while the nav arm was still out.""" - self.assertIsNone(read_cycle([START, MAP, BANNER]).verdict()) - self.assertIn("freeze did not hold", assert_sequence([START, MAP, BANNER])) + def test_a_banner_after_the_catch_up_means_the_freeze_outlived_its_search(self): + self.assertIn("outlived", assert_sequence([START, ANSWER, MAP, BANNER])) class StackAndFaults(unittest.TestCase): @@ -75,7 +100,7 @@ def test_no_peak_reported_is_not_a_failure(self): def test_a_boot_fault_or_a_watchdog_reset_ends_a_soak(self): self.assertEqual(len(faults(["2.0 ERROR boot fault: MAP UNREADABLE", "3.0 INFO watchdog reset"])), 2) - self.assertEqual(faults([START, BANNER, MAP]), []) + self.assertEqual(faults(HEALTHY), []) if __name__ == "__main__": From 79f6b689aa2e75d15c41725d9e84b9e8192db66e Mon Sep 17 00:00:00 2001 From: timohueser Date: Mon, 24 Aug 2026 13:20:20 +0200 Subject: [PATCH 3/4] Prove the liveness probe against the board, not against the log size MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit RTT keeps flowing from sensors and frames while VCOM input is wedged, so a probe that only watches the log grow passes against a board that heard nothing — the exact failure it exists to catch. It now requires the board's own `input: Step` acknowledgements: none is a wedge, fewer than six is a lossy cable and says so without sending anyone to the power switch. Co-Authored-By: Claude Fable 5 --- tools/s5_core_mode_soak.py | 30 +++++++++++++++++++++------ tools/tests/test_s5_core_mode_soak.py | 16 ++++++++++++++ 2 files changed, 40 insertions(+), 6 deletions(-) diff --git a/tools/s5_core_mode_soak.py b/tools/s5_core_mode_soak.py index bb06e4629..83b346844 100644 --- a/tools/s5_core_mode_soak.py +++ b/tools/s5_core_mode_soak.py @@ -51,8 +51,10 @@ `rtscts=False`. * **The J-Link CDC wedges silently**: `write()` succeeds, RTT keeps flowing, and nothing lands — a blind script then "passes" every step against a board that heard nothing. [`liveness_probe`] runs - before every scenario and between scenario A's cycles: snapshot the RTT log size, send six taps, - wait, re-check. Zero growth means wedged, and only a physical DK power-cycle clears it. + before every scenario and between scenario A's cycles: send six taps and require the board's own + `input: Step` acknowledgements back. A *grown log* is not enough — sensors and frames keep logging + right through a wedge. Zero acknowledgements means wedged, and only a physical DK power-cycle + clears it. * `nav plan: start` is a `defmt::debug!`, so the RTT shell needs `DEFMT_LOG=debug`. Without it every cycle reports a missing start line and the run is worthless. @@ -85,6 +87,10 @@ ARENA_RELEASE_REFUSED = "release refused" STACK_PEAK = "stack high-water" BOOT_FAULT = "boot fault" +# The board's own acknowledgement of an injected selection step (`ride.rs`'s input log). The liveness +# probe requires *this*, not merely a log that grew: RTT keeps flowing from sensors and frames while +# VCOM input is wedged, so growth alone passes a probe against a board that heard nothing. +STEP_ACK = "input: Step" # The refusal string `nav_take_arena` answers a live cable transfer with. Scenario B's whole point: # the rider must be told about the cable, not about "the scratch arena". @@ -211,6 +217,11 @@ def margin_verdict(peaks: list[int]) -> str | None: return None +def step_acks(lines: list[str]) -> int: + """How many injected selection steps the board acknowledged in this window.""" + return sum(STEP_ACK in line for line in lines) + + def faults(lines: list[str]) -> list[str]: """Boot faults and WDT resets seen in the window — either one ends a soak.""" return [line.strip() for line in lines if BOOT_FAULT in line.lower() or "watchdog" in line.lower()] @@ -285,18 +296,25 @@ def plan(self, frm: tuple[int, int], to: tuple[int, int]) -> None: def liveness_probe(link: Link) -> None: """**Run this before trusting a single assertion.** The J-Link CDC wedges with `write()` still succeeding and RTT still flowing, and a blind script then passes every step against a board that - heard nothing. Six taps must move the RTT log; zero growth is a wedge, and only a physical DK - power-cycle clears it.""" + heard nothing. + + Six taps must come back as the board's own `input: Step` acknowledgements. A grown log is *not* + enough — sensors and frames keep logging through a wedge. Zero acknowledgements is a wedge, and + only a physical DK power-cycle clears it; fewer than six is a lossy cable, worth saying out loud + but not worth sending someone to the power switch.""" mark = link.mark() for _ in range(6): link.step(1) time.sleep(0.1) time.sleep(2.0) - if link.mark() == mark: + acks = step_acks(link.since(mark)) + if acks == 0: raise SystemExit( - "VCOM is wedged: six injected taps produced no RTT output at all.\n" + "VCOM is wedged: six injected taps produced no `input: Step` acknowledgement.\n" "Power-cycle the DK physically (a re-flash does not clear it) and start again." ) + if acks < 6: + print(f" liveness: only {acks}/6 taps acknowledged — the cable is lossy, results may be noisy") # ── the scenarios ──────────────────────────────────────────────────────────────────────────────── diff --git a/tools/tests/test_s5_core_mode_soak.py b/tools/tests/test_s5_core_mode_soak.py index a6c994588..9a455d303 100644 --- a/tools/tests/test_s5_core_mode_soak.py +++ b/tools/tests/test_s5_core_mode_soak.py @@ -21,6 +21,7 @@ margin_verdict, read_cycle, stack_peaks, + step_acks, ) START = "0.100 DEBUG nav plan: start planner=0x2000a000 scratch=0x2000b000 tiles=0x2000c000" @@ -30,6 +31,10 @@ ANSWER = "0.800 INFO nav route: ok len=4210 total_ms=690 snap_ms=12 search_ms=540 emit_ms=90" MAP = "0.900 INFO map frame: render 41000 us + push 3000 us | lod 2 | feat 900/1200 | chunks 8" BUSY = "0.400 ERROR arena: render claim refused — held by Nav" +STEP = "0.050 INFO input: Step 1 on Map" +# What a wedged VCOM looks like: RTT keeps flowing from sensors and frames, so the log grows while +# not one injected tap has landed. +WEDGED = [MAP, "0.3 INFO gps: fix 46562000 8337000", SPINNER] REFUSED = "0.120 WARN nav: cannot start a plan (a cable transfer holds the store) — answering the failure tier" # What a healthy `N` cycle actually looks like: the spinner repaints several times while the planner @@ -87,6 +92,17 @@ def test_a_banner_after_the_catch_up_means_the_freeze_outlived_its_search(self): self.assertIn("outlived", assert_sequence([START, ANSWER, MAP, BANNER])) +class Liveness(unittest.TestCase): + def test_a_wedged_vcom_still_grows_the_log(self): + """**The trap the probe exists for.** Counting bytes passes here; counting the board's own + acknowledgements does not.""" + self.assertEqual(step_acks(WEDGED), 0) + + def test_acknowledgements_are_counted_not_merely_detected(self): + """A lossy cable is worth reporting and is not a wedge, so the probe needs the count.""" + self.assertEqual(step_acks([STEP, MAP, STEP, STEP]), 3) + + class StackAndFaults(unittest.TestCase): def test_peaks_are_read_and_the_margin_floor_is_enforced(self): deep = STACK_RESERVE - DEEP_RIDE_MARGIN_MIN + 1 From 2745acce108ad21c8118032712fdcb32e29edb85 Mon Sep 17 00:00:00 2001 From: timohueser Date: Mon, 24 Aug 2026 13:32:59 +0200 Subject: [PATCH 4/4] End the freeze at the answer, and take the soak's marks before the operator MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Two ways the driver still reported a healthy board as broken, or a broken one as healthy. The order check let a banner repaint sit between `nav route:` and the catch-up frame. The answer is where the freeze ends, not the catch-up: `nav_finish` logs the line and hands the app the answer in the same pass, `note_answer` clears the search level there, and the render decision comes after both. A banner at or past the answer is a stuck freeze caught one pass earlier, so it is rejected. Scenario B took both of its marks after an `input()` prompt, and both USB arena transitions are edges the board logs once, in the same pass as the card that accompanies them — the operator is slower than a pass, so the window started past the very line it was waiting for and a healthy upload reported SKIP. The marks now precede the prompts, and the second half waits for the arm to be reclaimed before planning: without that the next plan races a guard still held and reports a refusal that is the rig's fault. An arm that never comes back is the stuck-USB mirror of the bug this soak hunts, so it fails rather than hangs. Co-Authored-By: Claude Fable 5 --- tools/s5_core_mode_soak.py | 49 ++++++++++++++++++--------- tools/tests/test_s5_core_mode_soak.py | 8 ++++- 2 files changed, 40 insertions(+), 17 deletions(-) diff --git a/tools/s5_core_mode_soak.py b/tools/s5_core_mode_soak.py index 83b346844..2a8421114 100644 --- a/tools/s5_core_mode_soak.py +++ b/tools/s5_core_mode_soak.py @@ -158,9 +158,14 @@ def read_cycle(lines: list[str]) -> Cycle: def assert_sequence(lines: list[str]) -> str | None: """The order a cycle must walk: start → answer → the map catches up, with any banner repaint - strictly between the start and that catch-up. + strictly **between the start and the answer**. - Counts alone pass a transcript where the map frame landed *first*, which is exactly the + The answer is where the freeze ends, not the catch-up: `nav_finish` logs `nav route:` and hands + the app the answer in the same pass, `note_answer` clears the search level there, and the render + decision comes after both. So a banner repaint anywhere at or past the answer says the level + outlived the run that owned it — which is the stuck freeze, one pass early. + + Counts alone pass a transcript where a map frame landed *before* the answer, which is the other regression: the map plane drawing while the nav arm is still out.""" order = [ kind @@ -187,9 +192,8 @@ def assert_sequence(lines: list[str]) -> str | None: return "a full map repaint landed while the search still held the arm — the arena was not exclusive" if "map" not in after[answer_at:]: return "no map frame after the answer — the map did not catch up" - catch_up_at = answer_at + after[answer_at:].index("map") - if "banner" in after and after.index("banner") > catch_up_at: - return "a banner repaint after the catch-up — the freeze outlived its search" + if "banner" in after[answer_at:]: + return "a banner repaint at or after the answer — the freeze outlived its search" return None @@ -409,10 +413,14 @@ def scenario_b(link: Link, frm: tuple[int, int], to: tuple[int, int]) -> int: `usb::stage_requested()` and announces as `arena: 64 KiB USB write-combining arm granted`. Without that grant the arena is free and the plan proceeds beside the upload exactly as it did before this slice — so the step below checks for the grant first and says so rather than failing the board.""" + # Every mark around an `input()` is taken **before** the prompt. Both arena transitions are + # edges the board logs once, in the same pass as the card they accompany — and the operator is + # slower than a pass, so a mark taken after they press Enter starts the window past the very + # line it is waiting for. That is a healthy board reported as a SKIP (or as a false refusal). + mark = link.mark() print("B: plug the cable into J3, load a route, and start a map upload; press Enter when the") print(" transfer card is up.") input() - mark = link.mark() if not link.wait_for(mark, USB_GRANTED, timeout=10.0): print(" SKIP — the USB write-combining arm was never granted, so the arena is free and this") print(" step tests nothing. Re-run with an upload large enough to request it.") @@ -439,20 +447,29 @@ def scenario_b(link: Link, frm: tuple[int, int], to: tuple[int, int]) -> int: else: print(" refused before the planner armed, and the refusal names the transfer: ok") + reclaim_mark = link.mark() print("B: end the upload, then press Enter.") input() - mark = link.mark() - link.plan(frm, to) - if not link.wait_for(mark, PLAN_START, timeout=5.0): - print(" FAIL — no plan armed after the upload ended") - failures += 1 - elif any(PLAN_REFUSED in line for line in link.since(mark)): - print(" FAIL — the same input is still refused after the upload ended") + # The arm has to be *given back* before the plan can be expected to arm. Without this wait the + # next `N` races a guard that is still held, and the run reports a false refusal — the same + # mistake in the other direction. An arm that never comes back is the stuck-USB mirror of the + # stuck-nav-arm bug this whole soak hunts, so it fails rather than waiting forever. + if not link.wait_for(reclaim_mark, USB_RECLAIMED, timeout=10.0): + print(" FAIL — the USB write-combining arm was never reclaimed after the upload ended") failures += 1 else: - print(" the plan arms normally afterwards: ok") - link.wait_for(mark, PLAN_ANSWER, timeout=20.0) - link.back() + mark = link.mark() + link.plan(frm, to) + if not link.wait_for(mark, PLAN_START, timeout=5.0): + print(" FAIL — no plan armed after the upload ended") + failures += 1 + elif any(PLAN_REFUSED in line for line in link.since(mark)): + print(" FAIL — the same input is still refused after the upload ended") + failures += 1 + else: + print(" the plan arms normally afterwards: ok") + link.wait_for(mark, PLAN_ANSWER, timeout=20.0) + link.back() whole = link.since(0) granted = sum(USB_GRANTED in line for line in whole) diff --git a/tools/tests/test_s5_core_mode_soak.py b/tools/tests/test_s5_core_mode_soak.py index 9a455d303..0dc5d2f5c 100644 --- a/tools/tests/test_s5_core_mode_soak.py +++ b/tools/tests/test_s5_core_mode_soak.py @@ -88,8 +88,14 @@ def test_a_map_frame_while_the_arm_is_out_means_the_arena_was_not_exclusive(self self.assertIsNone(read_cycle(torn).verdict(), "counts see nothing wrong") self.assertIn("not exclusive", assert_sequence(torn)) - def test_a_banner_after_the_catch_up_means_the_freeze_outlived_its_search(self): + def test_a_banner_at_or_after_the_answer_means_the_freeze_outlived_its_search(self): + """The answer is where the freeze ends, not the catch-up: `nav route:` and `note_answer` + land in the same pass and the render decision comes after both. So the banner between the + answer and the catch-up repaint is a stuck freeze caught one pass earlier, not a healthy + frame — an earlier revision let exactly that transcript through.""" + self.assertIn("outlived", assert_sequence([START, ANSWER, BANNER, MAP])) self.assertIn("outlived", assert_sequence([START, ANSWER, MAP, BANNER])) + self.assertIsNone(assert_sequence([START, BANNER, ANSWER, MAP]), "…and before it is the freeze") class Liveness(unittest.TestCase):