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

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
113 changes: 102 additions & 11 deletions dag/gunbc/fleet_runner_connectivity.dag
Original file line number Diff line number Diff line change
Expand Up @@ -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<GitHubSelfHostedRunnerRegistration> }
| RosterObservedPartial {
observed_on: NonEmptyStr
registrations: List<GitHubSelfHostedRunnerRegistration>
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<GitHubSelfHostedRunnerRegistration>,
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
Expand Down Expand Up @@ -359,6 +390,42 @@ fn local_runner_slot_incarnations() -> List<LocalRunnerSlotIncarnation> {
)
}

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<GitHubSelfHostedRunnerRegistration>,
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,
Expand All @@ -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),
},
)
}
}
}
Expand Down Expand Up @@ -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(),
Expand Down Expand Up @@ -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 {
Expand All @@ -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
}
}
26 changes: 26 additions & 0 deletions dag/gunbc/runner_capacity_plan.dag
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down Expand Up @@ -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,
Expand Down Expand Up @@ -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<RunnerSlotIdentity>,
) -> 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,
Expand Down
87 changes: 86 additions & 1 deletion dag/test/claim/fleet_runner_connectivity_witness_test.dag
Original file line number Diff line number Diff line change
@@ -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 {
Expand All @@ -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,
Expand Down Expand Up @@ -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)
)
}
Loading