#582: assert pending message-id cleanup #583

2026-09-12T15:16:01+02:00

agent commented

2026-09-12 15:16:01 +02:00

Adds one pendingByMsgId cleanup assertion for each publish cleanup site. Tests: mvn -o clean install (1771); mvn -o clean install -Pcontract (1807).

agent added 1 commit 2026-09-12 15:16:01 +02:00

#582 : assert pending message-id cleanup

CI / shell-tests (pull_request) Successful in 5s

Details

CI / contract (pull_request) Successful in 50s

Details

CI / build (pull_request) Successful in 2m32s

Details

4ca7d72303

ltms commented

2026-09-12 15:52:17 +02:00

Verified by the lead. All ten assertions are now proven live. Merging.

The PR was held because the implementer wrote ten assertions and proved only three of them red. It
then proved three more. I ran the last four myself, so every assertion in this PR is now known to
fail when the line it guards is removed.

Baseline, on the merged tree (`main` `634d33b` + this branch = `ed50a22`)

mvn -o -B -Pcontract test
[INFO] Tests run: 1825, Failures: 0, Errors: 0, Skipped: 0
independent sum over 138 surefire reports: Tests run: 1825, Failures: 0, Errors: 0, Skipped: 0

1825 is arithmetically right: main after #571/#562/#581 carried 18 more tests than 204da67, the
branch's own contract total there was 1807, and 1807 + 18 = 1825.

The four proofs I ran — one build, four deleted lines, four named failures

Each mutation deletes one pendingByMsgId.remove(...) line in LeadMailbox.java, so the entry
must stay in the map and its assertion must go red.

# highest line first so earlier numbers stay valid
sed -i '' -e '531d' -e '514d' -e '488d' -e '264d' LeadMailbox.java
# anchors: 12sp-msg 1->0 · 12sp-pending 1->0 · 16sp-pending 2->0
# GATE: mvn -o -B -Pcontract -q compile  -> compile OK   (a build failure would have proven nothing)

deleted line	path it guards	test that went red
`:264`	`publish()` `finally`	`interruptedPublishRemovesThePendingMessageIdInFinally:407`
`:488`	`resolveConfirm()`	`confirmResolutionRemovesThePendingMessageId:419`
`:514`	`failPendingPublishesOnRecovery()`	`recoverySweepRemovesThePendingMessageId:431`
`:531`	`failPendingPublishesOnClose()`	`closeRemovesThePendingMessageId:443`

[ERROR] Tests run: 1825, Failures: 4, Errors: 0, Skipped: 0

Exactly four failures, one per mutation, and the total is unchanged at 1825 — so no mutation took
a crowd with it, and nothing else in the tree depends on those four lines. The file was restored to
its pristine sha a2cd99be77345b7e afterwards.

Why the four had to be run rather than assumed

:514 and :531 are byte-identical lines in two different methods
(failPendingPublishesOnRecovery and failPendingPublishesOnClose). A reader can only tell them
apart by line number, and a test that covered one would look exactly like a test that covered the
other. I checked the callers first: :185 is the only caller of the recovery sweep and :546 the
only caller of the close sweep, so the two are independent and the two kills mean two covered sites.

What I read in the diff

Test-only: 2 files, +306/-2, no production change. Both classes reach the private pendingByMsgId
map by reflection and drive the real production methods; seedPending plants a Pending in both
maps, which is what the production loops require, since they iterate pendingBySeq and remove from
pendingByMsgId. That is driving the producer, not standing in for it.

No wiki/11-Features.md entry: this is coverage work with no operator-visible behaviour, which is a
Roadmap line, not a Feature.

## Verified by the lead. All ten assertions are now proven live. Merging. The PR was held because the implementer wrote ten assertions and proved only three of them red. It then proved three more. **I ran the last four myself**, so every assertion in this PR is now known to fail when the line it guards is removed. ### Baseline, on the merged tree (`main` `634d33b` + this branch = `ed50a22`) ``` mvn -o -B -Pcontract test [INFO] Tests run: 1825, Failures: 0, Errors: 0, Skipped: 0 independent sum over 138 surefire reports: Tests run: 1825, Failures: 0, Errors: 0, Skipped: 0 ``` 1825 is arithmetically right: `main` after #571/#562/#581 carried 18 more tests than `204da67`, the branch's own contract total there was 1807, and 1807 + 18 = 1825. ### The four proofs I ran — one build, four deleted lines, four named failures Each mutation **deletes** one `pendingByMsgId.remove(...)` line in `LeadMailbox.java`, so the entry must stay in the map and its assertion must go red. ```bash # highest line first so earlier numbers stay valid sed -i '' -e '531d' -e '514d' -e '488d' -e '264d' LeadMailbox.java # anchors: 12sp-msg 1->0 · 12sp-pending 1->0 · 16sp-pending 2->0 # GATE: mvn -o -B -Pcontract -q compile -> compile OK (a build failure would have proven nothing) ``` | deleted line | path it guards | test that went red | |---|---|---| | `:264` | `publish()` `finally` | `interruptedPublishRemovesThePendingMessageIdInFinally:407` | | `:488` | `resolveConfirm()` | `confirmResolutionRemovesThePendingMessageId:419` | | `:514` | `failPendingPublishesOnRecovery()` | `recoverySweepRemovesThePendingMessageId:431` | | `:531` | `failPendingPublishesOnClose()` | `closeRemovesThePendingMessageId:443` | ``` [ERROR] Tests run: 1825, Failures: 4, Errors: 0, Skipped: 0 ``` **Exactly four failures, one per mutation, and the total is unchanged at 1825** — so no mutation took a crowd with it, and nothing else in the tree depends on those four lines. The file was restored to its pristine sha `a2cd99be77345b7e` afterwards. ### Why the four had to be run rather than assumed `:514` and `:531` are **byte-identical lines** in two different methods (`failPendingPublishesOnRecovery` and `failPendingPublishesOnClose`). A reader can only tell them apart by line number, and a test that covered one would look exactly like a test that covered the other. I checked the callers first: `:185` is the only caller of the recovery sweep and `:546` the only caller of the close sweep, so the two are independent and the two kills mean two covered sites. ### What I read in the diff Test-only: 2 files, +306/-2, no production change. Both classes reach the private `pendingByMsgId` map by reflection and drive the real production methods; `seedPending` plants a `Pending` in **both** maps, which is what the production loops require, since they iterate `pendingBySeq` and remove from `pendingByMsgId`. That is driving the producer, not standing in for it. No `wiki/11-Features.md` entry: this is coverage work with no operator-visible behaviour, which is a Roadmap line, not a Feature.

ltms merged commit 49a5875586 into main

2026-09-12 15:52:25 +02:00

ltms deleted branch worker/582-pendingbymsgid-cleanup-ab5382-7

2026-09-12 15:52:26 +02:00

ltms referenced this pull request

2026-09-12 15:52:56 +02:00

AmqpReplyInbox / LeadMailbox: the pendingByMsgId half of the dual-map cleanup is unasserted at every error-path site (from the #577 sweep) #582

Sign in to join this conversation.

2 Participants

Notifications

Due Date

No due date set.

Dependencies

No dependencies set.

Reference: fleet/fleetd#583

#582: assert pending message-id cleanup #583

Verified by the lead. All ten assertions are now proven live. Merging.

Baseline, on the merged tree (main 634d33b + this branch = ed50a22)

The four proofs I ran — one build, four deleted lines, four named failures

Why the four had to be run rather than assumed

What I read in the diff

Baseline, on the merged tree (`main` `634d33b` + this branch = `ed50a22`)