michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(util/worker_queue): bug in join method

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-12 23:25:43 +01:00
parent 7ccb9a389c
commit 585127ef66
1 changed files with 13 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/util/worker_queue.h
View file

@ -93,12 +93,12 @@ public:
std::vector<T> const & join() { std::vector<T> const & join() {
lean_assert(!m_done); lean_assert(!m_done);
m_done = true; m_done = true;
#ifndef LEAN_MULTI_THREAD if (m_threads.empty()) {
for (auto const & fn : m_todo) { for (auto const & fn : m_todo) {
m_result.push_back(fn()); m_result.push_back(fn());
} }
m_todo.clear(); m_todo.clear();
#else } else {
m_todo_cv.notify_all(); m_todo_cv.notify_all();
for (thread_ptr & t : m_threads) for (thread_ptr & t : m_threads)
t->join(); t->join();
@ -106,7 +106,7 @@ public:
m_thread_exceptions[m_failed_thread]->rethrow(); m_thread_exceptions[m_failed_thread]->rethrow();
if (m_interrupted) if (m_interrupted)
throw interrupted(); throw interrupted();
#endif }
return m_result; return m_result;
} }