From 4ed7929b394e07ff0cfe84d562ed59206a69287e Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Mon, 30 Sep 2024 17:30:48 +0200 Subject: [PATCH 1/2] fixing #3004? --- .../tla/bmcmt/passes/BoundedCheckerPassImpl.scala | 2 +- .../apalache/tla/bmcmt/smt/Z3SolverContext.scala | 15 ++++++++++----- 2 files changed, 11 insertions(+), 6 deletions(-) diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/passes/BoundedCheckerPassImpl.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/passes/BoundedCheckerPassImpl.scala index 71c00aa3c2..f8f63e4340 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/passes/BoundedCheckerPassImpl.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/passes/BoundedCheckerPassImpl.scala @@ -136,7 +136,7 @@ class BoundedCheckerPassImpl @Inject() ( val checker = new SeqModelChecker[SnapshotT](params, input, filteredTrex, Seq(DumpFilesModelCheckerListener)) val outcome = checker.run() - rewriter.dispose() + filteredTrex.dispose() logger.info(s"The outcome is: " + outcome) outcome } diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala index a978d637bb..1631c97697 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala @@ -144,17 +144,21 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext with LazyL private val statisticsLock: ReentrantLock = new ReentrantLock() // start a new thread to collect statistics private val statisticsThread = new Thread(() => { - while (state == Running()) { + var interrupted = false + while (state == Running() && !interrupted) { // Sleep for a while. // If we call printStatistics right away, we can easily run into a race condition with Z3 initializing. // This produces a core dump. - Thread.sleep(config.z3StatsSec * 1000) // make sure that the context is not being disposed right now. Otherwise, we can get a nice core dump. statisticsLock.lock() try { - if (state == Running()) { - printStatistics() - } + Thread.sleep(config.z3StatsSec * 1000) + printStatistics() + } catch { + case _: InterruptedException => + // terminate the thread immediately upon interruption + logger.info(s"Finishing the statistics thread ${id}") + interrupted = true } finally { statisticsLock.unlock() } @@ -173,6 +177,7 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext with LazyL state = Disposed() // Try to obtain the lock, to let the statistics thread finish its work. // If it is stuck for some reason, continue after the timeout in any case. + statisticsThread.interrupt() statisticsLock.tryLock(2 * config.z3StatsSec, java.util.concurrent.TimeUnit.SECONDS) try { if (config.debug) { From 26c78a040a451d01851301138e4c46a45d213ea6 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Mon, 30 Sep 2024 17:36:40 +0200 Subject: [PATCH 2/2] add release notes --- .unreleased/bug-fixes/dumps-by-statistics-thread.md | 1 + 1 file changed, 1 insertion(+) create mode 100644 .unreleased/bug-fixes/dumps-by-statistics-thread.md diff --git a/.unreleased/bug-fixes/dumps-by-statistics-thread.md b/.unreleased/bug-fixes/dumps-by-statistics-thread.md new file mode 100644 index 0000000000..dcb4839e26 --- /dev/null +++ b/.unreleased/bug-fixes/dumps-by-statistics-thread.md @@ -0,0 +1 @@ +Fix thread synchronization between the statistics thread and Z3Context, see #3009