From 88612e329e8ec66204f59482b251ba6e129da9f8 Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Fri, 31 Jul 2026 12:00:04 -0700 Subject: [PATCH] Export `killThreads` from z3-solver to allow Node.js thread cleanup (#10320) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Emscripten worker threads spawned for long-running Z3 operations (e.g. `solver.check()`) are never cleaned up, keeping the Node.js process alive after Z3 is done. The `killThreads` helper already existed internally in `jest.ts` but was never part of the public package. ## Changes - **`src/kill-threads.ts`** (new) — extracts `killThreads(em)` into a standalone module; calls `em.PThread.terminateAllThreads()` then polls until all workers are gone (5 s timeout) - **`src/node.ts`** — re-exports `killThreads` so it is part of the published `z3-solver` API - **`src/jest.ts`** — simplified to re-export from `./kill-threads` instead of duplicating ~45 lines - **`src/kill-threads.test.ts`** (new) — unit tests for the exported function - **`PUBLISHED_README.md`** — documents the new API ## Usage ```typescript import { init, killThreads } from 'z3-solver'; const api = await init(); // ... use Z3 ... await killThreads(api.em); ``` - Fixes #7070 --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> --- src/api/js/PUBLISHED_README.md | 12 +++++++- src/api/js/src/jest.ts | 46 +---------------------------- src/api/js/src/kill-threads.test.ts | 45 ++++++++++++++++++++++++++++ src/api/js/src/kill-threads.ts | 43 +++++++++++++++++++++++++++ src/api/js/src/node.ts | 1 + 5 files changed, 101 insertions(+), 46 deletions(-) create mode 100644 src/api/js/src/kill-threads.test.ts create mode 100644 src/api/js/src/kill-threads.ts diff --git a/src/api/js/PUBLISHED_README.md b/src/api/js/PUBLISHED_README.md index 85987ba7a2..bd11ae9769 100644 --- a/src/api/js/PUBLISHED_README.md +++ b/src/api/js/PUBLISHED_README.md @@ -27,7 +27,17 @@ const api = await init({ }); ``` -### Limitations +### Thread cleanup (Node.js) + +Long-running Z3 operations run on background worker threads. In Node.js, these workers keep the process alive even after Z3 has finished. Once you are done using Z3, call `killThreads` to terminate them and allow the process to exit cleanly. + +```typescript +import { init, killThreads } from 'z3-solver'; + +const api = await init(); +// ... use Z3 ... +await killThreads(api.em); +``` The package requires threads, which means you'll need to be running in an environment which supports `SharedArrayBuffer`. In browsers, in addition to ensuring the browser has implemented `SharedArrayBuffer`, you'll need to serve your page with [special headers](https://web.dev/coop-coep/). There's a [neat trick](https://github.com/gzuidhof/coi-serviceworker) for doing that client-side on e.g. Github Pages, though you shouldn't use that trick in more complex applications. diff --git a/src/api/js/src/jest.ts b/src/api/js/src/jest.ts index 7e8ed3f9ed..bcd07f4bd2 100644 --- a/src/api/js/src/jest.ts +++ b/src/api/js/src/jest.ts @@ -8,6 +8,7 @@ import initModule = require('../build/z3-built'); export * from './high-level/types'; export { Z3Core, Z3LowLevel } from './low-level'; export * from './low-level/types.__GENERATED__'; +export { killThreads } from './kill-threads'; export async function init(): Promise { const lowLevel = await initWrapper(initModule); @@ -15,48 +16,3 @@ export async function init(): Promise { return { ...lowLevel, ...highLevel }; } -function delay(ms: number): Promise & { cancel(): void }; -function delay(ms: number, result: Error): Promise & { cancel(): void }; -function delay(ms: number, result: T): Promise & { cancel(): void }; -function delay(ms: number, result?: T | Error): Promise & { cancel(): void } { - let handle: any; - const promise = new Promise( - (resolve, reject) => - (handle = setTimeout(() => { - if (result instanceof Error) { - reject(result); - } else if (result !== undefined) { - resolve(result); - } - resolve(); - }, ms)), - ); - return { ...promise, cancel: () => clearTimeout(handle) }; -} - -function waitWhile(premise: () => boolean, pollMs: number = 100): Promise & { cancel(): void } { - let handle: any; - const promise = new Promise(resolve => { - handle = setInterval(() => { - if (premise()) { - clearTimeout(handle); - resolve(); - } - }, pollMs); - }); - return { ...promise, cancel: () => clearInterval(handle) }; -} - -export function killThreads(em: any): Promise { - em.PThread.terminateAllThreads(); - - // Create a polling lock to wait for threads to return - // TODO(ritave): Threads should be killed automatically, or there should be a better way to wait for them - const lockPromise = waitWhile(() => !em.PThread.unusedWorkers.length && !em.PThread.runningWorkers.length); - const delayPromise = delay(5000, new Error('Waiting for threads to be killed timed out')); - - return Promise.race([lockPromise, delayPromise]).finally(() => { - lockPromise.cancel(); - delayPromise.cancel(); - }); -} diff --git a/src/api/js/src/kill-threads.test.ts b/src/api/js/src/kill-threads.test.ts new file mode 100644 index 0000000000..20e0adee36 --- /dev/null +++ b/src/api/js/src/kill-threads.test.ts @@ -0,0 +1,45 @@ +import { killThreads } from './kill-threads'; + +describe('killThreads', () => { + it('calls terminateAllThreads and resolves when workers are already gone', async () => { + const unusedWorkers: unknown[] = []; + const runningWorkers: unknown[] = []; + const mockEm = { + PThread: { + terminateAllThreads: jest.fn(), + get unusedWorkers() { + return unusedWorkers; + }, + get runningWorkers() { + return runningWorkers; + }, + }, + }; + + await killThreads(mockEm); + + expect(mockEm.PThread.terminateAllThreads).toHaveBeenCalledTimes(1); + }); + + it('resolves once running workers are terminated', async () => { + const runningWorkers: unknown[] = [{}]; + const mockEm = { + PThread: { + terminateAllThreads: jest.fn(), + unusedWorkers: [] as unknown[], + get runningWorkers() { + return runningWorkers; + }, + }, + }; + + // Simulate workers being terminated after a short delay. + setTimeout(() => { + runningWorkers.length = 0; + }, 150); + + await killThreads(mockEm); + + expect(mockEm.PThread.terminateAllThreads).toHaveBeenCalledTimes(1); + }); +}); diff --git a/src/api/js/src/kill-threads.ts b/src/api/js/src/kill-threads.ts new file mode 100644 index 0000000000..23469fda38 --- /dev/null +++ b/src/api/js/src/kill-threads.ts @@ -0,0 +1,43 @@ +/** + * Terminates all Emscripten worker threads spawned by Z3. + * + * Long-running Z3 operations (such as `solver.check()`) run on background + * worker threads. In Node.js these workers keep the process alive even after + * Z3 has finished. Call this function once you are done using Z3 to allow the + * Node.js process to exit cleanly. + * + * ```typescript + * import { init, killThreads } from 'z3-solver'; + * + * const api = await init(); + * // ... use Z3 ... + * await killThreads(api.em); + * ``` + * @category Global + */ +export function killThreads(em: any): Promise { + em.PThread.terminateAllThreads(); + + // Poll until all workers have been terminated. + let intervalHandle: ReturnType; + let timeoutHandle: ReturnType; + + const lockPromise = new Promise(resolve => { + intervalHandle = setInterval(() => { + if (!em.PThread.unusedWorkers.length && !em.PThread.runningWorkers.length) { + clearInterval(intervalHandle); + clearTimeout(timeoutHandle); + resolve(); + } + }, 100); + }); + + const delayPromise = new Promise((_, reject) => { + timeoutHandle = setTimeout(() => { + clearInterval(intervalHandle); + reject(new Error('Waiting for threads to be killed timed out')); + }, 5000); + }); + + return Promise.race([lockPromise, delayPromise]); +} diff --git a/src/api/js/src/node.ts b/src/api/js/src/node.ts index a2e4f3e0c1..755808159a 100644 --- a/src/api/js/src/node.ts +++ b/src/api/js/src/node.ts @@ -6,6 +6,7 @@ import { init as initWrapper, Z3LowLevel, Z3ModuleOverrides } from './low-level' export * from './high-level/types'; export { Z3Core, Z3LowLevel } from './low-level'; export * from './low-level/types.__GENERATED__'; +export { killThreads } from './kill-threads'; /** * The main entry point to the Z3 API