search

LeventErkok / sbv

SMT Based Verification in Haskell. Express properties about Haskell programs and automatically prove them using SMT solvers.
https://github.com/LeventErkok/sbv
Other
239 stars 33 forks source link

Fix the zombie solver processes mentioned in #477 #691

Closed lsrcz closed 3 months ago

lsrcz commented 4 months ago

I encountered the same issue as mentioned in #477, and this pull request tries to fix it. I do not fully understand the codebase, so please carefully review my changes.

I believe that the root cause of the issue is that the queryTerminate (i.e., the cleanUp function defined in runSolver) is skipped when an exception happens before it but after the solver has been started by the runSolver call.

This pull request moves the termination of the solver to executeQuery function, and terminates it immediately after we finished all the interaction with the solver. In this function, we have the handy ExtractIO class, which allows us to do the clean up no matter whether an exception is raised with finally.

The ExtractIO instance for IO is also buggy, though. It violates the law mentioned in the comment. This pull request also fixes it, and the fix is required for the clean up to work. https://github.com/LeventErkok/sbv/blob/ddd2c87f280e3bd29d1115b388282ec3a9b2647b/Data/SBV/Utils/ExtractIO.hs#L29-L31

After doing these changes, I observed no zombie or long-running processes after killing a thread running sbv.

LeventErkok commented 4 months ago

Great! Unfortunately I’m away from any decent computing device till about May 15th. I’ll take a look at that time.

I’m happy to merge to mainline if you’ve an urgent need. Let me know.

lsrcz commented 4 months ago

No hurry, I can rely on my own patched version for now.