Trial P-44 (pass): one Run holds the lane and at most one waits; the fake's lane does the same

Merged
DO
5d ago
+12370-15

Trial P-44, by the working rulings on #251: with a concurrency group for each Work item, does GitHub keep one Run running and one pending, cancel the older pending Run, and never cancel the one running? Yes. The trial passes. The lane in the fake now does the same, as ruling 2 asks.

What ran, and what it showed

The trial ran on the canary, through the Maintainer's login. The workflow ran on one branch, trial/p-44, with one job:

  • granted nothing, holding no secret, checking nothing out and caching nothing;
  • sleeping ninety seconds under concurrency: {group: lane-p44, cancel-in-progress: false}.

Four pushes went in ten seconds apart, and the run list was read every fifteen seconds until all four concluded.

RunConclusionJob
1successhad a runner and three steps
2cancelled, when run 3 queuedno runner, no step
3cancelled, when run 4 queuedno runner, no step
4success, started when run 1 endedhad a runner and three steps

At every read, at most one run was in progress and at most one waited. GitHub lists the waiting one as pending. The trigger was a push. The Factory's Run is a dispatch, but a group applies to a job whatever started its workflow. The branch, and the workflow with it, is deleted.

What changes

  • trials/P-44.json. 894 KB of GitHub's run lists and jobs. Its last exchange computes the three parts of the pass.
  • sim/grounding.py. a_run_waits_its_turn says what P-44 shows, and names the fixture:
    • one Run holds the lane and at most one waits;
    • a newer Run cancels the one waiting, which never starts, and never the one running.
  • sim/world.py and sim/issues.py. Both worlds queue a Run through enqueue().
    • The group's first Run holds it, in progress or waiting for a runner.
    • A Run waiting behind that one is cancelled as a newer one queues, and is read as superseded, so it is no attempt.
    • Each world checks that no more than one Run waits behind the one that holds the lane.
    • That the first Run holds the group while it waits for a runner is GitHub's documented rule. P-44 did not need to show it, since its first run was in progress at once.
  • The design.
    • §3's outcomes say a Run cancelled before its job had a runner or a step is superseded, no attempt. A person's cancel reads the same, and is bounded by the Run ceiling.
    • The records port reads pending as queued.
    • §6's P-44 row records the pass.
  • sim/AGENTS.md. The lane leaves "Known to differ", and the lane's test is named.
  • Tests and mutants.
    • A test of each world's lane, the empty lane included, and on a pinned seed of each world.
    • A test that computes the pass from the fixture's run lists and jobs, and holds the workflow's group to the blob the upload answered with.
    • Eight mutants, each killed.
  • One coverage test pins a seed. The first seed on which a Hold takes an item out of the queue moved from 39 to 109, so it is run as a pinned seed and a local run of forty seeds still asks for it.

Reviews and verification

  • make verify passed in the worktree with history, at SIM_SEEDS=40: 862 tests. Both simulators passed at 300 seeds, as CI runs them. The mutation run is CI's, and every lane mutant was checked by hand.
  • Muse (Wonder Full) on 0e06e2d found two majors, both fixed in 60c88c1:
    • The fake cancelled the Run that holds the group when nothing was in progress, which GitHub would start. That was nearly every cancellation on the seeds.
    • The empty lane was not tested.
      Muse also found the Kernel safe: a cancelled Run read as superseded admits nothing it should not, and holds early if anything.
  • AGY (Gemini 3.8 Flash) found:
    • The call sites were unheld. This is fixed.
    • A cancelled Run spends an adjudication round. This is the Kernel's reading of every superseded Run today. It holds early, never late, and this pull request does not change it.
  • A fresh Claude review with a security pass found two majors, the call sites and a design rule that named no test. Both are fixed, along with its minors.

Part of #251. P-45 waits on the Maintainer's word on Dependabot for the canary.

🤖 Generated with Claude Code