diff --git a/.claude/skills/verify-failover/SKILL.md b/.claude/skills/verify-failover/SKILL.md new file mode 100644 index 0000000000..f83159c7cb --- /dev/null +++ b/.claude/skills/verify-failover/SKILL.md @@ -0,0 +1,63 @@ +--- +name: verify-failover +description: Model-check failover along a chain of relays (`rs/moq-net/verify/failover/FailoverChain.tla`) with TLA+. Use when a change touches how a relay's front switches routes or ends a track (`model/front.rs` `track_ended`, `model/origin.rs` `Action::Finish`, `park`), how a switch asks the new copy (`model/resume.rs` `Reader::sync`, `backfill_gaps`, `Producer::subscription`), how a group continues on another copy mid-read (`Recover`, `Fetching`), or when a failover bug spans more than one hop and needs every ordering of deaths, switches, and frames checked rather than a random sweep. +--- + +# Verify failover along a relay chain + +`rs/moq-net/verify/failover/FailoverChain.tla` models one track served to a client `C` through relay `E`, which starts on relay `A` and may fail over to relay `B`; both pull from the origin `O`, and with `Mesh` `B` may also route through `A`. Each layer is abstracted to the steps its own model checked, so the state stays small: a route change is one `Switch` (`verify-route`), a switch asks the new copy from where the readers got to and each reader hands a group out once and ends once nothing it replaced may still deliver (`verify-resume`), and a group handed out crosses a hop unless its session dies (`verify-subscribe`, with an hour's budget). What the chain adds is frames: a group whose copy fails or stalls mid-read continues on another copy at the same frame (`Recover`), from a copy its relay holds, from the serving copy, or by fetching the rest from the serving route, which asks its own upstream in turn. + +## Rules + +Each rule is an INVARIANT, except `Settles`, which is TLC's deadlock check: every path must end with the read over (`Finished`); the harm says why it matters. + +| Rule | Holds when | Harm if broken | +| --- | --- | --- | +| `CleanEndIsComplete` | The client's track ends cleanly only with every group handed out. | The viewer loses media silently at the end. | +| `CleanEndIsDeclared` | The client's track ends cleanly only after the origin ended it. | A failover reads as the broadcast ending. | +| `NoSkipWhileHeld` | A group the client started fails only once `E` has no route left. | A group is cut short while another path holds the rest. | +| `SettledIsWhole` | A finished read holds every frame of every group. | A group ends short of its last frame. | +| `Settles` (deadlock) | Every path ends with the read over, or, once the client left, with no relay holding a copy. | Playback hangs, or a relay keeps its upstream subscribed after the viewer left. | + +## Run + +```sh +just rs tla moq-net/verify/failover/FailoverChain.tla +just rs tla moq-net/verify/failover/FailoverChain.tla -config rs/moq-net/verify/failover/Leave.cfg +just rs tla moq-net/verify/failover/FailoverChain.tla -config rs/moq-net/verify/failover/EndedRelay.cfg +``` + +The first checks every rule with `E` failing over between `A` and `B`, one death, and one switch per relay, with a client that stays, so a deadlock is a playback hang: about 2.0M states. The second lets the client leave at any point, so a deadlock is a relay still holding a copy after it left; leaving is always possible there, which is why it cannot stand in for the first: about 2.2M states. Each takes under 30 seconds on 24 cores and passes at the sync commit. The third adds `B`'s route through `A`, so the route also moves at the middle hop: it fails at the sync commit on the open finding below at depth 31, after about 50M distinct states and 11 minutes on 8 workers. + +## Open finding: an ended relay cannot move a fetch off a dying route + +`EndedRelay.cfg` breaks `NoSkipWhileHeld`. `E` reads group 0 through `A` and hands out group 1, then switches to `B`, asking it from group 1, and fetches the rest of group 0 from `B`. `B` moves its route to `A`, its copy from group 1 completes, and its track ends (`Action::Finish`); then `A` dies. `B`'s front no longer switches, so its fetch for group 0 fails although `B` still reaches `O` directly (`Fetching` returns the dead copy's error once `route.end()` is set), and `E`, whose serving route gave up on the group, cuts it short. The real stack breaks the same rule earlier, on the first code finding below, so this path has no replay of its own yet; once that is fixed, replay it in `failover_chain.rs` and pin or fix it. Once both are fixed, merge `EndedRelay.cfg`'s `Mesh` into `FailoverChain.cfg` if the bounds allow, and delete `EndedRelay.cfg`. + +## Open findings: the code falls short of the model + +The model lets a fetch reach the serving route whenever that route lives, after the track ended too. Replaying its paths in `rs/moq-net/tests/integration/failover_chain.rs` found two places where the code does not, each pinned as a `residual_*` test that passes while the bug stands; `a_half_read_group_continues_through_the_new_route` is the same path without the end, which passes. Once one is fixed, flip its test. + +- `residual_ending_the_track_fails_a_fetch_in_flight`: `E`'s fetch of the rest of a group is in flight through `B` when the publisher ends the track. `B`'s copy, asked from a later group, completes, `B`'s fetch from the publisher is cancelled, and `E`'s read fails with `NotFound` while the publisher still writes the rest (`NoSkipWhileHeld`). +- `residual_a_fetch_from_a_completed_copy_never_leaves_the_relay`: the same group read on only after `E`'s serving copy completed. `Recover::poll_fetch` calls `fetch_group` on that copy, but no FETCH goes on the wire, so the read waits out the subscriber's budget (`Settles`). + +## Reading a failure + +A counterexample is a path through the model, not yet a bug. Replay it on the real stack in `rs/moq-net/tests/integration/failover_chain.rs`: relays are `origin::Producer`s linked over the memory transport (`link`, `priced_link`, a cost to make a route win), a relay or hop dies by aborting its sessions, a group read past a failed copy is what makes `Recover` fetch, and time is simulated. If the code does not follow the path, the model is wrong: fix the model to match the code. If it does, report the path and the rule in the code's words, and pin it as a `residual_*` test with its own config so the others still pass. Do not weaken a rule, add a constraint, or shrink the bounds until the check passes. + +## Coverage + +Sync commit: `88572c583e2f64c7f5fc9bfa59df90706308497e`. Run `git log 88572c583e.. -- rs/moq-net/src/model/resume.rs rs/moq-net/src/model/front.rs rs/moq-net/src/model/origin.rs` to see what changed since. After a change to a covered function, mirror it in the model, rerun every config, and move the sync commit forward only once the model describes the code at the new commit. + +| Code (`rs/moq-net/src/model/`) | Model | +| --- | --- | +| `resume.rs` `Reader::sync`, `backfill_gaps`, `Producer::subscription` | `ResumeAsk`, `Demand`, `Switch`, `Subscribe` | +| `resume.rs` `Reader::take`, `poll_end` | `HandOut`, `Drained`, `EndOk` | +| `resume.rs` `Reader::let_go`, `Copy::retains`, `Producer::park` | `LetGo`, `Park` | +| `resume.rs` `Recover::wants`, `poll`, `held`, `poll_serving` | `Recover`, `Holders`, `Exhausted`, `Abort` | +| `resume.rs` `Recover::poll_fetch`, `Fetching`; `track.rs` `fetch_group` | `Ask` | +| `front.rs` `track_ended`; `origin.rs` `Action::Finish`, `TrackIo::end` | `FrontFinish`, `Whole` | +| `front.rs` failover and its unroutable end | `Switch`, `FrontFail` | + +## Not covered + +Routing is abstracted to any live upstream winning, so feasibility, ROUTE_END, and announce order are `verify-route`'s; how a reader picks among its copies, bounds replaced copies, and orders groups is `verify-resume`'s; drops, skips, and re-offers on a hop are `verify-subscribe`'s. The client's track fails only through `FrontFail`, so whether one dead relay can end playback is that step's guard, not a rule. Every hop has an hour's budget, so nothing goes stale or expires. The origin writes each group whole and never fails, `E` never dies, a dead relay never returns, and a relay's cache is dropped when it parks. A fetched group holds its head from frame 0 (`lend_head`), and compressed groups are left out. A pass covers two groups of two frames, one death, one switch per relay, and one client. diff --git a/quest/m1/failover-chain-model.md b/quest/m1/failover-chain-model.md deleted file mode 100644 index 2d4c139ec9..0000000000 --- a/quest/m1/failover-chain-model.md +++ /dev/null @@ -1,35 +0,0 @@ -# [L] A model of a relay chain's failover delivers every group once - -## Goal - -A TLA+ model of one track served to a client through a chain of relays -(client, relay, relay, origin, with an alternate path) checks that when a -relay dies or a route moves at any hop, the client gets every group its -budget allows, each once and in order, and the track never ends while the -broadcast is live. - -## Plan - -Decided 2026-11-10 (maintainer, /quest-plan). Resume failover has caused many -production issues, and each subsystem model in [moq-dev/moq#8447](https://github.com/moq-dev/moq/pull/8447) -checks one layer alone: routing picks the next hop (`verify-route`), a front -switches copies (`verify-resume`), and a subscription accounts for each group -(`verify-subscribe`). This composes them at the level where they interact: -each relay's front switching routes while the relay below it is itself -resuming. - -- Abstract each layer to the steps its own model proved, citing that model, - so the state space stays small: a route change is one step, a copy switch is - the resume model's switch, a group's delivery is the subscribe model's - accounting. -- Rules: each group within the client's budget reaches it exactly once, in - order; no group is skipped while an alternate path holds it; the track - ends only after the origin ends it; no relay keeps a copy after the client - leaves. -- Cover a group that stalls or fails mid-read and continues on another - copy at the same frame (`Recover` in `model/resume.rs`), which - `verify-resume` leaves out because it models whole groups. -- Replay each counterexample on the real stack (relays over the memory - transport, mocked clock), and pin confirmed bugs as `residual_*` tests. - -Public API: none. Wire: none. diff --git a/rs/moq-net/tests/integration/failover_chain.rs b/rs/moq-net/tests/integration/failover_chain.rs new file mode 100644 index 0000000000..bbb92d706f --- /dev/null +++ b/rs/moq-net/tests/integration/failover_chain.rs @@ -0,0 +1,182 @@ +#![cfg(feature = "async")] + +//! Failover along a chain of relays, replaying what `rs/moq-net/verify/failover/FailoverChain.tla` +//! checks: a group the subscriber started continues on another route at the same frame +//! while any path still holds it. +//! +//! The publisher `P` is pulled by relays `A` and `B`. The subscribing relay `E` reads through +//! `A` until a cheaper route through `B` appears; `B` resumes it from the newest group `E` +//! handed out. Then `A`'s session to `E` dies with an older group half read, so `E` fetches +//! the rest of that group from `B`, whose subscription never asked for it. + +use crate::route_change::{link, payload, priced_link, produce_origin, settle, timed}; +use crate::support::harness::MockPair; + +use std::time::Duration; + +use futures::StreamExt; +use futures::channel::mpsc; +use moq_net::{Error, Timestamp, Version, group, origin, track}; + +/// Within the subscriber's one-minute budget, so a group that never continues is a hang +/// rather than a group given up as too old. +const PATIENCE: Duration = Duration::from_secs(30); + +type Frames = mpsc::UnboundedReceiver>>>; + +struct Chain { + /// Group 0, open at the publisher with its first frame written. + group0: Option, + /// Group 0 as `E`'s subscriber reads it, past its first frame. + read0: Option, + track: track::Producer, + _sub: track::Subscriber, + _read1: group::Consumer, + _relays: Vec, + _broadcast: origin::Route, + _links: Vec, +} + +impl Chain { + /// `E` holds group 0 half read through `A`, and group 1 handed out, while `B` serves it + /// from group 1 on and `A`'s session to `E` is gone. + async fn new() -> Self { + let version: Version = "moq-lite-07-wip".parse().unwrap(); + let publisher = produce_origin(1); + let relay_a = produce_origin(2); + let relay_b = produce_origin(3); + let relay_e = produce_origin(4); + + let broadcast = publisher.route("live", origin::RouteOptions::hidden()).unwrap(); + let track = broadcast.broadcast().create_track("video", timed()).unwrap(); + broadcast.announce().unwrap(); + + let mut links = vec![ + link(version, &publisher, &relay_a).await, + link(version, &publisher, &relay_b).await, + ]; + let a_to_e = priced_link(version, &relay_a, &relay_e, Some(1_000)).await; + + let remote = relay_e + .consume() + .follow("live", None) + .unwrap() + .available() + .await + .unwrap() + .unwrap(); + let prefs = + track::Subscription::default().with_delay(track::Delay::default().with_max(Duration::from_secs(60))); + let mut sub = remote.track("video").unwrap().subscribe(prefs).await.unwrap(); + + let mut group0 = track.append_group().unwrap(); + group0.write_frame(Timestamp::ZERO, payload(0, 0)).unwrap(); + let mut read0 = sub.recv_group().await.unwrap().unwrap(); + assert_eq!(read0.sequence, 0); + assert_eq!( + read0.read_frame().await.unwrap().unwrap().payload.to_vec(), + payload(0, 0) + ); + + let mut group1 = track.append_group().unwrap(); + group1.write_frame(Timestamp::ZERO, payload(1, 0)).unwrap(); + group1.finish().unwrap(); + let mut read1 = sub.recv_group().await.unwrap().unwrap(); + assert_eq!(read1.sequence, 1); + assert_eq!( + read1.read_frame().await.unwrap().unwrap().payload.to_vec(), + payload(1, 0) + ); + + // The cheaper route through `B` wins; `E` asks it from group 1. + links.push(link(version, &relay_b, &relay_e).await); + settle().await; + + a_to_e.server.abort(Error::Cancel); + a_to_e.client.abort(Error::Cancel); + settle().await; + + Self { + group0: Some(group0), + read0: Some(read0), + track, + _sub: sub, + _read1: read1, + _relays: vec![relay_a, relay_b, relay_e], + _broadcast: broadcast, + _links: links, + } + } + + /// Read group 0's next frame in the background, which fetches the rest from `B`. + fn read_on(&mut self) -> Frames { + let (tx, rx) = mpsc::unbounded(); + let mut read0 = self.read0.take().expect("read once"); + kio::clock::sim::spawn(async move { + let frame = read0.read_frame().await; + let _ = tx.unbounded_send(frame.map(|frame| frame.map(|frame| frame.payload.to_vec()))); + }); + rx + } + + /// The publisher ends the track at group 2 while group 0 is still open. + async fn end(&mut self) { + self.track.finish_at(track::Position::group(2), None).unwrap(); + settle().await; + } + + /// The publisher writes the rest of group 0, which every relay can still reach. + fn finish_group0(&mut self) { + let mut group0 = self.group0.take().expect("finished once"); + group0.write_frame(Timestamp::ZERO, payload(0, 1)).unwrap(); + group0.finish().unwrap(); + } +} + +/// Without the end, the rest of group 0 comes through `B`: the path both residuals break. +#[kio::test] +async fn a_half_read_group_continues_through_the_new_route() { + let mut chain = Chain::new().await; + let mut rx = chain.read_on(); + settle().await; + chain.finish_group0(); + let frame = kio::clock::timeout(PATIENCE, rx.next()).await.expect("group 0 hung"); + assert_eq!(frame.unwrap().unwrap(), Some(payload(0, 1))); +} + +/// Pins a group cut short that `verify/failover/FailoverChain.tla` rules out +/// (`NoSkipWhileHeld`). `E`'s fetch of the rest of group 0 is in flight through `B` when +/// the publisher ends the track: `B`'s copy, asked from group 1, completes, which cancels +/// `B`'s fetch from `P`, and `E`'s read of group 0 fails though every relay still reaches +/// `P`, which then writes the rest. A fix keeps the fetch, so the frame arrives. +#[kio::test] +async fn residual_ending_the_track_fails_a_fetch_in_flight() { + let mut chain = Chain::new().await; + let mut rx = chain.read_on(); + settle().await; + chain.end().await; + chain.finish_group0(); + let frame = kio::clock::timeout(PATIENCE, rx.next()) + .await + .expect("group 0 hung") + .unwrap(); + assert!(frame.is_err(), "group 0 continued: {frame:?}"); +} + +/// Pins a hang that `verify/failover/FailoverChain.tla` rules out (`Settles`). The +/// publisher ends the track before `E` reads on, so `E`'s copy from `B`, asked from +/// group 1, completes and `E`'s track ends. Reading group 0 on then asks `B`'s completed +/// copy for the rest, and that fetch never goes on the wire: the read waits out the +/// subscriber's budget though `P` has written the rest. A fix sends the fetch, so the +/// frame arrives. +#[kio::test] +async fn residual_a_fetch_from_a_completed_copy_never_leaves_the_relay() { + let mut chain = Chain::new().await; + chain.end().await; + let mut rx = chain.read_on(); + chain.finish_group0(); + assert!( + kio::clock::timeout(PATIENCE, rx.next()).await.is_err(), + "group 0 continued" + ); +} diff --git a/rs/moq-net/tests/integration/main.rs b/rs/moq-net/tests/integration/main.rs index e87fc5e918..cb0d66d025 100644 --- a/rs/moq-net/tests/integration/main.rs +++ b/rs/moq-net/tests/integration/main.rs @@ -24,6 +24,7 @@ mod drained_claim; mod empty_group; mod errored_end; mod extensions; +mod failover_chain; mod fastest_reader; mod fetch_cancel; mod fetch_fanout; diff --git a/rs/moq-net/verify/failover/EndedRelay.cfg b/rs/moq-net/verify/failover/EndedRelay.cfg new file mode 100644 index 0000000000..283268079b --- /dev/null +++ b/rs/moq-net/verify/failover/EndedRelay.cfg @@ -0,0 +1,19 @@ +\* FailoverChain.cfg with B also routing through A, so the route can move at +\* the middle hop. Fails on the open finding in the verify-failover skill: a +\* relay whose track ended cannot move a fetch off a route that dies. +CONSTANTS + G = 2 + F = 2 + MaxDeaths = 1 + MaxSwitches = 1 + Mesh = TRUE + Leave = FALSE + +SPECIFICATION Spec + +INVARIANTS + TypeOK + CleanEndIsComplete + CleanEndIsDeclared + NoSkipWhileHeld + SettledIsWhole diff --git a/rs/moq-net/verify/failover/FailoverChain.cfg b/rs/moq-net/verify/failover/FailoverChain.cfg new file mode 100644 index 0000000000..dff6afd994 --- /dev/null +++ b/rs/moq-net/verify/failover/FailoverChain.cfg @@ -0,0 +1,21 @@ +\* The client reads two groups of two frames through E, which fails over +\* between A and B, each pulling from the origin. One relay may die, and each +\* relay may move off a live route once. The client stays, so a deadlock is a +\* hang; Leave.cfg lets it go to check cleanup. EndedRelay.cfg adds B's +\* route through A while its finding is open. +CONSTANTS + G = 2 + F = 2 + MaxDeaths = 1 + MaxSwitches = 1 + Mesh = FALSE + Leave = FALSE + +SPECIFICATION Spec + +INVARIANTS + TypeOK + CleanEndIsComplete + CleanEndIsDeclared + NoSkipWhileHeld + SettledIsWhole diff --git a/rs/moq-net/verify/failover/FailoverChain.tla b/rs/moq-net/verify/failover/FailoverChain.tla new file mode 100644 index 0000000000..4d70aec146 --- /dev/null +++ b/rs/moq-net/verify/failover/FailoverChain.tla @@ -0,0 +1,433 @@ +---------------------------- MODULE FailoverChain ---------------------------- +(***************************************************************************) +(* One track served to a client through a chain of relays, as the relays *) +(* of `rs/moq-net` compose: each relay's front (`model/front.rs`) serves *) +(* the track from one upstream route at a time, and each downstream *) +(* subscription reads it through a resume reader (`model/resume.rs`) whose *) +(* groups continue across switches through `Recover`. *) +(* *) +(* C <- E <- A <- O the client reads relay E, which starts on A *) +(* E <- B <- O B is E's alternate path *) +(* B <- A with Mesh, B may also route through A *) +(* *) +(* Each layer is one step its own model checked, so the state stays small: *) +(* - A route change is one `Switch` (`verify-route` checks which next hop *) +(* routing picks; here any live upstream may win). *) +(* - A switch asks the new copy from the reader's newest group, or from *) +(* the lowest gap below it (`Reader::sync`, `backfill_gaps`, *) +(* `verify-resume`). A reader hands each group out once, from any copy *) +(* its relay holds, and ends cleanly once its serving copy is complete *) +(* and nothing a replaced copy may still deliver is missing *) +(* (`OnceEach`, `CleanEndIsComplete`, `EndWaitsForReplaced` there). *) +(* - A group's delivery over a hop is the subscribe model's accounting *) +(* with an hour's budget (`verify-subscribe`): a group handed out *) +(* arrives unless its session dies, and nothing is dropped as stale. *) +(* *) +(* What this model adds is frames: a group is F frames, and a group whose *) +(* copy fails or stalls mid-read continues on another copy at the same *) +(* frame (`Recover`), from a copy its relay holds, from the serving copy's *) +(* subscription, or by fetching the rest from the serving route, which *) +(* asks its own upstream in turn. *) +(* *) +(* Scope: the origin O never fails, writes each group whole, and E never *) +(* dies, so the client always has its one hop; a dead relay never returns; *) +(* every hop subscribes before the first group, and a copy's range is *) +(* resolved from its first group (SUBSCRIBE_OK), so a relay knows which *) +(* groups its copy owes. A fetch reaches the serving route while that *) +(* route lives, after the track ended too: the skill's open findings are *) +(* where the code does not yet. *) +(***************************************************************************) +EXTENDS Integers, FiniteSets + +CONSTANTS + G, \* groups 0 .. G - 1 + F, \* frames per group + MaxDeaths, \* relays among A and B that may die + MaxSwitches, \* route changes, per relay, away from a live route + Mesh, \* whether B may route through A + Leave \* whether the client may unsubscribe + +Groups == 0 .. G - 1 +Relays == {"E", "A", "B"} +Mortal == {"A", "B"} +None == "-" + +\* The routes each node may take, in the order the front prefers. +Up(n) == + CASE n = "C" -> {"E"} + [] n = "E" -> {"A", "B"} + [] n = "A" -> {"O"} + [] n = "B" -> IF Mesh THEN {"O", "A"} ELSE {"O"} + +\* A copy at d of the track as u serves it. Its reader lives at u. +Edges == {<<"C", "E">>} \cup UNION {{<> : u \in Up(d)} : d \in Relays} +Downs(u) == {e \in Edges : e[2] = u} +CE == <<"C", "E">> + +Min(S) == CHOOSE x \in S : \A y \in S : x <= y +Max(S) == CHOOSE x \in S : \A y \in S : y <= x + +VARIABLES + org, \* the origin's track: frames written per group, and whether it ended + alive, \* which relays are up + deaths, \* relays that died + cp, \* cp[e]: the copy at e[1] of the track e[2] serves, and e[2]'s reader for it + front, \* front[r]: the route r serves from, how its track ended, switches made + left \* the client unsubscribed + +vars == <> + +(***************************************************************************) +(* A copy, and the reader at its upstream that feeds it. *) +(* *) +(* st "none" (not subscribed), "live", or "failed" (its session died, *) +(* or its upstream's track failed). A failed copy keeps its cache. *) +(* ask the groups its subscription asks for. *) +(* fetch groups fetched outside the subscription (`fetch_group`). *) +(* fr fr[g]: frames of g it holds; -1 before the upstream hands g out.*) +(* bad groups the upstream aborted mid-read. *) +(* fin the upstream's reader ended the subscription cleanly. *) +(* src src[g]: the upstream's copy its reader reads g from (`Recover`).*) +(***************************************************************************) + +Fresh(ask) == + [st |-> "live", ask |-> ask, fetch |-> {}, fr |-> [g \in Groups |-> -1], + bad |-> {}, fin |-> FALSE, src |-> [g \in Groups |-> None]] + +Gone == + [st |-> "none", ask |-> {}, fetch |-> {}, fr |-> [g \in Groups |-> -1], + bad |-> {}, fin |-> FALSE, src |-> [g \in Groups |-> None]] + +Live(e) == cp[e].st = "live" +Held(e) == cp[e].st # "none" + +\* A group the reader still owes its copy: asked or fetched, and not handed out. +Lacks(e, g) == Live(e) /\ g \in cp[e].ask \cup cp[e].fetch /\ cp[e].fr[g] = -1 +\* A group handed out and still short of its last frame. +Short(e, g) == Live(e) /\ cp[e].fr[g] \in 0 .. F - 1 /\ g \notin cp[e].bad + +\* The copies a relay's readers read: the origin's own track, or every copy the +\* relay still holds (the serving one and the replaced ones it keeps). +Srcs(u) == IF u = "O" THEN {"O"} ELSE {s \in Up(u) : Held(<>)} +SrcFr(u, s, g) == IF u = "O" THEN org.fr[g] ELSE cp[<>].fr[g] +\* The source will bring no more frames of g: its copy failed or gave up on g. +SrcDead(u, s, g) == + /\ u # "O" + /\ \/ cp[<>].st # "live" + \/ g \in cp[<>].bad + +\* What a switch asks the new copy for: from the reader's newest group handed +\* out (`sync`), or from the lowest group below it the reader lacks +\* (`backfill_gaps`), or everything when nothing was handed out yet. +ResumeAsk(e) == + LET got == {g \in Groups : cp[e].fr[g] >= 0} + newest == Max(got) + gaps == {g \in cp[e].ask : g < newest /\ cp[e].fr[g] = -1} + from == IF got = {} THEN 0 ELSE IF gaps # {} THEN Min(gaps) ELSE newest + IN {g \in cp[e].ask : g >= from} + +\* What a copy at u asks: the union of its readers' demand (`Producer::subscription`). +Demand(u) == UNION {ResumeAsk(e) : e \in {x \in Downs(u) : Live(x)}} +Wanted(u) == \E e \in Downs(u) : Live(e) + +Serving(u) == <> +Routable(w) == IF w = "O" THEN TRUE ELSE alive[w] /\ front[w].end # "err" + +\* A complete copy (`TrackState::is_complete` once every group below the end +\* finished): its upstream ended it, and every group it asked holds every frame. +Whole(e) == + /\ cp[e].fin + /\ \A g \in cp[e].ask : cp[e].fr[g] = F \/ g \in cp[e].bad + +\* A held copy at u may still land g: it is live, asked for g, and is not done. +MayLand(u, g) == + \E s \in Up(u) : + /\ Live(<>) + /\ g \in cp[<>].ask + /\ cp[<>].fr[g] = -1 + /\ ~cp[<>].fin + +\* The reader at u has handed out all it can: every group its copy asks for is +\* out, or no copy at u holds it or may still land it (`poll_end`). +Drained(e) == + LET u == e[2] IN + \A g \in cp[e].ask : + \/ cp[e].fr[g] >= 0 + \/ /\ \A s \in Srcs(u) : SrcFr(u, s, g) < 0 + /\ ~MayLand(u, g) + +\* Where a short group can continue at u: a copy holding it whose source is +\* still alive or holds a frame past the reader's (`Recover::held`). +Holders(u, e, g) == + {s \in Srcs(u) : + /\ s # cp[e].src[g] + /\ SrcFr(u, s, g) >= 0 + /\ ~SrcDead(u, s, g) \/ SrcFr(u, s, g) > cp[e].fr[g]} + +\* The group's source has nothing more for the reader now. +Exhausted(e, g) == SrcFr(e[2], cp[e].src[g], g) <= cp[e].fr[g] + +(***************************************************************************) +(* Steps. *) +(***************************************************************************) + +Init == + /\ org = [fr |-> [g \in Groups |-> -1], fin |-> FALSE] + /\ alive = [r \in Relays |-> TRUE] + /\ deaths = 0 + \* The client subscribed through E, E through A, and A to the origin. + /\ cp = [e \in Edges |-> + IF e \in {CE, <<"E", "A">>, <<"A", "O">>} THEN Fresh(Groups) ELSE Gone] + /\ front = [r \in Relays |-> + [cur |-> IF r = "E" THEN "A" ELSE "O", end |-> "open", sw |-> 0]] + /\ left = FALSE + +\* The origin writes a group whole, in order. Frames split only at the hops. +Write(g) == + /\ ~org.fin + /\ org.fr[g] < 0 + /\ IF g = 0 THEN TRUE ELSE org.fr[g - 1] >= 0 + /\ org' = [org EXCEPT !.fr[g] = F] + /\ UNCHANGED <> + +\* The origin ends the track after its last frame. +OriginEnd == + /\ ~org.fin + /\ \A g \in Groups : org.fr[g] = F + /\ org' = [org EXCEPT !.fin = TRUE] + /\ UNCHANGED <> + +\* The reader at e[2] hands out a group from a copy that holds it, opening its +\* stream to e[1] (`Reader::take`). A fetch is served after the end too. +HandOut(e, g, s) == + /\ Lacks(e, g) + /\ ~cp[e].fin \/ g \in cp[e].fetch + /\ s \in Srcs(e[2]) + /\ SrcFr(e[2], s, g) >= 0 + /\ cp' = [cp EXCEPT ![e].fr[g] = 0, ![e].src[g] = s] + /\ UNCHANGED <> + +\* The next frame of a group crosses the hop. +Frame(e, g) == + /\ Short(e, g) + /\ SrcFr(e[2], cp[e].src[g], g) > cp[e].fr[g] + /\ cp' = [cp EXCEPT ![e].fr[g] = @ + 1] + /\ UNCHANGED <> + +\* A short group whose copy failed continues on any other copy holding it, and +\* one whose copy stalls while a newer route serves continues on the serving +\* copy, both at the same frame (`Recover::poll`). +Recover(e, g, s) == + LET u == e[2] IN + /\ u # "O" + /\ Short(e, g) + /\ Exhausted(e, g) + /\ front[u].end # "err" + /\ s \in Holders(u, e, g) + /\ \/ SrcDead(u, cp[e].src[g], g) + \/ cp[e].src[g] # front[u].cur /\ s = front[u].cur /\ front[u].end = "open" + /\ cp' = [cp EXCEPT ![e].src[g] = s] + /\ UNCHANGED <> + +\* A relay asks its serving route for a group a reader needs that no copy it +\* holds has or may still land: a backfill for a widened or fetched range, or a +\* fetch of the rest of a short group (`Recover::poll_fetch`). +Ask(u, g) == + LET w == front[u].cur + e0 == Serving(u) + IN + /\ u \in Relays + /\ front[u].end # "err" + /\ Live(e0) + /\ g \notin cp[e0].ask \cup cp[e0].fetch + /\ cp[e0].fr[g] = -1 + /\ \E e \in Downs(u) : + \/ /\ Lacks(e, g) + /\ \A s \in Srcs(u) : SrcFr(u, s, g) < 0 + /\ ~MayLand(u, g) + \/ /\ Short(e, g) + /\ Exhausted(e, g) + /\ cp[e].src[g] # w + /\ Holders(u, e, g) = {} + /\ cp' = [cp EXCEPT ![e0].fetch = @ \cup {g}] + /\ UNCHANGED <> + +\* A short group nothing can continue fails (`Recover::poll` gives up): its +\* source failed, no other copy holds it, and no fetch can reach the rest, +\* because the front has no route left, ended with its serving copy gone, or +\* the live serving copy is the source that gave up on the group. +Abort(e, g) == + LET u == e[2] IN + /\ u # "O" + /\ Short(e, g) + /\ Exhausted(e, g) + /\ SrcDead(u, cp[e].src[g], g) + /\ Holders(u, e, g) = {} + /\ \/ front[u].end = "err" + \/ front[u].end = "ok" /\ ~Live(Serving(u)) + \/ cp[e].src[g] = front[u].cur /\ Live(Serving(u)) + /\ cp' = [cp EXCEPT ![e].bad = @ \cup {g}] + /\ UNCHANGED <> + +\* A relay with readers subscribes its serving route. +Subscribe(u) == + /\ u \in Relays + /\ front[u].end = "open" + /\ Wanted(u) + /\ Routable(front[u].cur) + /\ ~Held(Serving(u)) + /\ cp' = [cp EXCEPT ![Serving(u)] = Fresh(Demand(u))] + /\ UNCHANGED <> + +\* The front moves to another route: forced off a dead one, or at will while +\* the switches last (`Producer::splice`). A copy it still holds of that route +\* is asked again from where the readers got to; otherwise a new one is. +Switch(u, w) == + LET usable == Live(Serving(u)) /\ Routable(front[u].cur) + e1 == <> + IN + /\ u \in Relays + /\ front[u].end = "open" + /\ Wanted(u) + /\ w \in Up(u) /\ w # front[u].cur + /\ Routable(w) + /\ usable => front[u].sw < MaxSwitches + /\ front' = [front EXCEPT ![u].cur = w, ![u].sw = @ + (IF usable THEN 1 ELSE 0)] + /\ cp' = [cp EXCEPT ![e1] = + IF Live(e1) /\ ~cp[e1].fin THEN [@ EXCEPT !.ask = Demand(u)] + ELSE IF Live(e1) THEN @ + ELSE Fresh(Demand(u))] + /\ UNCHANGED <> + +\* The serving copy completed: the front ends the track (`Action::Finish`). +FrontFinish(u) == + /\ u \in Relays + /\ front[u].end = "open" + /\ Live(Serving(u)) + /\ Whole(Serving(u)) + /\ front' = [front EXCEPT ![u].end = "ok"] + /\ UNCHANGED <> + +\* No route is left: the front fails the track, and every reader with it. +FrontFail(u) == + /\ u \in Relays + /\ front[u].end = "open" + /\ ~Live(Serving(u)) \/ ~Routable(front[u].cur) + /\ \A w \in Up(u) : ~Routable(w) + /\ front' = [front EXCEPT ![u].end = "err"] + /\ cp' = [e \in Edges |-> + IF e[2] = u /\ Live(e) THEN [cp[e] EXCEPT !.st = "failed"] ELSE cp[e]] + /\ UNCHANGED <> + +\* A reader ends its subscription cleanly: its track ended at the origin or +\* the relay's front finished, and it handed out all it can. +EndOk(e) == + LET u == e[2] IN + /\ Live(e) + /\ ~cp[e].fin + /\ IF u = "O" THEN org.fin ELSE front[u].end = "ok" + /\ Drained(e) + /\ cp' = [cp EXCEPT ![e].fin = TRUE] + /\ UNCHANGED <> + +\* A relay lets go of a replaced copy nothing needs: no short group reads from +\* it or could continue on it, and it holds or may land no group a reader +\* lacks (`Reader::let_go`, `Copy::retains`). +LetGo(u, s) == + LET e1 == <> IN + /\ u \in Relays + /\ s \in Up(u) + /\ Held(e1) + /\ s # front[u].cur \/ front[u].end = "err" + /\ \A e \in Downs(u), g \in Groups : + /\ Short(e, g) => cp[e].src[g] # s /\ cp[e1].fr[g] < 0 /\ ~MayLand(u, g) + /\ Lacks(e, g) => cp[e1].fr[g] < 0 /\ ~(Live(e1) /\ g \in cp[e1].ask) + /\ cp' = [cp EXCEPT ![e1] = Gone] + /\ UNCHANGED <> + +\* A relay nobody reads parks its track, letting go of every copy (`park`). A +\* track that ended is forgotten, so the next reader gets a fresh front: the +\* cache is only an optimization, so the model keeps none. +Park(u) == + /\ u \in Relays + /\ ~Wanted(u) + /\ \E s \in Up(u) : Held(<>) + /\ cp' = [e \in Edges |-> IF e[1] = u THEN Gone ELSE cp[e]] + /\ front' = [front EXCEPT ![u].end = IF @ = "ok" THEN "open" ELSE @] + /\ UNCHANGED <> + +\* A relay dies: copies downstream of it fail, and its own vanish. +Die(r) == + /\ r \in Mortal + /\ alive[r] + /\ deaths < MaxDeaths + /\ alive' = [alive EXCEPT ![r] = FALSE] + /\ deaths' = deaths + 1 + /\ cp' = [e \in Edges |-> + IF e[1] = r THEN Gone + ELSE IF e[2] = r /\ Live(e) THEN [cp[e] EXCEPT !.st = "failed"] + ELSE cp[e]] + /\ UNCHANGED <> + +\* The client unsubscribes. +Unsubscribe == + /\ Leave + /\ ~left + /\ left' = TRUE + /\ cp' = [cp EXCEPT ![CE] = Gone] + /\ UNCHANGED <> + +\* The read is over, or the client left and every relay let go. +Finished == + \/ /\ ~left + /\ \/ cp[CE].st = "failed" + \/ Whole(CE) /\ \A g \in Groups : cp[CE].fr[g] >= 0 + \/ left /\ \A e \in Edges : ~Held(e) + +Done == + /\ Finished + /\ UNCHANGED vars + +Next == + \/ \E g \in Groups : Write(g) + \/ OriginEnd + \/ \E e \in Edges, g \in Groups : + \/ \E s \in Srcs(e[2]) : HandOut(e, g, s) \/ Recover(e, g, s) + \/ Frame(e, g) \/ Abort(e, g) + \/ \E u \in Relays : + \/ Subscribe(u) \/ FrontFinish(u) \/ FrontFail(u) \/ Park(u) + \/ \E w \in Up(u) : Switch(u, w) \/ LetGo(u, w) + \/ \E g \in Groups : Ask(u, g) + \/ \E e \in Edges : EndOk(e) + \/ \E r \in Mortal : Die(r) + \/ Unsubscribe + \/ Done + +Spec == Init /\ [][Next]_vars + +(***************************************************************************) +(* Rules. *) +(***************************************************************************) + +\* The client's track ends cleanly only with every group handed out. +CleanEndIsComplete == Live(CE) /\ cp[CE].fin => \A g \in Groups : cp[CE].fr[g] >= 0 + +\* The client's track ends cleanly only after the origin ended it. +CleanEndIsDeclared == cp[CE].fin => org.fin + +\* A group the client started fails only once no route is left to continue it. +NoSkipWhileHeld == cp[CE].bad # {} => front["E"].end = "err" + +\* A finished read holds every frame of every group, unless E lost every route. +SettledIsWhole == + (Finished /\ ~left /\ cp[CE].st = "live") => + \A g \in Groups : cp[CE].fr[g] = F + +TypeOK == + /\ \A e \in Edges : + /\ cp[e].st \in {"none", "live", "failed"} + /\ cp[e].bad \subseteq Groups + /\ \A g \in Groups : cp[e].fr[g] \in -1 .. F + /\ \A r \in Relays : front[r].end \in {"open", "ok", "err"} + +============================================================================= diff --git a/rs/moq-net/verify/failover/Leave.cfg b/rs/moq-net/verify/failover/Leave.cfg new file mode 100644 index 0000000000..cb09b109e1 --- /dev/null +++ b/rs/moq-net/verify/failover/Leave.cfg @@ -0,0 +1,19 @@ +\* FailoverChain.cfg with a client that may leave at any point, so a deadlock +\* is a relay that keeps a copy after it left. Leaving is always possible +\* here, which hides a playback hang: FailoverChain.cfg checks that. +CONSTANTS + G = 2 + F = 2 + MaxDeaths = 1 + MaxSwitches = 1 + Mesh = FALSE + Leave = TRUE + +SPECIFICATION Spec + +INVARIANTS + TypeOK + CleanEndIsComplete + CleanEndIsDeclared + NoSkipWhileHeld + SettledIsWhole