fix(proxy): name the pre-response eventless timeout honestly and derive its budget from settings - #1633
Open
Komzpa wants to merge 9 commits into
Open
fix(proxy): name the pre-response eventless timeout honestly and derive its budget from settings#1633Komzpa wants to merge 9 commits into
Komzpa wants to merge 9 commits into
Conversation
github-actions
Bot
added
the
db migration
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 248ccfb7de
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
Komzpa
pushed a commit
that referenced
this pull request
Aug 6, 2026
Every new bug class extends the leg that should have caught it, so the three classes proven on the live stack today each get model state, an invariant or liveness property, and a negative control that reproduces the failure. Anchor account ownership (PR #1638). A continuity anchor now carries the account that owns it. Upstream accepts a request carrying a previous_response_id owned by a different account and then never sends response.created, so UpstreamRespondsTo gates StartStream, CompleteTurn and ClaimCompletedDelivery: a foreign-anchored turn can only leave the pre-response phase through a timer or a cancel. Inv10AnchorAccountOwnership forbids dispatching with a foreign-owned anchor; weak-cross-account-anchor.cfg reproduces the wedge. Pre-response eventless phase (PR #1633). The "active" phase - dispatched upstream, response.created not seen yet - now has its own bound instead of sharing the request/stream-idle budget, and ExpireDeadline picks both its bound and its budget label per phase. Inv11PreResponseBudget requires the pre-response bound to be the minimum of the named gate-retire and stream-idle budgets, at or above the keepalive cadence floor, strictly below the post-start budget, and forbids reporting a kill under the post-start stream-idle budget while the response had not started. weak-conflated-timers.cfg collapses the two timer names and TLC produces a healthy pre-start wait killed under the wrong budget. Bounded client retry backoff (PR #1634). A turn killed in the pre-response phase tears the client session; ClientRetryAttempt repairs it and is fair, but only while retryBackoff stays inside MaxRetryBackoff. The new liveness property TearEventuallyRecovers states that a recoverable tear is eventually recovered; weak-unbounded-backoff.cfg lets the backoff grow past every deadline in the model, and TLC produces a behaviour where the client stays torn forever - the 29-hour client sleep observed today. check.sh gains the three mappings and a PROPERTY:<Name> expectation form: a liveness control must violate exactly the temporal property its config declares and must not violate any invariant. bash spec/check.sh exits 0. Full model: 16696096 states generated, 3606740 distinct, depth 23, zero violations, deadlock checking enabled. All 13 weakenings produce their mapped counterexample.
Komzpa
force-pushed
the
bridge-eventless-semantics
branch
from
August 6, 2026 17:50
350c41e to
303742d
Compare
Komzpa
added a commit
that referenced
this pull request
Aug 6, 2026
Every new bug class extends the leg that should have caught it, so the three classes proven on the live stack today each get model state, an invariant or liveness property, and a negative control that reproduces the failure. Anchor account ownership (PR #1638). A continuity anchor now carries the account that owns it. Upstream accepts a request carrying a previous_response_id owned by a different account and then never sends response.created, so UpstreamRespondsTo gates StartStream, CompleteTurn and ClaimCompletedDelivery: a foreign-anchored turn can only leave the pre-response phase through a timer or a cancel. Inv10AnchorAccountOwnership forbids dispatching with a foreign-owned anchor; weak-cross-account-anchor.cfg reproduces the wedge. Pre-response eventless phase (PR #1633). The "active" phase - dispatched upstream, response.created not seen yet - now has its own bound instead of sharing the request/stream-idle budget, and ExpireDeadline picks both its bound and its budget label per phase. Inv11PreResponseBudget requires the pre-response bound to be the minimum of the named gate-retire and stream-idle budgets, at or above the keepalive cadence floor, strictly below the post-start budget, and forbids reporting a kill under the post-start stream-idle budget while the response had not started. weak-conflated-timers.cfg collapses the two timer names and TLC produces a healthy pre-start wait killed under the wrong budget. Bounded client retry backoff (PR #1634). A turn killed in the pre-response phase tears the client session; ClientRetryAttempt repairs it and is fair, but only while retryBackoff stays inside MaxRetryBackoff. The new liveness property TearEventuallyRecovers states that a recoverable tear is eventually recovered; weak-unbounded-backoff.cfg lets the backoff grow past every deadline in the model, and TLC produces a behaviour where the client stays torn forever - the 29-hour client sleep observed today. check.sh gains the three mappings and a PROPERTY:<Name> expectation form: a liveness control must violate exactly the temporal property its config declares and must not violate any invariant. bash spec/check.sh exits 0. Full model: 16696096 states generated, 3606740 distinct, depth 23, zero violations, deadlock checking enabled. All 13 weakenings produce their mapped counterexample.
Komzpa
force-pushed
the
bridge-eventless-semantics
branch
from
August 6, 2026 20:08
303742d to
4a94c36
Compare
Komzpa
force-pushed
the
bridge-eventless-semantics
branch
from
August 6, 2026 22:27
5e3cb70 to
588ecf7
Compare
Komzpa
added a commit
that referenced
this pull request
Aug 6, 2026
Every new bug class extends the leg that should have caught it, so the three classes proven on the live stack today each get model state, an invariant or liveness property, and a negative control that reproduces the failure. Anchor account ownership (PR #1638). A continuity anchor now carries the account that owns it. Upstream accepts a request carrying a previous_response_id owned by a different account and then never sends response.created, so UpstreamRespondsTo gates StartStream, CompleteTurn and ClaimCompletedDelivery: a foreign-anchored turn can only leave the pre-response phase through a timer or a cancel. Inv10AnchorAccountOwnership forbids dispatching with a foreign-owned anchor; weak-cross-account-anchor.cfg reproduces the wedge. Pre-response eventless phase (PR #1633). The "active" phase - dispatched upstream, response.created not seen yet - now has its own bound instead of sharing the request/stream-idle budget, and ExpireDeadline picks both its bound and its budget label per phase. Inv11PreResponseBudget requires the pre-response bound to be the minimum of the named gate-retire and stream-idle budgets, at or above the keepalive cadence floor, strictly below the post-start budget, and forbids reporting a kill under the post-start stream-idle budget while the response had not started. weak-conflated-timers.cfg collapses the two timer names and TLC produces a healthy pre-start wait killed under the wrong budget. Bounded client retry backoff (PR #1634). A turn killed in the pre-response phase tears the client session; ClientRetryAttempt repairs it and is fair, but only while retryBackoff stays inside MaxRetryBackoff. The new liveness property TearEventuallyRecovers states that a recoverable tear is eventually recovered; weak-unbounded-backoff.cfg lets the backoff grow past every deadline in the model, and TLC produces a behaviour where the client stays torn forever - the 29-hour client sleep observed today. check.sh gains the three mappings and a PROPERTY:<Name> expectation form: a liveness control must violate exactly the temporal property its config declares and must not violate any invariant. bash spec/check.sh exits 0. Full model: 16696096 states generated, 3606740 distinct, depth 23, zero violations, deadlock checking enabled. All 13 weakenings produce their mapped counterexample.
Komzpa
force-pushed
the
bridge-eventless-semantics
branch
from
August 7, 2026 01:26
d75844e to
350c41e
Compare
Komzpa
force-pushed
the
bridge-eventless-semantics
branch
from
August 7, 2026 08:12
cceac47 to
410bfae
Compare
…ream The HTTP responses bridge killed pre-`response.created` streams under the name `stream_idle_timeout`, whose configured budget (`stream_idle_timeout_seconds`, 7200s) governs only post-start gaps. The kill actually fired at the implicit `_STREAM_KEEPALIVE_MAX_COUNT (6) * sse_keepalive_interval_seconds (10s)` product, i.e. ~60s, derived from no configured timeout at all. It therefore raced and beat the owner-side `missing_response_created_timeout` gate and relabelled local bridge handoff wedges as upstream idle failures. Four local recovery paths compounded this by settling their own resets with "Upstream websocket closed before response.completed" when no upstream close happened. - Pre-response-start terminals now use a distinct `bridge_eventless_timeout` code across logs, request-log `failure_detail`/`failure_phase`, retry-circuit `last_detail`, the Prometheus surface label, and the client error. The retry-circuit detail is deliberately not aliased onto `stream_idle_timeout`. `stream_idle_timeout` is now reserved for post-start silence. - The client-visible shape stays retryable: 503 with a message stating no response was created upstream and the request is safe to retry. - The pre-response budget becomes the named, settings-derived `_http_bridge_eventless_budget_seconds` = min(stuck gate, stream idle, bridge request budget), aligning it with the 300s owner-side stuck gate. - Unmatched-but-live upstream frames emit an `unmatched_upstream_liveness` marker plus a per-session counter that the eventless timeout reports; locally injected `codex.keepalive` frames are excluded. - The four local reset sites say local bridge reset and stay account-health neutral for anchored `stream_incomplete` settlements.
…heads Merging origin/main brought `20260806_020000_add_usage_history_bulk_covering_indexes` into this branch. It revises the same parent as the already-shipped `20260806_120000_add_http_bridge_owner_process_epoch`, so the chain forked and the deploy preflight refused with `alembic_head_count_invalid expected=1 actual=2`. The owner-epoch revision id is already in production, so reparenting it is not an option. Add an empty merge revision recording the convergence instead. `ScriptDirectory.get_heads()` now returns exactly one head and `codex-lb-db check` reports `migration_policy=ok schema_drift=none`.
The five new pre-response-start regressions were appended to the end of tests/unit/test_proxy_http_bridge.py, which collides with PR #1630 appending its quarantine tests at the same spot. Move them (and their local _eventless_settings/_make_bridge_session helpers) into tests/unit/test_http_bridge_eventless_semantics.py so both branches can land. The two in-place assertion updates in test_proxy_http_bridge.py stay where they are; that file's tail is now byte-identical to its pre-branch state, so there is no append surface left to collide on.
Collaborator
Author
|
@codex review |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: d4354c3cfe
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
Comment on lines
+1251
to
+1254
| dead_owner_process_epoch_mismatch = ( | ||
| durable_lookup.owner_process_epoch is not None | ||
| and durable_lookup.owner_process_epoch != current_process_epoch | ||
| ) |
There was a problem hiding this comment.
In a multi-replica deployment, an active row owned by another instance normally has a process epoch different from this process, so this marks every remote owner as dead even when its lease and ring membership are current. For replay-safe full-resend requests, the branch at lines 1872–1889 consequently switches directly to account-neutral replay instead of forwarding to the live owner, potentially duplicating or forking a turn and changing its account; only compare owner_process_epoch when owner_instance_id == current_instance.
AGENTS.md reference: AGENTS.md:L105-L110
Useful? React with 👍 / 👎.
| settings, | ||
| fallback_seconds=interval_seconds * max(1, floor_count), | ||
| ) | ||
| return max(max(1, floor_count), math.ceil(budget_seconds / interval_seconds)) |
There was a problem hiding this comment.
When any configured eventless clamp is shorter than floor_count * keepalive_interval_seconds, this outer max makes the actual watchdog outlive the derived budget. For example, a 45-second idle/request budget with the default 10-second interval and floor 6 returns six ticks and waits about 60 seconds; a 20-second request budget is exceeded by roughly 40 seconds. Preserve the floor only when it does not violate the configured stuck-gate, idle, or request budget.
AGENTS.md reference: AGENTS.md:L129-L132
Useful? React with 👍 / 👎.
Comment on lines
3875
to
3878
| await self._record_http_bridge_retry_circuit_failure( | ||
| session, | ||
| detail="stream_idle_timeout", | ||
| detail=_HTTP_BRIDGE_EVENTLESS_TIMEOUT_DETAIL, | ||
| ) |
There was a problem hiding this comment.
For the normal hard-bridge pre-response timeout, this records another bridge_eventless_timeout failure but discards the returned consecutive-failure count and never calls _abandon_durable_http_bridge_continuity. The new poison threshold is checked only in the separate reader-failure path when an admission waiter exists, so repeated timeouts through this primary downstream watchdog can exceed the configured threshold indefinitely while the poisoned durable anchor remains reusable. Check the threshold here as well and clear continuity before retiring the session.
AGENTS.md reference: AGENTS.md:L105-L110
Useful? React with 👍 / 👎.
Owner
|
Triage follow-up (2026-08-10): CI is fully green and the branch is mergeable, but the latest codex review (2026-08-08) left three unresolved P-threads, which are merge blockers under the repo gate. Round 1 was addressed promptly in 5e3cb70 — appreciated — but there have been no pushes since the second review. Summarizing what's outstanding after verifying each finding against the PR head:
Two logistics notes: since this is stacked on #1625 (still open) and carries its two Alembic revisions (including the heads-merge migration), the maintainer will need to coordinate merge order — and the fix for (1) likely belongs in #1625's commits rather than this PR's. Once the three threads are addressed (or rebutted in-thread) and re-reviewed, this looks close to mergeable. |
13 tasks
Komzpa
added
the
needs rebase
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Stacked on #1625. An audit of today's live incident found the bridge conflating two different timers and blaming the upstream for local recovery:
response.createdsilence watchdog killed requests after an implicit6 x sse_keepalive_interval = ~60s, but emitted the kill asstream_idle_timeout— whose configured budget is 7200s. Zero-event bridge handoff wedges were logged as upstream stream failures all day (57/64 reader failures hadresponse_events_seen=0; successful luna turns' first event p95 is 930ms, so no healthy turn ever needed 60s).Changes
bridge_eventless_timeoutclassification for every pre-response terminal (logs, request-log detail, retry-circuitlast_detail, Prometheus surface label). Client shape stays a retryable 503 with an honest message.min(stuck_gate_retire_after_seconds, stream_idle_timeout_seconds, bridge_request_budget_seconds)(300s at defaults) — no more magic 60s;_STREAM_KEEPALIVE_MAX_COUNTis demoted to a keepalive-cadence floor. The owner-side missing-created watchdog still fires first on the common path, so recovery latency is unchanged — only the label is fixed.unmatched_upstream_liveness=Non the eventless terminal), distinguishing a local matching wedge from a genuinely silent upstream.codex.keepaliveis excluded.Verification: 744 passed across bridge regression files;
tests/unit5672 passed;tests/integrationhas only the pre-existing warm-now failure fixed separately in #1623; ruff, architecture check,openspec validate name-bridge-eventless-timeout --strict, and type check (no new diagnostics) all green. Five new behavior tests cover each fix, including a grep-style guard that local resets never blame the upstream again.