fix: make timers and signals safe against re-entrant continuations and lost signals - #15191
Open
algebraic-dev wants to merge 12 commits into
Open
algebraic-dev wants to merge 12 commits into
algebraic-dev wants to merge 12 commits into
Conversation
…ntinuations This PR fixes use-after-free crashes when a (sync := true) continuation of a timer or signal promise cancels or stops the handle, marks timer promises multi-threaded, restores timer state when starting fails, and no longer asserts when the caller resolved the promise itself. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
This PR makes a repeating libuv timer created with a 0 ms period keep ticking every millisecond instead of firing only once. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
This PR makes Signal.Waiter.selector report a waiter that already received its signal as ready. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
This PR corrects the libuv timer, signal and socket documentation to match their current behavior. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… numbers A signal selector that loses a select no longer misses a signal delivered before the next select, and selecting on a `Sleep` no longer cancels it, so it keeps its deadline across selects. Signal waiters now resolve with the signal number in Lean's `Signal` numbering instead of the operating system's, and a `Sleep` or `Interval` longer than a `UInt64` of milliseconds is clamped instead of wrapping to a short duration. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
`Signal.cancel` now only drops the pending promise and keeps the handler listening, and a signal that arrives with no promise pending is reported by the next `next` instead of being consumed. `Signal.Waiter.selector` goes back to cancelling on unregister, without the extra state it kept to avoid losing those signals. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
A `Sleep` whose selector loses a select is cancelled again, so the next select starts it from its full duration; the documentation of `Sleep.selector` now says so. This drops the separate `Selector.sleep` override that stopped one-off timers. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…-fixes # Conflicts: # src/Std/Internal/UV/UDP.lean
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
github-actions
Bot
added
the
toolchain-available
This branch has not been deployed
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
1 participant
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.
This PR fixes crashes in libuv timers and signals:
Timerwith a 0 ms period fired once and every later promise stayed pending. It now ticks every millisecond.Signal.cancelonly drops the pending promise and keeps the handler listening, and a signal that arrives with no promise pending resolves the promise of the nextnext.Signal.toInt32on every platform, instead of the operating system's number for that signal.