From bdceae55658d8109692fad02eab7a893c07d6bee Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 27 Aug 2026 23:16:55 +0000 Subject: [PATCH] A truncated roster read is a successful one, so absence from a prefix rendered as "the runner is gone" OrganizationRunnerRosterEvidence had two states -- observed, or read-unavailable -- and a TRUNCATED read had no spelling. The GitHub org runners API is paginated at 100 rows; measured 2026-08-27T21:29Z the org holds 522 registrations, so a one-page read sees 19% of the roster and enters as RosterObserved carrying a prefix. Every registration past the cut then classified as absent, which renders SlotConnectivityOrphaned, which connectivity_replace_action maps to a restart. That is the empty-observation narrow (DESIGN section 5): an observation that could not express what it failed to see, rendered as the verdict "these are gone". The adjacent case was already defended -- roster_unavailable_yields_unknown_not_detached refuses to read a FAILED read as everything-detached -- and truncation slipped past it because a truncated read arrives as SUCCESS. RosterObservedPartial carries observed_count and authority_total as a variant rather than a flag, and organization_runner_roster_from_page derives completeness at the boundary: a caller cannot hand it a prefix and reach RosterObserved, since that variant requires the observed length to equal the authority's own total. The refusal is per-question rather than per-roster -- slots inside the prefix still answer normally, and only the ABSENT arm changes -- because refusing the whole read would replace a fail-open with a fail-shut that stops reconciliation on hosts the read covered. Aggregate widths do refuse, since no sub-question of an aggregate is answered correctly by a prefix. organization_roster_is_one_org_read_note asserted the false completeness fact and is DELETED rather than corrected; its three surviving facts are enumerated into organization_roster_read_locus_note, which makes no completeness claim. Evidence by execution, compile on 472cadfcfe at 0 blocking / 435 files emitted. Five witnesses baseline true. Mutating the partial arm's unseen answer back to Orphaned flips truncated_roster_never_orphans_an_unseen_slot to false while complete_roster_still_orphans_an_unseen_slot holds at true, so the RED measures this repair and is not tracking a globally disabled Orphaned; carrier restored byte-identically and both re-run green. RUNG: mechanically preventable for the MODEL. NOT structurally guaranteed for the fleet -- the running runner-liveness-reconcile.sh still requests per_page=100 with no pagination, and this change alters no byte that executes on any host. Next-rung trigger is a render route from this authority to that script, analogous to gunbc.runner_unit_file in #9401. This fixes no observed cancellation. It repairs a false belief about the roster. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_01Sg8fwMAaPgbsNtns1gpVd9 --- dag/gunbc/fleet_runner_connectivity.dag | 113 ++++++++++++++++-- dag/gunbc/runner_capacity_plan.dag | 26 ++++ ...fleet_runner_connectivity_witness_test.dag | 87 +++++++++++++- 3 files changed, 214 insertions(+), 12 deletions(-) diff --git a/dag/gunbc/fleet_runner_connectivity.dag b/dag/gunbc/fleet_runner_connectivity.dag index 5f47208f9eb..c89cca87d8b 100644 --- a/dag/gunbc/fleet_runner_connectivity.dag +++ b/dag/gunbc/fleet_runner_connectivity.dag @@ -28,14 +28,45 @@ data fleet_runner_connectivity_authority_disposition: Disposition = Terminal { reason: "Single authority for GITHUB REGISTRATION CONNECTIVITY versus LOCAL RUNNER INCARNATIONS. It joins one org-level registration roster (remote ground truth from the GitHub Actions runners API) to per-slot stable identities (host, index) and their local systemd incarnations. It does NOT repair wedged runners — that is PR B. It refuses to fold connected width into desired width, and it refuses to treat a roster read failure as 'everything detached' (empty-observation narrow)." } -data organization_roster_is_one_org_read_note: String = "THE ROSTER IS ONE CENTRAL ORG READ, not a per-host poll. GitHub's org runners API returns every self-hosted registration for the organization in one response; slot health is derived by joining that roster to stable (host, index) identities. The gunbai-ci GitHub App carries organization_self_hosted_runners read permission for this producer. Local journal mining and per-host gh api calls are not the authority for whether GitHub will schedule work onto a registration." +data organization_roster_read_locus_note: String = "THE ROSTER IS ONE CENTRAL ORG READ, not a per-host poll: slot health is derived by joining the org-level registration roster to stable (host, index) identities. The gunbai-ci GitHub App carries organization_self_hosted_runners read permission for this producer. Local journal mining and per-host gh api calls are not the authority for whether GitHub will schedule work onto a registration.\n\nTHIS ROW SAYS NOTHING ABOUT COMPLETENESS, AND THAT IS DELIBERATE. It replaces organization_roster_is_one_org_read_note, which asserted that the API 'returns every self-hosted registration for the organization in one response'. That was false and is now decided by OrganizationRunnerRosterEvidence rather than claimed here; a corrected sentence beside a carrier that decides the same question would be a second authority for it (DESIGN section 3). The three facts above are the surviving contents of that row, enumerated rather than swept away with it -- a prose row is deleted for one reason and takes everything in it unless its contents are named first." data achieved_widths_are_orthogonal_to_desired_width_note: String = "THE ACHIEVED AXES HERE ARE ORTHOGONAL TO gunbc.runner_slot_allocation's desired-side widths (#7930 candidate/actuatable/observed). registered_width counts GitHub org roster rows; connected_width counts status == online; schedulable_width counts online AND NOT busy; executing_width counts online AND busy. desired_width is INTENT from gunbc_runner_slots_per_host and does NOT reconcile down when connected collapses during an outage. materialized_width and unit_active_width are LOCAL incarnation facts pinned from the incident corpus until the local producer grounds them." type OrganizationRunnerRosterEvidence = RosterObserved { observed_on: NonEmptyStr, registrations: List } + | RosterObservedPartial { + observed_on: NonEmptyStr + registrations: List + observed_count: Int + authority_total: Int + } | RosterReadUnavailable { reason: String } +// COMPLETENESS IS DERIVED AT THE BOUNDARY, NEVER ASSERTED BY A CALLER. The org runners API is +// PAGINATED -- measured 2026-08-27 at total_count 522 against a 100-row page -- so a read that +// succeeds is not thereby a read that saw everything. A caller cannot hand this constructor a +// prefix and have it enter as RosterObserved: the only way to reach that variant is for the +// observed length to equal the authority's own total, so "I saw all of it" is a computed fact +// about the response rather than a claim about the request (DESIGN section 5, construction over +// validation). +fn organization_runner_roster_from_page( + observed_on: NonEmptyStr, + registrations: List, + authority_total: Int, +) -> OrganizationRunnerRosterEvidence { + let observed = registrations.length() + if observed == authority_total { + RosterObserved { observed_on: observed_on, registrations: registrations } + } else { + RosterObservedPartial { + observed_on: observed_on, + registrations: registrations, + observed_count: observed, + authority_total: authority_total, + } + } +} + type FleetAchievedRunnerWidths = AchievedWidthsObserved { registered_width: Int @@ -359,6 +390,42 @@ fn local_runner_slot_incarnations() -> List { ) } +fn partial_roster_unseen_reason(observed_count: Int, authority_total: Int) -> String { + concat( + concat("roster read was truncated at ", to_string(observed_count)), + concat( + concat(" of ", to_string(authority_total)), + " registrations, so this slot was never looked at -- absence from a prefix is not absence from the authority" + ) + ) +} + +// ONE LOOKUP, TWO UNSEEN ANSWERS. The complete and truncated arms must read the prefix the SAME way +// or they are two decodings of one fact; the only thing that legitimately differs between them is +// what absence MEANS, so that is the only thing passed in. +fn registration_verdict_or( + registrations: List, + incarnation: LocalRunnerSlotIncarnation, + unseen: RunnerSlotConnectivityVerdict, +) -> RunnerSlotConnectivityVerdict { + match find_registration_by_name(registrations: registrations, name: incarnation.registration_name) { + Absent => unseen + Present { value: reg } => + match reg.status { + GitHubRunnerOnline => + SlotConnectivityHealthy { slot: incarnation.slot, registration_id: reg.id } + GitHubRunnerOffline => + SlotConnectivityDetached { slot: incarnation.slot, registration_id: reg.id } + } + } +} + +// THE REFUSAL IS PER-QUESTION, NOT PER-ROSTER. A truncated read still answers exactly about every +// slot INSIDE the prefix, so refusing the whole roster would be a widen (DESIGN section 5: a failure +// arm must refuse, never widen) and would stop reconciliation on hosts this read covered perfectly +// well. What changes is only the ABSENT arm: a slot missing from a prefix was never observed to be +// missing, and rendering it Orphaned is the empty-observation narrow -- could-not-see reported as +// the verdict "it is gone", whose remedy is a restart at connectivity_replace_action. fn runner_slot_connectivity_verdict_for_incarnation( incarnation: LocalRunnerSlotIncarnation, roster: OrganizationRunnerRosterEvidence, @@ -373,16 +440,25 @@ fn runner_slot_connectivity_verdict_for_incarnation( RosterReadUnavailable { reason: r } => SlotConnectivityUnknown { slot: incarnation.slot, reason: r } RosterObserved { observed_on: _, registrations: regs } => - match find_registration_by_name(registrations: regs, name: incarnation.registration_name) { - Absent => SlotConnectivityOrphaned { slot: incarnation.slot } - Present { value: reg } => - match reg.status { - GitHubRunnerOnline => - SlotConnectivityHealthy { slot: incarnation.slot, registration_id: reg.id } - GitHubRunnerOffline => - SlotConnectivityDetached { slot: incarnation.slot, registration_id: reg.id } - } - } + registration_verdict_or( + registrations: regs, + incarnation: incarnation, + unseen: SlotConnectivityOrphaned { slot: incarnation.slot }, + ) + RosterObservedPartial { + observed_on: _, + registrations: regs, + observed_count: seen, + authority_total: total, + } => + registration_verdict_or( + registrations: regs, + incarnation: incarnation, + unseen: SlotConnectivityUnknown { + slot: incarnation.slot, + reason: partial_roster_unseen_reason(observed_count: seen, authority_total: total), + }, + ) } } } @@ -493,11 +569,22 @@ fn fleet_unit_active_width_total() -> Int { ) } +// A WIDTH OVER A PREFIX IS WRONG, NOT PARTIAL. Unlike the per-slot question, every field here is an +// AGGREGATE over the whole roster, so there is no sub-question a prefix answers correctly -- +// reporting counts from a truncated read would understate connected width and read as an outage. +// The truncated arm is therefore unobserved rather than a smaller number. fn fleet_achieved_runner_widths_from_roster( roster: OrganizationRunnerRosterEvidence, ) -> FleetAchievedRunnerWidths { match roster { RosterReadUnavailable { reason: r } => AchievedWidthsUnobserved { reason: r } + RosterObservedPartial { + observed_on: _, + registrations: _, + observed_count: seen, + authority_total: total, + } => + AchievedWidthsUnobserved { reason: partial_roster_unseen_reason(observed_count: seen, authority_total: total) } RosterObserved { observed_on: _, registrations: regs } => AchievedWidthsObserved { registered_width: regs.length(), @@ -560,6 +647,9 @@ fn connectivity_verdict_is_unknown(v: RunnerSlotConnectivityVerdict) -> Bool { } } +// TRUNCATION IS NOT THIS LAW'S SUBJECT. This function pins the FAILED-read guarantee; the +// truncated-read guarantee is a different proposition with its own witness (unseen slots must not be +// Orphaned), and folding both into one predicate would let either hold up the other's evidence. fn roster_unavailable_yields_unknown_not_detached( roster: OrganizationRunnerRosterEvidence, ) -> Bool { @@ -570,5 +660,6 @@ fn roster_unavailable_yields_unknown_not_detached( v => connectivity_verdict_is_unknown(v: v) && !connectivity_verdict_is_detached(v: v) ) RosterObserved { observed_on: _, registrations: _ } => true + RosterObservedPartial { observed_on: _, registrations: _, observed_count: _, authority_total: _ } => true } } diff --git a/dag/gunbc/runner_capacity_plan.dag b/dag/gunbc/runner_capacity_plan.dag index 97554ca0d84..77aa6b3f5e7 100644 --- a/dag/gunbc/runner_capacity_plan.dag +++ b/dag/gunbc/runner_capacity_plan.dag @@ -11,7 +11,9 @@ import extdeps.github.ci_runner { GitHubSelfHostedRunnerRegistration } import gunbc.fleet_runner_connectivity { OrganizationRunnerRosterEvidence, RosterObserved, + RosterObservedPartial, RosterReadUnavailable, + partial_roster_unseen_reason, runner_slot_connectivity_verdict_for_incarnation, materialized_width_for_host, local_incarnations_for_host, @@ -162,12 +164,25 @@ fn accumulate_decoded_registration( } } +// A POPULATION BUILT FROM A PREFIX IS AN UNDER-COUNT, and this module already names why that is the +// dangerous direction: "a dropped member is an under-count that reads as a converged host". Unlike +// the per-slot verdict, there is no sub-question a prefix answers correctly here -- the whole point +// of the fold is to enumerate everything GitHub holds for this host, so a truncated read refuses. fn observed_github_slot_identities( host: HostIdentity, roster: OrganizationRunnerRosterEvidence, ) -> ObservedGitHubSlotPopulation { match roster { RosterReadUnavailable { reason: r } => GitHubSlotPopulationUnreadable { reason: r } + RosterObservedPartial { + observed_on: _, + registrations: _, + observed_count: seen, + authority_total: total, + } => + GitHubSlotPopulationUnreadable { + reason: partial_roster_unseen_reason(observed_count: seen, authority_total: total) + } RosterObserved { observed_on: _, registrations: regs } => fold( regs, @@ -264,12 +279,23 @@ fn accumulate_connectivity_action( } } +// A TRUNCATED ROSTER STILL PLANS REPAIRS, AND THAT IS THE POINT. Refusing here would replace a +// fail-open with a fail-shut that stops reconciliation on every host the read DID cover. Slots +// inside the prefix are still planned normally; slots the read never reached answer +// SlotConnectivityUnknown at runner_slot_connectivity_verdict_for_incarnation, which yields no +// replace action -- so the false restart is cut at the verdict rather than by widening here. fn connectivity_actions_for_observed( roster: OrganizationRunnerRosterEvidence, observed: List, ) -> ConnectivityActionsOutcome { match roster { RosterReadUnavailable { reason: r } => ConnectivityActionsRosterUnavailable { reason: r } + RosterObservedPartial { observed_on: _, registrations: _, observed_count: _, authority_total: _ } => + fold( + observed, + init: ConnectivityActionsPlanned { actions: [] }, + f: (acc, slot) => accumulate_connectivity_action(roster: roster, acc: acc, slot: slot) + ) RosterObserved { observed_on: _, registrations: _ } => fold( observed, diff --git a/dag/test/claim/fleet_runner_connectivity_witness_test.dag b/dag/test/claim/fleet_runner_connectivity_witness_test.dag index 2234593c36f..cf9c21213a0 100644 --- a/dag/test/claim/fleet_runner_connectivity_witness_test.dag +++ b/dag/test/claim/fleet_runner_connectivity_witness_test.dag @@ -1,7 +1,7 @@ module test.claim.fleet_runner_connectivity_witness import std.logic { Bool } -import std.types { String, List } +import std.types { String, NonEmptyStr, List } import std.nat { Nat } import gunbc.build_cache_instance { RunnerSlotIdentity } import gunbc.fleet_intent_network { @@ -24,7 +24,10 @@ import gunbc.fleet_runner_connectivity { runner_slot_incarnation, incident_2026_08_06_registrations, RosterObserved, + RosterObservedPartial, RosterReadUnavailable, + OrganizationRunnerRosterEvidence, + organization_runner_roster_from_page, AchievedWidthsObserved, AchievedWidthsUnobserved, SlotConnectivityHealthy, @@ -168,3 +171,85 @@ fn count_matching( f: (n, v) => if matched(v) { n + 1 } else { n } ) } + + +// --------------------------------------------------------------------------- +// TRUNCATED ROSTER: the discriminating pair for the paginated-read repair. +// +// The org runners API is paginated. Measured 2026-08-27T21:29Z: total_count 522 +// against a 100-row page. A read that SUCCEEDS is therefore not a read that saw +// everything, and the defect this pair pins is that a slot missing from a PREFIX +// was never observed to be missing -- rendering it Orphaned is the empty-observation +// narrow, and Orphaned is what maps to a restart at +// gunbc.runner_capacity_plan connectivity_replace_action. +// +// THE PAIR IS THE POINT. The RED arm alone would also pass if Orphaned had simply +// been disabled everywhere, so the complete-roster control is what makes it +// discriminating rather than merely green. + +// BOTH FIXTURES DERIVE THEIR TOTAL FROM THE SPECIMEN, so neither can silently change meaning when +// a registration row is added. A hand-written total would make "partial" and "complete" facts about +// a literal someone remembered to update rather than facts about the pair. +fn truncated_incident_roster() -> OrganizationRunnerRosterEvidence { + organization_runner_roster_from_page( + observed_on: "2026-08-27" as NonEmptyStr, + registrations: incident_2026_08_06_registrations, + authority_total: incident_2026_08_06_registrations.length() + 1, + ) +} + +fn complete_incident_roster() -> OrganizationRunnerRosterEvidence { + organization_runner_roster_from_page( + observed_on: "2026-08-27" as NonEmptyStr, + registrations: incident_2026_08_06_registrations, + authority_total: incident_2026_08_06_registrations.length(), + ) +} + +// NO TRANSCRIBED COUNT. Asserting the specimen list's current length would pin a literal measured +// from the tree it is testing (DESIGN section 5 on oracles) and would rot the next time a +// registration row is added. The property under test is the RELATION: a page smaller than the +// authority's own total is partial, whatever either number happens to be. +test fn prefix_below_authority_total_is_partial() -> Bool { + match truncated_incident_roster() { + RosterObservedPartial { observed_on: _, registrations: _, observed_count: seen, authority_total: total } => + seen < total + _ => false + } +} + +test fn page_equal_to_authority_total_is_complete() -> Bool { + match complete_incident_roster() { + RosterObserved { observed_on: _, registrations: _ } => true + _ => false + } +} + +// THE RED. Before the repair every unseen slot rendered Orphaned here. +test fn truncated_roster_never_orphans_an_unseen_slot() -> Bool { + all( + connectivity_verdicts_for_active_incarnations(roster: truncated_incident_roster()), + v => !connectivity_verdict_is_orphaned(v: v) + ) +} + +// THE POSITIVE CONTROL. The required refusal must SURVIVE the repair: over a roster +// the authority itself calls complete, a slot with no registration is genuinely gone +// and must still be Orphaned. If this arm ever goes green-by-absence the RED above +// has stopped discriminating. +test fn complete_roster_still_orphans_an_unseen_slot() -> Bool { + !all( + connectivity_verdicts_for_active_incarnations(roster: complete_incident_roster()), + v => !connectivity_verdict_is_orphaned(v: v) + ) +} + +// PER-QUESTION, NOT PER-ROSTER. A truncated read still answers exactly about every +// slot INSIDE the prefix; refusing the whole roster would be a widen that stops +// reconciliation on hosts the read covered perfectly well. +test fn truncated_roster_still_answers_slots_inside_the_prefix() -> Bool { + !all( + connectivity_verdicts_for_active_incarnations(roster: truncated_incident_roster()), + v => connectivity_verdict_is_unknown(v: v) + ) +}