[IvanAnishchuk]

Summary

The test binary hung in about one run in fifty at 4 workers. The cause is the keepalive check of the yamux suite: it advanced the test clock past the pong deadline without waiting for the timer, as TestClock.nextTimer asks of every advance. This PR adds the wait. The session code does not change.

What changed

Tests/Yamux.lean, the keepalive check of hostileChecks:

• Before the advance of pingDeadlineMs, the check waits through tc.nextTimer for the two timers the keepalive ping arms: the writer's deadline for its write, and the ticker's deadline for the pong. A new check records that both armed.
• The block comment now states the race. The old one said "a deadline the clock has passed already fires at once, whichever runs first". That holds only when the advance comes before the ticker reads the time.

The race

Conc.Alarm.run reads clock.nowMs, then arms clock.after (due - now). TestClock.after counts the wait from the clock's now at the moment of arming. When the test's advance fell between the read and the arming, the pong timer was due at I + 2P on a clock that stopped at I + P. The tick never came, and server.join waited forever with every task parked.

On the system clock the same gap only makes a timer late by the time between the two steps, and the clock contract allows a late timer ("no timer fires early"). So the session is correct, and the test broke the documented TestClock rule. Every other advance in Tests/ already waits on nextTimer, or arms its timer in the test itself.

How it was found: under gdb, one hung run showed main waiting in Conc.Async.run, every pool worker idle, and libuv with no work. Stderr markers per section, then per check group, then per block narrowed it to this check on hackathon26 itself (hangs at runs 2, 26, and 146 of the marked loops).

Test plan

• lake build --wfail is green.
• lake test passes: 27170 passed, 0 failed, 10 skipped. It passes again with LEAN_NUM_THREADS=1.
• Stress at 4 workers: 250 of 250 plain runs pass, each under a 60 s timeout. Without the fix, the same loop hung at runs 2, 26, and 146.
• The import-rule lint is green: 163 modules, 0 violations.

Risk / trust footprint

None. The change is in a test.

Notes for reviewers

• Found while testing refactor(negotiate): run the upgrader over the seam types of libp2p/core #82, and unrelated to its change: this check and the alarm are the same on hackathon26. It is the hang that refactor(negotiate): run the upgrader over the seam types of libp2p/core #82's description notes.

LICENSE (LGPL version 3)

• I have read and accepted LICENSE (LGPL version 3), NOTICE and CLA in the root of this project.

[leolara]

Reviewed at 2d85a06. I rebased the branch onto origin/hackathon26 (5fa9e63, which carries the merged #84); the rebase was clean. The branch now holds the author's commit b63a8fc and one nit commit of mine, 2d85a06, pushed to the fork.

Test-only. Both commits touch Tests/Yamux.lean alone. The session code does not change.

The race, checked against the code. Alarm.run reads clock.nowMs (packages/base/conc/Conc/Alarm.lean:87), then arms clock.after left (Alarm.lean:88). TestClock.after counts the due time from the clock's now at the moment of arming (packages/base/conc/Conc/Clock.lean:142). An advance that lands between the read and the arming leaves the pong timer due at I + 2P on a clock that stops at I + P, so the tick never comes. The rewritten block comment (Tests/Yamux.lean:1189 to 1193) states this correctly, and it drops the old claim that a passed deadline fires at once, which held only when the advance came first.

The wait semantics, checked. The keepalive ping arms exactly two timers: the writer's write deadline, which withinDeadline arms for every write, parked or not (packages/base/conc/Conc/Deadline.lean:94, packages/net/yamux/Yamux/Loop.lean:592), and the pong deadline, which the ticker's alarm arms through .wakeAt (packages/net/yamux/Yamux/Loop.lean:425). Both durations are pingDeadlineMs, and pingDeadlineMs := writeDeadlineMs (packages/net/yamux/Yamux/Constants.lean:98), so the single advance pingDeadlineMs fires both. nextTimer returns only after the atomic arming step has put the timer in the list, so each waited timer counts its due time from the time before the advance, and both fire. The new check at Tests/Yamux.lean:1206 to 1209 asserts that both armed.

Other advances in the file. Tests/Yamux.lean has three advance calls, and each has its wait: line 1182 waits through the counting loop at lines 1178 to 1179, line 1200 waits at line 1199, and line 1210 waits through the new checks. None violates the TestClock rule.

Nit, fixed and pushed. The new check's message named only the pong deadline, while its condition asserts both timers. A run where the write timer missed its arming would have printed a message about the pong, and sent the investigation the wrong way. Commit 2d85a06 rewords the message to name both.

Checks I ran. lake build --wfail is green (253 jobs). lake test gives 27189 passed, 0 failed, 10 skipped, and the same summary under +RTS -N1 -RTS. scripts/lint-imports.sh reports 160 modules, 0 violations. No sorry in the touched file, and the change is test-only, so no axiom audit.

Stress. I ran the test binary 30 times at default workers, each under a 60 s timeout: 30 of 30 pass. That is on top of the two lake test runs above. I did not repeat the body's full 250-run loop; the mechanism above is the evidence I relied on.

The fix restores the documented rule every other advance follows, and the hang at the merged tip goes with it.

APPROVE