scoped_timer::finalize is called from fork. However, it may race with
other threads creating or freeing timer threads.
This patch removes the loop in scoped_timer::finalize (because it is not
needed and it may spin) and also removes two unlocked assignments.
The idle thread is added to "available_workers" in
scoped_timer::~scoped_timer destructor.
If we call the "finalize" method as a part of total memory cleanup, all
the scoped_timers' destructors were already executed and all the worker
threads are already on "available_workers" vector. So, we don't need to
loop; the first loop iteration will clean all the threads.
If the "finalize" method is called from single-threaded program's fork(),
then all the scoped timers' destructors are already called and the case
is analogous to the previous case.
If the "finalize" method is called from multi-threaded program's fork(),
then it breaks down - the "num_workers" variable is the total amount of
workers (both sleeping and busy), and we loop until we terminated
"num_workers" threads - that means that if the number of sleeping workers
is less than "num_workers", the function just spins.
Then, there is unlocked assignment to "num_workers = 0" and
"available_workers.clear()" that can race with other threads doing z3
work and corrupt memory. available_workers.clear() is not needed, because
it was already cleared by std::swap(available_workers, cleanup_workers)
(and that was correctly locked).
Signed-off-by: Mikulas Patocka <mikulas@twibright.com>
* Check that Z3_get_numeral_small is given non-null out params
Analogous to other Z3_get_numeral_* functions with out params.
* Note that Z3_get_numeral_small is essentially redundant
The error behavior of Z3_get_numeral_small does not follow the pattern of
the other functions. The functions that have out params and return a bool
indicating success (such as Z3_get_numeral_rational_int64) return false
rather than signaling an error when given an unsupported expression
argument (such as a rounding mode value). The functions that do not have out
params signal an error in such cases. Z3_get_numeral_small is the odd one
out in that it signals errors and returns a status bool.
This error handling is the only difference between Z3_get_numeral_small and
Z3_get_numeral_rational_int64, so this patch adds a comment to the
documentation.
