Fixing context disposal vs. statistics thread #3009
Conversation
| // 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() |
There was a problem hiding this comment.
Grabbing the lock before you Thread.sleep() does not look right, it blocks out the other thread for a rather long time.
Why is it necessary?
| @@ -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 | |||
There was a problem hiding this comment.
There is Thread#isInterrupted, I don't think you need an extra local flag
| statisticsThread.interrupt() | ||
| statisticsLock.tryLock(2 * config.z3StatsSec, java.util.concurrent.TimeUnit.SECONDS) |
There was a problem hiding this comment.
Since you're waiting 2*z3StatsSec for the lock, why do you need the interrupt?
I can see how it shortcuts while the thread is sleeping. But then you shouldn't need to wait 2*z3StatsSec afterwards.
Also, what happens if you interrupt it while it's not sleeping?
From the javadoc it does not look like it'd have any effect.
| @@ -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() | |||
|
Did the Z3 downgrade in #3012 fix anything? |
I stopped getting other failures, but this one still appears from time to time |
Closes #3004, hopefully. I feel like I am doing monkey patching with thread synchronization. I know, it must be hilarious, but I keep getting rare core dumps in z3 thanks to the statistics thread. Maybe I should check this code with TLC or Apalache :))
make fmt-fix(or had formatting run automatically on all files edited)./unreleased/][changelog format] for any new functionality