niklasso / minisat

A minimalistic and high-performance SAT solver
minisat.se
Other
1.02k stars 390 forks source link

Async interrupt should not work #21

Open msoos opened 9 years ago

msoos commented 9 years ago

The Solver::interrupt(){ asynch_interrupt = true; } with bool asynch_interrupt; should not really work -- it's not clear that asynch_interrupt can be changed from another thread and the compiler is completely at liberty to optimize out the check (as I suspect it does). It should have lock/atomic/etc. primitives around it so the compiler is aware that it can be changed from elsewhere. Also note that using volatile does not fix this issue -- it does not signal the system that another thread might change the value and so it does not force a memory sync between the threads. A memory barrier is needed before every access to it from any thread, i.e. one after the change in interrupt() and one everywhere where the value of asynch_interrupt is checked.