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

fix(library/module): potential deadlock when child thread threw an exception

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-07 20:34:18 -07:00
parent 25b822b1c7
commit 7124866a4f
1 changed files with 8 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/library/module.cpp
View file

@ -358,23 +358,29 @@ struct import_modules_fn {
return;
std::vector<std::unique_ptr<interruptible_thread>> extra_threads;
std::vector<std::unique_ptr<exception>> thread_exceptions(m_num_threads - 1);
atomic<int> failed_thread_idx(-1); // >= 0 if error
for (unsigned i = 0; i < m_num_threads - 1; i++) {
extra_threads.push_back(std::unique_ptr<interruptible_thread>(new interruptible_thread([=, &thread_exceptions]() {
extra_threads.push_back(std::unique_ptr<interruptible_thread>(new interruptible_thread([=, &thread_exceptions, &failed_thread_idx]() {
try {
while (auto t = next_task()) {
(*t)(m_senv);
}
m_asynch_cv.notify_all();
} catch (exception ex) {
} catch (exception & ex) {
thread_exceptions[i].reset(ex.clone());
failed_thread_idx = i;
} catch (...) {
thread_exceptions[i].reset(new exception("module import thread failed for unknown reasons"));
failed_thread_idx = i;
}
})));
}
try {
while (auto t = next_task()) {
(*t)(m_senv);
int idx = failed_thread_idx;
if (idx >= 0)
thread_exceptions[idx]->rethrow();
}
m_asynch_cv.notify_all();
for (auto & th : extra_threads)
@ -386,10 +392,6 @@ struct import_modules_fn {
th->join();
throw;
}
for (auto const & ex : thread_exceptions) {
if (ex.get())
ex->rethrow();
}
}
environment process_delayed_tasks() {