The scoped_timer uses a std::therad. Spawning this thread fails in cases of WASM.
Instead of adapting builds and using async features at the level of WASM and the client, we expose a specialized version of z3 that doesn't use threads at all, neither for solvers nor for timers.
The tradeoff is that the periodic poll that checks for timeout directly queries the global clock each time.
We characterize it as based on polling.
* on POSIX systems, fork() is dangerous in the presence of a thread
pool, because the child process inherits only the thread from the
parent that actually called fork().
this patch winds down the scoped_timer thread pool in preparation for
forking; workers will get freshly created again following the fork
call.
creating a fresh thread for every scoped_timer has significant overhead
in some use cases. this patch creates a persistent pool of worker threads
to do this job, resulting in 20-30% speedup of some alive2 jobs on a
large multicore
@nunolopes .
If `pthread_cond_signal()` is called while `m_mutex` is held then the
timing thread might be woken up twice due to waking up from
`pthread_cond_timeout()` (due to being signaled) but then being forced
to sleep again because the thread calling `~imp()` is still holding
`m_mutex` (which the timing thread needs to acquire).
incorrectly assumed that `pthread_cond_timedwait()` would exit
due to a condition variable being signaled or a timeout occuring.
According to the documentation `pthread_cond_timedwait()` might
spuriously wake so we introduce a new variable `m_signal_sent` (that is
guarded by an existing mutex) that is used as the variable to check that
the thread wake was not spurious.
This is intended to partially fix#839 .
The previous version was racy and could lead to crashes.
The timer could be deleted before the callback was called, making it execute on already freed memory
This new version is similar to Mac's. It spawns its own thread and uses pthread_cond_wait.
Care is taken for small timeouts to avoid races in the thread creation and timer destruction.
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
