Reduce use of event-dispatch thread (EDT) from I/Q#207
Draft
hanno-becker wants to merge 2 commits intomainfrom
Draft
Reduce use of event-dispatch thread (EDT) from I/Q#207hanno-becker wants to merge 2 commits intomainfrom
hanno-becker wants to merge 2 commits intomainfrom
Conversation
Several MCP tool handlers blocked the EDT to obtain snapshots they only read. Use PIDE.session.snapshot(node_name) directly from the worker thread instead. Name worker threads iq-worker-N, set daemon + MIN_PRIORITY so the OS scheduler prefers the EDT when CPU is contended. Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>
Theory completion, command retrieval, and stable-snapshot waits all polled with Thread.sleep, stalling the calling thread and — in some paths — the EDT. jEdit would freeze for the duration of long-running proof checks. Subscribe to Session.Commands_Changed and count down a latch when the target condition is met. Re-check immediately after subscribing to close the TOCTOU window. Add PIDE.editor.flush() after write_to_theory so PIDE.session.snapshot() reflects the pending edit without an EDT round-trip. Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>
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.
[refactor] I/Q: Avoid EDT for read-only PIDE snapshots
Several MCP tool handlers blocked the EDT to obtain snapshots they
only read. Use PIDE.session.snapshot(node_name) directly from the
worker thread instead.
Name worker threads iq-worker-N, set daemon + MIN_PRIORITY so the
OS scheduler prefers the EDT when CPU is contended.
I/Q: Replace polling loops with event-driven waiting
Theory completion, command retrieval, and stable-snapshot waits all
polled with Thread.sleep, stalling the calling thread and — in some
paths — the EDT. jEdit would freeze for the duration of long-running
proof checks.
Subscribe to Session.Commands_Changed and count down a latch when
the target condition is met. Re-check immediately after subscribing
to close the TOCTOU window. Add PIDE.editor.flush() after
write_to_theory so PIDE.session.snapshot() reflects the pending
edit without an EDT round-trip.