From 3b628de8a5da1f1656eb3f5c30fb41080da7b690 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Wed, 18 Sep 2024 18:54:41 +0200 Subject: [PATCH 01/11] add a Z3 statistics thread --- .../bmcmt/passes/BoundedCheckerPassImpl.scala | 4 ++- .../apalache/tla/bmcmt/smt/SolverConfig.scala | 11 ++++---- .../tla/bmcmt/smt/Z3SolverContext.scala | 25 +++++++++++++++++++ .../tla/bmcmt/CrossTestEncodings.scala | 2 +- 4 files changed, 35 insertions(+), 7 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 aa2b3bb34a..e505371812 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 @@ -75,7 +75,9 @@ class BoundedCheckerPassImpl @Inject() ( val smtProfile = options.common.smtprof val smtRandomSeed = tuning.getOrElse("smt.randomSeed", "0").toInt - val solverConfig = SolverConfig(debug, smtProfile, smtRandomSeed, smtEncoding) + val smtStatsSec = + tuning.getOrElse("smt.statsSec", SolverConfig.default.z3StatsSec.toString).toInt + val solverConfig = SolverConfig(debug, smtProfile, smtRandomSeed, smtStatsSec, smtEncoding) val result = options.checker.algo match { case Algorithm.Incremental => runIncrementalChecker(params, input, tuning, solverConfig) diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/SolverConfig.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/SolverConfig.scala index 3b415e64e2..a54ca71bbb 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/SolverConfig.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/SolverConfig.scala @@ -19,10 +19,11 @@ import at.forsyte.apalache.infra.passes.options.SMTEncoding * Igor Konnov, Rodrigo Otoni */ sealed case class SolverConfig( - debug: Boolean, - profile: Boolean, - randomSeed: Int, - smtEncoding: SMTEncoding) {} + debug: Boolean, + profile: Boolean, + randomSeed: Int, + z3StatsSec: Int, + smtEncoding: SMTEncoding) {} object SolverConfig { @@ -30,5 +31,5 @@ object SolverConfig { * Get the default configuration. */ val default: SolverConfig = - new SolverConfig(debug = false, profile = false, randomSeed = 0, smtEncoding = SMTEncoding.OOPSLA19) + new SolverConfig(debug = false, profile = false, randomSeed = 0, smtEncoding = SMTEncoding.OOPSLA19, z3StatsSec = 60) } 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 76cac9981d..d40ec0605a 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 @@ -120,11 +120,36 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext with LazyL */ private var maxCellIdPerContext = List(-1) + private trait ContextState + private case class Running() extends ContextState + private case class Disposed() extends ContextState + + /** + * The internal state of the Z3 solver context. + */ + private var state: ContextState = Running() + + // start a new thread to collect statistics + private val statisticsThread = new Thread(() => { + while (state == Running()) { + Thread.sleep(config.z3StatsSec * 1000) + logger.info(s"Z3 statistics for context $id:") + val entries = z3solver.getStatistics.getEntries.map(stat => { + s"${stat.Key}=${stat.getValueString}" + }) + logger.info(entries.mkString(",")) + } + }) + if (config.debug && config.z3StatsSec > 0) { + statisticsThread.start() + } + /** * Dispose whatever has to be disposed in the end. */ override def dispose(): Unit = { logger.debug(s"Disposing Z3 solver context ${id}") + state = Disposed() z3context.close() closeLogs() cellCache.clear() diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/CrossTestEncodings.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/CrossTestEncodings.scala index f55afdc52b..a8fb0c4e30 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/CrossTestEncodings.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/CrossTestEncodings.scala @@ -183,7 +183,7 @@ trait CrossTestEncodings extends AnyFunSuite with Checkers { val checkerParams = new ModelCheckerParams(checkerInput, 0) val solverContext = - new Z3SolverContext(new SolverConfig(debug = false, profile = false, randomSeed = 0, smtEncoding = smtEncoding)) + new Z3SolverContext(new SolverConfig(debug = false, profile = false, randomSeed = 0, smtEncoding = smtEncoding, z3StatsSec = 0)) val rewriter: SymbStateRewriterImpl = smtEncoding match { case SMTEncoding.OOPSLA19 => new SymbStateRewriterImpl(solverContext, renaming) case SMTEncoding.Arrays => new SymbStateRewriterImplWithArrays(solverContext, renaming) From 010c9b2aeaeba69011f2d91bf2f3ce251fe68805 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Wed, 18 Sep 2024 19:04:54 +0200 Subject: [PATCH 02/11] print statistics on dispose --- .../tla/bmcmt/smt/Z3SolverContext.scala | 18 +++++++++++++----- 1 file changed, 13 insertions(+), 5 deletions(-) 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 d40ec0605a..78c10a325a 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 @@ -133,13 +133,10 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext with LazyL private val statisticsThread = new Thread(() => { while (state == Running()) { Thread.sleep(config.z3StatsSec * 1000) - logger.info(s"Z3 statistics for context $id:") - val entries = z3solver.getStatistics.getEntries.map(stat => { - s"${stat.Key}=${stat.getValueString}" - }) - logger.info(entries.mkString(",")) + printStatistics() } }) + if (config.debug && config.z3StatsSec > 0) { statisticsThread.start() } @@ -149,6 +146,9 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext with LazyL */ override def dispose(): Unit = { logger.debug(s"Disposing Z3 solver context ${id}") + if (config.debug) { + printStatistics() + } state = Disposed() z3context.close() closeLogs() @@ -1039,6 +1039,14 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext with LazyL flushLogs() throw e } + + private def printStatistics(): Unit = { + logger.info(s"Z3 statistics for context $id...") + val entries = z3solver.getStatistics.getEntries.map(stat => { + s"${stat.Key}=${stat.getValueString}" + }) + logger.info(entries.mkString(",") + "\n") + } } object Z3SolverContext { From 69ba14cfe9b6d375bf8f37c55bda9989cdc119f7 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Wed, 18 Sep 2024 19:18:27 +0200 Subject: [PATCH 03/11] add z3StatsSec in the tests --- .../apalache/tla/bmcmt/TestSeqModelCheckerWithArrays.scala | 2 +- .../apalache/tla/bmcmt/TestSeqModelCheckerWithOOPSLA19.scala | 2 +- .../tla/bmcmt/smt/TestRecordingSolverContextWithArrays.scala | 2 +- .../trex/TestTransitionExecutorWithIncrementalAndArrays.scala | 2 +- .../bmcmt/trex/TestTransitionExecutorWithOfflineAndArrays.scala | 2 +- .../trex/TestTransitionExecutorWithOfflineAndOOPSLA19.scala | 2 +- 6 files changed, 6 insertions(+), 6 deletions(-) diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSeqModelCheckerWithArrays.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSeqModelCheckerWithArrays.scala index e6e69cfe9d..7a385d4646 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSeqModelCheckerWithArrays.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSeqModelCheckerWithArrays.scala @@ -13,7 +13,7 @@ import org.scalatestplus.junit.JUnitRunner class TestSeqModelCheckerWithArrays extends TestSeqModelCheckerTrait { override protected def withFixture(test: OneArgTest): Outcome = { val solver = RecordingSolverContext - .createZ3(None, SolverConfig(debug = false, profile = false, 0, smtEncoding = SMTEncoding.Arrays)) + .createZ3(None, SolverConfig(debug = false, profile = false, 0, z3StatsSec = 0, smtEncoding = SMTEncoding.Arrays)) val rewriter = new SymbStateRewriterImpl(solver, new IncrementalRenaming(new IdleTracker), new ExprGradeStoreImpl) test(rewriter) } diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSeqModelCheckerWithOOPSLA19.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSeqModelCheckerWithOOPSLA19.scala index c0140039bc..2cef92d041 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSeqModelCheckerWithOOPSLA19.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSeqModelCheckerWithOOPSLA19.scala @@ -13,7 +13,7 @@ import org.scalatestplus.junit.JUnitRunner class TestSeqModelCheckerWithOOPSLA19 extends TestSeqModelCheckerTrait { override protected def withFixture(test: OneArgTest): Outcome = { val solver = RecordingSolverContext - .createZ3(None, SolverConfig(debug = false, profile = false, 0, smtEncoding = SMTEncoding.OOPSLA19)) + .createZ3(None, SolverConfig(debug = false, profile = false, 0, z3StatsSec = 0, smtEncoding = SMTEncoding.OOPSLA19)) val rewriter = new SymbStateRewriterImpl(solver, new IncrementalRenaming(new IdleTracker), new ExprGradeStoreImpl) test(rewriter) } diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContextWithArrays.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContextWithArrays.scala index 06bdac0974..e852d3ad16 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContextWithArrays.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContextWithArrays.scala @@ -8,7 +8,7 @@ import org.scalatestplus.junit.JUnitRunner @RunWith(classOf[JUnitRunner]) class TestRecordingSolverContextWithArrays extends TestRecordingSolverContext { override protected def withFixture(test: NoArgTest): Outcome = { - solverConfig = SolverConfig(debug = false, profile = false, randomSeed = 0, smtEncoding = SMTEncoding.Arrays) + solverConfig = SolverConfig(debug = false, profile = false, randomSeed = 0, z3StatsSec = 0, smtEncoding = SMTEncoding.Arrays) test() } } diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithIncrementalAndArrays.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithIncrementalAndArrays.scala index 3b0f552d11..7cbb7670c2 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithIncrementalAndArrays.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithIncrementalAndArrays.scala @@ -13,7 +13,7 @@ class TestTransitionExecutorWithIncrementalAndArrays override protected def withFixture(test: OneArgTest): Outcome = { val solver = new Z3SolverContext(SolverConfig(debug = false, profile = false, randomSeed = 0, - smtEncoding = SMTEncoding.Arrays)) + z3StatsSec = 0, smtEncoding = SMTEncoding.Arrays)) withFixtureInContext(solver, new IncrementalExecutionContext(_), test) } } diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithOfflineAndArrays.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithOfflineAndArrays.scala index f96b0133cf..4392cfe462 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithOfflineAndArrays.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithOfflineAndArrays.scala @@ -12,7 +12,7 @@ import org.scalatestplus.junit.JUnitRunner class TestTransitionExecutorWithOfflineAndArrays extends TestTransitionExecutorImpl[OfflineExecutionContextSnapshot] { override protected def withFixture(test: OneArgTest): Outcome = { val solver = RecordingSolverContext - .createZ3(None, SolverConfig(debug = false, profile = false, randomSeed = 0, smtEncoding = SMTEncoding.Arrays)) + .createZ3(None, SolverConfig(debug = false, profile = false, randomSeed = 0, z3StatsSec = 0, smtEncoding = SMTEncoding.Arrays)) withFixtureInContext(solver, new OfflineExecutionContext(_, new IncrementalRenaming(new IdleTracker)), test) } } diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithOfflineAndOOPSLA19.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithOfflineAndOOPSLA19.scala index 85ca1e0edb..1ff60f9fd4 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithOfflineAndOOPSLA19.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithOfflineAndOOPSLA19.scala @@ -18,7 +18,7 @@ import org.scalatestplus.junit.JUnitRunner class TestTransitionExecutorWithOfflineAndOOPSLA19 extends TestTransitionExecutorImpl[OfflineExecutionContextSnapshot] { override def withFixture(test: OneArgTest): Outcome = { val solver = RecordingSolverContext - .createZ3(None, SolverConfig(debug = false, profile = false, randomSeed = 0, smtEncoding = SMTEncoding.OOPSLA19)) + .createZ3(None, SolverConfig(debug = false, profile = false, randomSeed = 0, z3StatsSec = 0, smtEncoding = SMTEncoding.OOPSLA19)) withFixtureInContext(solver, new OfflineExecutionContext(_, new IncrementalRenaming(new IdleTracker)), test) } } From 5c49f38ac0905796566d86feda7b7a2c0e6c140b Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Wed, 18 Sep 2024 19:50:37 +0200 Subject: [PATCH 04/11] add z3StatsSec in tests --- .../apalache/tla/bmcmt/TestSeqModelCheckerWithFunArrays.scala | 2 +- .../tla/bmcmt/smt/TestRecordingSolverContextWithFunArrays.scala | 2 +- .../tla/bmcmt/smt/TestRecordingSolverContextWithOOPSLA19.scala | 2 +- .../TestTransitionExecutorWithIncrementalAndFunArrays.scala | 2 +- .../trex/TestTransitionExecutorWithIncrementalAndOOPSLA19.scala | 2 +- .../trex/TestTransitionExecutorWithOfflineAndFunArrays.scala | 2 +- 6 files changed, 6 insertions(+), 6 deletions(-) diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSeqModelCheckerWithFunArrays.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSeqModelCheckerWithFunArrays.scala index 768510f257..d007a5defb 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSeqModelCheckerWithFunArrays.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSeqModelCheckerWithFunArrays.scala @@ -13,7 +13,7 @@ import org.scalatestplus.junit.JUnitRunner class TestSeqModelCheckerWithFunArrays extends TestSeqModelCheckerTrait { override protected def withFixture(test: OneArgTest): Outcome = { val solver = RecordingSolverContext - .createZ3(None, SolverConfig(debug = false, profile = false, 0, smtEncoding = SMTEncoding.FunArrays)) + .createZ3(None, SolverConfig(debug = false, profile = false, 0, z3StatsSec = 0, smtEncoding = SMTEncoding.FunArrays)) val rewriter = new SymbStateRewriterImpl(solver, new IncrementalRenaming(new IdleTracker), new ExprGradeStoreImpl) test(rewriter) } diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContextWithFunArrays.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContextWithFunArrays.scala index d6aa779b3d..8c8f79f98d 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContextWithFunArrays.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContextWithFunArrays.scala @@ -8,7 +8,7 @@ import org.scalatestplus.junit.JUnitRunner @RunWith(classOf[JUnitRunner]) class TestRecordingSolverContextWithFunArrays extends TestRecordingSolverContext { override protected def withFixture(test: NoArgTest): Outcome = { - solverConfig = SolverConfig(debug = false, profile = false, randomSeed = 0, smtEncoding = SMTEncoding.FunArrays) + solverConfig = SolverConfig(debug = false, profile = false, randomSeed = 0, z3StatsSec = 0, smtEncoding = SMTEncoding.FunArrays) test() } } diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContextWithOOPSLA19.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContextWithOOPSLA19.scala index 41e8153c4b..affccbb227 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContextWithOOPSLA19.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContextWithOOPSLA19.scala @@ -8,7 +8,7 @@ import org.scalatestplus.junit.JUnitRunner @RunWith(classOf[JUnitRunner]) class TestRecordingSolverContextWithOOPSLA19 extends TestRecordingSolverContext { override protected def withFixture(test: NoArgTest): Outcome = { - solverConfig = SolverConfig(debug = false, profile = false, randomSeed = 0, smtEncoding = SMTEncoding.OOPSLA19) + solverConfig = SolverConfig(debug = false, profile = false, randomSeed = 0, z3StatsSec = 0, smtEncoding = SMTEncoding.OOPSLA19) test() } } diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithIncrementalAndFunArrays.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithIncrementalAndFunArrays.scala index ef0afec8ce..3a5b64c6d7 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithIncrementalAndFunArrays.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithIncrementalAndFunArrays.scala @@ -12,7 +12,7 @@ class TestTransitionExecutorWithIncrementalAndFunArrays with TestFilteredTransitionExecutor[IncrementalExecutionContextSnapshot] { override protected def withFixture(test: OneArgTest): Outcome = { val solver = new Z3SolverContext(SolverConfig(debug = false, profile = false, randomSeed = 0, - smtEncoding = SMTEncoding.FunArrays)) + z3StatsSec = 0, smtEncoding = SMTEncoding.FunArrays)) withFixtureInContext(solver, new IncrementalExecutionContext(_), test) } } diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithIncrementalAndOOPSLA19.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithIncrementalAndOOPSLA19.scala index b697502d79..e5f7d7c3be 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithIncrementalAndOOPSLA19.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithIncrementalAndOOPSLA19.scala @@ -19,7 +19,7 @@ class TestTransitionExecutorWithIncrementalAndOOPSLA19 override protected def withFixture(test: OneArgTest): Outcome = { val solver = new Z3SolverContext(SolverConfig(debug = false, profile = false, randomSeed = 0, - smtEncoding = SMTEncoding.OOPSLA19)) + z3StatsSec = 0, smtEncoding = SMTEncoding.OOPSLA19)) withFixtureInContext(solver, new IncrementalExecutionContext(_), test) } } diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithOfflineAndFunArrays.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithOfflineAndFunArrays.scala index 701d8fcbe0..dd7102178f 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithOfflineAndFunArrays.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithOfflineAndFunArrays.scala @@ -13,7 +13,7 @@ class TestTransitionExecutorWithOfflineAndFunArrays extends TestTransitionExecutorImpl[OfflineExecutionContextSnapshot] { override protected def withFixture(test: OneArgTest): Outcome = { val solver = RecordingSolverContext - .createZ3(None, SolverConfig(debug = false, profile = false, randomSeed = 0, smtEncoding = SMTEncoding.FunArrays)) + .createZ3(None, SolverConfig(debug = false, profile = false, randomSeed = 0, z3StatsSec = 0, smtEncoding = SMTEncoding.FunArrays)) withFixtureInContext(solver, new OfflineExecutionContext(_, new IncrementalRenaming(new IdleTracker)), test) } } From bf12a13610936a19cf09185027a132b59f6f410b Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Wed, 18 Sep 2024 19:53:20 +0200 Subject: [PATCH 05/11] fix formatting --- .../apalache/tla/bmcmt/smt/SolverConfig.scala | 13 +++++++------ .../apalache/tla/bmcmt/CrossTestEncodings.scala | 3 ++- .../bmcmt/TestSeqModelCheckerWithFunArrays.scala | 3 ++- .../tla/bmcmt/TestSeqModelCheckerWithOOPSLA19.scala | 3 ++- .../smt/TestRecordingSolverContextWithArrays.scala | 3 ++- .../TestRecordingSolverContextWithFunArrays.scala | 3 ++- .../TestRecordingSolverContextWithOOPSLA19.scala | 3 ++- ...TransitionExecutorWithIncrementalAndArrays.scala | 4 ++-- ...nsitionExecutorWithIncrementalAndFunArrays.scala | 4 ++-- ...ansitionExecutorWithIncrementalAndOOPSLA19.scala | 4 ++-- ...TestTransitionExecutorWithOfflineAndArrays.scala | 4 +++- ...tTransitionExecutorWithOfflineAndFunArrays.scala | 4 +++- ...stTransitionExecutorWithOfflineAndOOPSLA19.scala | 4 +++- 13 files changed, 34 insertions(+), 21 deletions(-) diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/SolverConfig.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/SolverConfig.scala index a54ca71bbb..0a4d6face7 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/SolverConfig.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/SolverConfig.scala @@ -19,11 +19,11 @@ import at.forsyte.apalache.infra.passes.options.SMTEncoding * Igor Konnov, Rodrigo Otoni */ sealed case class SolverConfig( - debug: Boolean, - profile: Boolean, - randomSeed: Int, - z3StatsSec: Int, - smtEncoding: SMTEncoding) {} + debug: Boolean, + profile: Boolean, + randomSeed: Int, + z3StatsSec: Int, + smtEncoding: SMTEncoding) {} object SolverConfig { @@ -31,5 +31,6 @@ object SolverConfig { * Get the default configuration. */ val default: SolverConfig = - new SolverConfig(debug = false, profile = false, randomSeed = 0, smtEncoding = SMTEncoding.OOPSLA19, z3StatsSec = 60) + new SolverConfig(debug = false, profile = false, randomSeed = 0, smtEncoding = SMTEncoding.OOPSLA19, + z3StatsSec = 60) } diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/CrossTestEncodings.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/CrossTestEncodings.scala index a8fb0c4e30..44b94ec10e 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/CrossTestEncodings.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/CrossTestEncodings.scala @@ -183,7 +183,8 @@ trait CrossTestEncodings extends AnyFunSuite with Checkers { val checkerParams = new ModelCheckerParams(checkerInput, 0) val solverContext = - new Z3SolverContext(new SolverConfig(debug = false, profile = false, randomSeed = 0, smtEncoding = smtEncoding, z3StatsSec = 0)) + new Z3SolverContext(new SolverConfig(debug = false, profile = false, randomSeed = 0, smtEncoding = smtEncoding, + z3StatsSec = 0)) val rewriter: SymbStateRewriterImpl = smtEncoding match { case SMTEncoding.OOPSLA19 => new SymbStateRewriterImpl(solverContext, renaming) case SMTEncoding.Arrays => new SymbStateRewriterImplWithArrays(solverContext, renaming) diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSeqModelCheckerWithFunArrays.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSeqModelCheckerWithFunArrays.scala index d007a5defb..ced0b710ed 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSeqModelCheckerWithFunArrays.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSeqModelCheckerWithFunArrays.scala @@ -13,7 +13,8 @@ import org.scalatestplus.junit.JUnitRunner class TestSeqModelCheckerWithFunArrays extends TestSeqModelCheckerTrait { override protected def withFixture(test: OneArgTest): Outcome = { val solver = RecordingSolverContext - .createZ3(None, SolverConfig(debug = false, profile = false, 0, z3StatsSec = 0, smtEncoding = SMTEncoding.FunArrays)) + .createZ3(None, + SolverConfig(debug = false, profile = false, 0, z3StatsSec = 0, smtEncoding = SMTEncoding.FunArrays)) val rewriter = new SymbStateRewriterImpl(solver, new IncrementalRenaming(new IdleTracker), new ExprGradeStoreImpl) test(rewriter) } diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSeqModelCheckerWithOOPSLA19.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSeqModelCheckerWithOOPSLA19.scala index 2cef92d041..44d0df1e92 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSeqModelCheckerWithOOPSLA19.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSeqModelCheckerWithOOPSLA19.scala @@ -13,7 +13,8 @@ import org.scalatestplus.junit.JUnitRunner class TestSeqModelCheckerWithOOPSLA19 extends TestSeqModelCheckerTrait { override protected def withFixture(test: OneArgTest): Outcome = { val solver = RecordingSolverContext - .createZ3(None, SolverConfig(debug = false, profile = false, 0, z3StatsSec = 0, smtEncoding = SMTEncoding.OOPSLA19)) + .createZ3(None, + SolverConfig(debug = false, profile = false, 0, z3StatsSec = 0, smtEncoding = SMTEncoding.OOPSLA19)) val rewriter = new SymbStateRewriterImpl(solver, new IncrementalRenaming(new IdleTracker), new ExprGradeStoreImpl) test(rewriter) } diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContextWithArrays.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContextWithArrays.scala index e852d3ad16..ba43176647 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContextWithArrays.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContextWithArrays.scala @@ -8,7 +8,8 @@ import org.scalatestplus.junit.JUnitRunner @RunWith(classOf[JUnitRunner]) class TestRecordingSolverContextWithArrays extends TestRecordingSolverContext { override protected def withFixture(test: NoArgTest): Outcome = { - solverConfig = SolverConfig(debug = false, profile = false, randomSeed = 0, z3StatsSec = 0, smtEncoding = SMTEncoding.Arrays) + solverConfig = SolverConfig(debug = false, profile = false, randomSeed = 0, z3StatsSec = 0, + smtEncoding = SMTEncoding.Arrays) test() } } diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContextWithFunArrays.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContextWithFunArrays.scala index 8c8f79f98d..9463feb097 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContextWithFunArrays.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContextWithFunArrays.scala @@ -8,7 +8,8 @@ import org.scalatestplus.junit.JUnitRunner @RunWith(classOf[JUnitRunner]) class TestRecordingSolverContextWithFunArrays extends TestRecordingSolverContext { override protected def withFixture(test: NoArgTest): Outcome = { - solverConfig = SolverConfig(debug = false, profile = false, randomSeed = 0, z3StatsSec = 0, smtEncoding = SMTEncoding.FunArrays) + solverConfig = SolverConfig(debug = false, profile = false, randomSeed = 0, z3StatsSec = 0, + smtEncoding = SMTEncoding.FunArrays) test() } } diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContextWithOOPSLA19.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContextWithOOPSLA19.scala index affccbb227..b5dd9265b3 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContextWithOOPSLA19.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContextWithOOPSLA19.scala @@ -8,7 +8,8 @@ import org.scalatestplus.junit.JUnitRunner @RunWith(classOf[JUnitRunner]) class TestRecordingSolverContextWithOOPSLA19 extends TestRecordingSolverContext { override protected def withFixture(test: NoArgTest): Outcome = { - solverConfig = SolverConfig(debug = false, profile = false, randomSeed = 0, z3StatsSec = 0, smtEncoding = SMTEncoding.OOPSLA19) + solverConfig = SolverConfig(debug = false, profile = false, randomSeed = 0, z3StatsSec = 0, + smtEncoding = SMTEncoding.OOPSLA19) test() } } diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithIncrementalAndArrays.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithIncrementalAndArrays.scala index 7cbb7670c2..4a0401caac 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithIncrementalAndArrays.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithIncrementalAndArrays.scala @@ -12,8 +12,8 @@ class TestTransitionExecutorWithIncrementalAndArrays with TestFilteredTransitionExecutor[IncrementalExecutionContextSnapshot] { override protected def withFixture(test: OneArgTest): Outcome = { val solver = - new Z3SolverContext(SolverConfig(debug = false, profile = false, randomSeed = 0, - z3StatsSec = 0, smtEncoding = SMTEncoding.Arrays)) + new Z3SolverContext(SolverConfig(debug = false, profile = false, randomSeed = 0, z3StatsSec = 0, + smtEncoding = SMTEncoding.Arrays)) withFixtureInContext(solver, new IncrementalExecutionContext(_), test) } } diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithIncrementalAndFunArrays.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithIncrementalAndFunArrays.scala index 3a5b64c6d7..dca20cf4fe 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithIncrementalAndFunArrays.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithIncrementalAndFunArrays.scala @@ -11,8 +11,8 @@ class TestTransitionExecutorWithIncrementalAndFunArrays extends TestTransitionExecutorImpl[IncrementalExecutionContextSnapshot] with TestFilteredTransitionExecutor[IncrementalExecutionContextSnapshot] { override protected def withFixture(test: OneArgTest): Outcome = { - val solver = new Z3SolverContext(SolverConfig(debug = false, profile = false, randomSeed = 0, - z3StatsSec = 0, smtEncoding = SMTEncoding.FunArrays)) + val solver = new Z3SolverContext(SolverConfig(debug = false, profile = false, randomSeed = 0, z3StatsSec = 0, + smtEncoding = SMTEncoding.FunArrays)) withFixtureInContext(solver, new IncrementalExecutionContext(_), test) } } diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithIncrementalAndOOPSLA19.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithIncrementalAndOOPSLA19.scala index e5f7d7c3be..3cb658ab3d 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithIncrementalAndOOPSLA19.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithIncrementalAndOOPSLA19.scala @@ -18,8 +18,8 @@ class TestTransitionExecutorWithIncrementalAndOOPSLA19 with TestFilteredTransitionExecutor[IncrementalExecutionContextSnapshot] { override protected def withFixture(test: OneArgTest): Outcome = { val solver = - new Z3SolverContext(SolverConfig(debug = false, profile = false, randomSeed = 0, - z3StatsSec = 0, smtEncoding = SMTEncoding.OOPSLA19)) + new Z3SolverContext(SolverConfig(debug = false, profile = false, randomSeed = 0, z3StatsSec = 0, + smtEncoding = SMTEncoding.OOPSLA19)) withFixtureInContext(solver, new IncrementalExecutionContext(_), test) } } diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithOfflineAndArrays.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithOfflineAndArrays.scala index 4392cfe462..b4df42ad9d 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithOfflineAndArrays.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithOfflineAndArrays.scala @@ -12,7 +12,9 @@ import org.scalatestplus.junit.JUnitRunner class TestTransitionExecutorWithOfflineAndArrays extends TestTransitionExecutorImpl[OfflineExecutionContextSnapshot] { override protected def withFixture(test: OneArgTest): Outcome = { val solver = RecordingSolverContext - .createZ3(None, SolverConfig(debug = false, profile = false, randomSeed = 0, z3StatsSec = 0, smtEncoding = SMTEncoding.Arrays)) + .createZ3(None, + SolverConfig(debug = false, profile = false, randomSeed = 0, z3StatsSec = 0, + smtEncoding = SMTEncoding.Arrays)) withFixtureInContext(solver, new OfflineExecutionContext(_, new IncrementalRenaming(new IdleTracker)), test) } } diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithOfflineAndFunArrays.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithOfflineAndFunArrays.scala index dd7102178f..e4dec6e82c 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithOfflineAndFunArrays.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithOfflineAndFunArrays.scala @@ -13,7 +13,9 @@ class TestTransitionExecutorWithOfflineAndFunArrays extends TestTransitionExecutorImpl[OfflineExecutionContextSnapshot] { override protected def withFixture(test: OneArgTest): Outcome = { val solver = RecordingSolverContext - .createZ3(None, SolverConfig(debug = false, profile = false, randomSeed = 0, z3StatsSec = 0, smtEncoding = SMTEncoding.FunArrays)) + .createZ3(None, + SolverConfig(debug = false, profile = false, randomSeed = 0, z3StatsSec = 0, + smtEncoding = SMTEncoding.FunArrays)) withFixtureInContext(solver, new OfflineExecutionContext(_, new IncrementalRenaming(new IdleTracker)), test) } } diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithOfflineAndOOPSLA19.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithOfflineAndOOPSLA19.scala index 1ff60f9fd4..1ff9ad4d81 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithOfflineAndOOPSLA19.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithOfflineAndOOPSLA19.scala @@ -18,7 +18,9 @@ import org.scalatestplus.junit.JUnitRunner class TestTransitionExecutorWithOfflineAndOOPSLA19 extends TestTransitionExecutorImpl[OfflineExecutionContextSnapshot] { override def withFixture(test: OneArgTest): Outcome = { val solver = RecordingSolverContext - .createZ3(None, SolverConfig(debug = false, profile = false, randomSeed = 0, z3StatsSec = 0, smtEncoding = SMTEncoding.OOPSLA19)) + .createZ3(None, + SolverConfig(debug = false, profile = false, randomSeed = 0, z3StatsSec = 0, + smtEncoding = SMTEncoding.OOPSLA19)) withFixtureInContext(solver, new OfflineExecutionContext(_, new IncrementalRenaming(new IdleTracker)), test) } } From 15ad96d3defa68f5ba07589d139fa455aa968243 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Wed, 18 Sep 2024 19:56:43 +0200 Subject: [PATCH 06/11] add release notes --- .unreleased/features/z3-stats.md | 1 + 1 file changed, 1 insertion(+) create mode 100644 .unreleased/features/z3-stats.md diff --git a/.unreleased/features/z3-stats.md b/.unreleased/features/z3-stats.md new file mode 100644 index 0000000000..a3011f003a --- /dev/null +++ b/.unreleased/features/z3-stats.md @@ -0,0 +1 @@ +Periodically print Z3 statistics when `--debug` is on (#2992) From 193a110dc8eddef03232b3a362d1c7eaaf1858f0 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Thu, 19 Sep 2024 13:04:00 +0200 Subject: [PATCH 07/11] swap sleep and stat query to avoid late exceptions --- .../at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 78c10a325a..a65d1cf221 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 @@ -132,8 +132,8 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext with LazyL // start a new thread to collect statistics private val statisticsThread = new Thread(() => { while (state == Running()) { - Thread.sleep(config.z3StatsSec * 1000) printStatistics() + Thread.sleep(config.z3StatsSec * 1000) } }) From 5c0aecfddff34d7823bba5f834533557d3e8f41e Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Thu, 19 Sep 2024 13:35:07 +0200 Subject: [PATCH 08/11] print stats a bit more accurately --- .../apalache/tla/bmcmt/smt/Z3SolverContext.scala | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) 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 a65d1cf221..e78c136a93 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 @@ -132,8 +132,16 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext with LazyL // start a new thread to collect statistics private val statisticsThread = new Thread(() => { while (state == Running()) { - printStatistics() + // 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) + // Check whether the solver has not been disposed yet. Otherwise, we get a Z3Exception printed. + // There is still a small probability of getting this exception. I would like to avoid mutexes here, + // to avoid accidental deadlocks in dispose(). + if (state == Running()) { + printStatistics() + } } }) From e01af53517db935714a30cf175e17af94f3a25f3 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Sat, 21 Sep 2024 20:18:28 +0200 Subject: [PATCH 09/11] use a lock --- .../tla/bmcmt/smt/Z3SolverContext.scala | 46 ++++++++++++------- 1 file changed, 29 insertions(+), 17 deletions(-) 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 e78c136a93..969f3c78db 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 @@ -18,6 +18,7 @@ import com.typesafe.scalalogging.LazyLogging import java.io.PrintWriter import java.util.concurrent.atomic.AtomicLong +import java.util.concurrent.locks.{Lock, ReentrantLock} import scala.collection.mutable import scala.collection.mutable.ListBuffer @@ -124,11 +125,11 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext with LazyL private case class Running() extends ContextState private case class Disposed() extends ContextState - /** - * The internal state of the Z3 solver context. - */ + // the state of the context: Running or Disposed private var state: ContextState = Running() + // the lock shared between the context and the statistics thread + private var statisticsLock: ReentrantLock = new ReentrantLock() // start a new thread to collect statistics private val statisticsThread = new Thread(() => { while (state == Running()) { @@ -136,11 +137,14 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext with LazyL // 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) - // Check whether the solver has not been disposed yet. Otherwise, we get a Z3Exception printed. - // There is still a small probability of getting this exception. I would like to avoid mutexes here, - // to avoid accidental deadlocks in dispose(). - if (state == Running()) { - printStatistics() + // 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() + } + } finally { + statisticsLock.unlock() } } }) @@ -154,16 +158,24 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext with LazyL */ override def dispose(): Unit = { logger.debug(s"Disposing Z3 solver context ${id}") - if (config.debug) { - printStatistics() - } state = Disposed() - z3context.close() - closeLogs() - cellCache.clear() - inCache.clear() - funDecls.clear() - cellSorts.clear() + // 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. + statisticsLock.tryLock(2 * config.z3StatsSec, java.util.concurrent.TimeUnit.SECONDS) + try { + if (config.debug) { + printStatistics() + } + z3context.close() + closeLogs() + cellCache.clear() + inCache.clear() + funDecls.clear() + cellSorts.clear() + } finally { + // it's not that important at this point, but let's unlock it for the piece of mind + statisticsLock.unlock() + } } /** From 14ffe66e00e3ce901042efc3b04fc8f8e1f47102 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Sat, 21 Sep 2024 20:54:40 +0200 Subject: [PATCH 10/11] fix formatting --- .../at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 969f3c78db..8756e88ec0 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 @@ -18,7 +18,7 @@ import com.typesafe.scalalogging.LazyLogging import java.io.PrintWriter import java.util.concurrent.atomic.AtomicLong -import java.util.concurrent.locks.{Lock, ReentrantLock} +import java.util.concurrent.locks.ReentrantLock import scala.collection.mutable import scala.collection.mutable.ListBuffer From 93c9b6f17454ad6ead761b1531a39bc1a76c5709 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Mon, 23 Sep 2024 09:59:35 +0200 Subject: [PATCH 11/11] make statisticsLock a val --- .../at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 8756e88ec0..0c9ea9476e 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 @@ -129,7 +129,7 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext with LazyL private var state: ContextState = Running() // the lock shared between the context and the statistics thread - private var statisticsLock: ReentrantLock = new ReentrantLock() + private val statisticsLock: ReentrantLock = new ReentrantLock() // start a new thread to collect statistics private val statisticsThread = new Thread(() => { while (state == Running()) {