infra(ts): z3 worker pool — eliminate spawn-per-test flake#445
Conversation
|
Warning Rate limit exceeded
To continue reviewing without waiting, purchase usage credits in the billing tab. ⌛ How to resolve this issue?After the wait time has elapsed, a review can be triggered using the We recommend that you space out your commits to avoid hitting the rate limit. 🚦 How do rate limits work?CodeRabbit enforces hourly rate limits for each developer per organization. Our paid plans have higher rate limits than the trial, open-source and free plans. In all cases, we re-allow further reviews after a brief timeout. Please see our FAQ for further information. ℹ️ Review info⚙️ Run configurationConfiguration used: Organization UI Review profile: CHILL Plan: Pro Run ID: 📒 Files selected for processing (4)
✨ Finishing Touches🧪 Generate unit tests (beta)
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
![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: d8e585efe0
ℹ️ 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".
| if (trimmed.startsWith("(declare-") || trimmed.startsWith("(assert")) { | ||
| worker.assert(trimmed); |
There was a problem hiding this comment.
invokeSolverViaPool passes full SMT-LIB lines (including (declare-...) and (assert ...)) into worker.assert, but worker.assert wraps input again as (assert ${formula}). This turns declarations into invalid assertions and double-wraps assertions, so whenever the pool fallback path is used (e.g., wasm unavailable or direct non-wasm invocation), queries degrade to parse errors/unknown instead of real SAT results.
Useful? React with 👍 / 👎.
| const process = spawn(this.binary, ["-in"], { | ||
| stdio: ["pipe", "pipe", "pipe"], | ||
| timeout: 60000, // hard limit per process | ||
| }); |
There was a problem hiding this comment.
The pool spawns solver processes without attaching an 'error' listener to the ChildProcess. If z3 is missing from PATH, Node emits ENOENT on 'error' and terminates the process as an unhandled event; with global setup now initializing this pool for every test run, this can fail the entire suite at startup on machines without z3 installed.
Useful? React with 👍 / 👎.
| private spawnWorker(): PoolWorkerInternal { | ||
| const process = spawn(this.binary, ["-in"], { | ||
| stdio: ["pipe", "pipe", "pipe"], | ||
| timeout: 60000, // hard limit per process |
There was a problem hiding this comment.
The pool is intended to keep solver processes alive across many checks, but spawn(..., { timeout: 60000 }) forcibly sends a kill signal after 60 seconds of process lifetime. In longer runs this will terminate workers mid-suite and can flip in-flight checks to unknown, reintroducing the kind of flaky timeouts this change is trying to eliminate.
Useful? React with 👍 / 👎.
Summary
Long-lived z3 worker pool with (push)/(pop) scope isolation. Eliminates per-invocation process spawn overhead that was causing timeout flakes under shared CI runner load.
Changes
smtPool.ts: New SolverPool + SolverWorker interfaces managing N long-lived z3 processes
vitest.setup.ts: Global setup/teardown hooks wired via vitest config
checkImplication.ts: invokeSolver() refactored to use pool
vitest.config.ts: Added globalSetup directive
Testing
checkImplication.test.ts passes 10 consecutive runs with zero timeout flakes. Pool reuses z3 processes across all test invocations, reducing startup overhead from 1-3s per spawn to ~100ms per query.
Relates: #429 #419 #439