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
243 stars 34 forks source link

Don't use async exceptions to kill threads #534

Closed robdockins closed 4 years ago

robdockins commented 4 years ago

When using sbvWithAny or sbvConcurrentlyWithAny, don't use the ThreadKilled exception to cancel solver threads once we get a result back. If we use an async exception, it will be explicitly filtered by the exception-handling code, leaving the solver processes continuting to work on queries.

Instead, we throw a ExitSuccess value to the threads, which causes them to enter their normal exception-handling stacks. This eventually sends a termination signal to the associated solver processes before killing the associated thread.

Fixes #532

LeventErkok commented 4 years ago

Awesome! Thanks..