From b63a8fc4725e5ffbe212456eb75e218ca6f61d5d Mon Sep 17 00:00:00 2001 From: Ivan Anishchuk Date: Sun, 8 Nov 2026 16:46:49 +0530 Subject: [PATCH 1/2] test(yamux): wait for the pong deadline before the clock moves The keepalive check advanced the test clock past the pong deadline without waiting for the timer. The alarm reads the time, then arms a timer for the time left, and TestClock counts that from its own now. An advance that fell between the two steps left the timer due past the clock. The deadline never fired. The join waited forever, in about one run of the suite in fifty at four workers. The check now waits, through nextTimer, for the two timers the ping arms: the writer's deadline for its write, and the ticker's for the pong. TestClock's doc asks this of every advance, and every other advance in the suites already does it. The session code is unchanged: on the system clock the gap only makes a timer late by the time between the two steps, and no timer fires early. --- Tests/Yamux.lean | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/Tests/Yamux.lean b/Tests/Yamux.lean index b2113e02..25a43118 100644 --- a/Tests/Yamux.lean +++ b/Tests/Yamux.lean @@ -1186,9 +1186,11 @@ private def hostileChecks (r : Runner) : Async Unit := do raw.close -- A peer that never answers our keepalive: after the interval the -- session pings, and when the pong's deadline passes, it ends with a - -- fault and no go-away. The ticker reads the time when it arms its - -- timer, so a deadline the clock has passed already fires at once, - -- whichever runs first. + -- fault and no go-away. The ticker reads the time, then arms its timer + -- for the time left, and the test clock counts that from its own now. + -- An advance between the two steps would push the timer past the + -- clock, so each advance waits for the timers it must fire + -- (`TestClock.nextTimer`). do let tc ← TestClock.new let (raw, s) ← pair @@ -1199,6 +1201,12 @@ private def hostileChecks (r : Runner) : Async Unit := do let some (h, _, pending) ← readFrame raw .empty | throw <| IO.userError "no keepalive" r.check "hostile: after the interval with no bytes, the session pings" (h.type == .ping && h.flags.syn) + -- The ping arms two timers, in either order: the writer's deadline + -- for its write, and the ticker's for the pong. + let writeArmed ← tc.nextTimer + let pongArmed ← tc.nextTimer + r.check "hostile: the pong deadline is armed before the clock moves" + (writeArmed && pongArmed) tc.advance pingDeadlineMs let res ← try match ← server.join with From 2d85a0658b1ee12578b3c6f98c4a23d032483160 Mon Sep 17 00:00:00 2001 From: Leo Lara Date: Mon, 9 Nov 2026 09:50:35 +0700 Subject: [PATCH 2/2] test(yamux): make the keepalive armed check name both timers The check asserts that the writer's deadline and the pong deadline armed, but its message named only the pong. A run where the write timer missed its arming would print a message about the pong, and send the investigation the wrong way. The message now names both. --- Tests/Yamux.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Tests/Yamux.lean b/Tests/Yamux.lean index 25a43118..ad9e55c2 100644 --- a/Tests/Yamux.lean +++ b/Tests/Yamux.lean @@ -1205,7 +1205,7 @@ private def hostileChecks (r : Runner) : Async Unit := do -- for its write, and the ticker's for the pong. let writeArmed ← tc.nextTimer let pongArmed ← tc.nextTimer - r.check "hostile: the pong deadline is armed before the clock moves" + r.check "hostile: the ping arms its two timers before the clock moves" (writeArmed && pongArmed) tc.advance pingDeadlineMs let res ← try