Fix ParallelPool timer threads keeping failed JVM runs alive

[mmv08]

Summary

Make ParallelPool's shared scoped-resource timer executor create daemon threads.

Motivation

ParallelPool.allocInScope keeps expensive closeable resources alive briefly after use, then schedules closeIfUnused to run after cvt.scoped.alloc.close.delay.

The scheduled executor used for this delayed cleanup was created with the default JVM thread factory. Those threads are non-daemon, so once the timer thread was created it could keep the JVM alive even after the prover's useful work had finished. This showed up in failed local/WSL runs that did not exit cleanly.

The timer is only housekeeping. It should not prevent JVM shutdown.

Change

globalTimers now uses a custom thread factory that marks timer threads as daemon threads.

This matches the existing treatment of other background pool infrastructure.

Reproduction

I reproduced the issue locally with a temporary child-JVM test like this:

class ParallelPoolShutdownTest {
    @Test
    fun scopedAllocationTimerDoesNotKeepJvmAlive() {
        val java = Path.of(System.getProperty("java.home"), "bin", "java").toString()
        val process = ProcessBuilder(
            java,
            "-cp",
            System.getProperty("java.class.path"),
            "parallel.ParallelPoolShutdownTestKt",
        ).start()

        try {
            assertTrue(
                process.waitFor(2, TimeUnit.SECONDS),
                "child JVM did not exit; a non-daemon ParallelPool timer thread is likely still alive"
            )
            assertEquals(0, process.exitValue())
        } finally {
            if (process.isAlive) {
                process.destroyForcibly()
            }
        }
    }
}

private class TestResource : Closeable {
    override fun close() {}
}

fun main() {
    ParallelPool(1).use { pool ->
        pool.run {
            Scheduler.compute {
                ParallelPool.allocInScope({ TestResource() }) {}
            }
        }
    }
}

Before this change, the child JVM did not exit within 2 seconds because the scheduled cleanup executor had a non-daemon timer thread alive.

After this change, the child JVM exited normally in under 100 ms.

As an additional minimal sanity check, a standalone Java probe showed the same lifecycle behavior:

• default Executors.newScheduledThreadPool(1) kept the JVM alive until killed by timeout
• a scheduled executor using daemon threads exited normally

Validation

Ran locally with JDK 19:

./gradlew :GeneralUtils:test --tests "parallel.*" --no-daemon

All 23 related parallel tests passed.

[yoav-el-certora]

Hi @mmv08, thanks for reaching out.
This looks like a positive improvement, we will process it as a part of our regular prover release process and benchmarks and update you once we have a conclusion.