diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-11-28 21:52:56 +0000 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-11-28 21:52:56 +0000 |
commit | f0ebc08cf865d654a6d7ca4361775db8a64b1f62 (patch) | |
tree | 5ae2f40355dc3b581506aa467f7fd6f555212908 /src/main | |
parent | 436a0aac57b3217ad7f0e463cf4cf29b807581e4 (diff) |
fix a potential race (have failed to reproduce)
Diffstat (limited to 'src/main')
-rw-r--r-- | src/main/portfolio.cpp | 20 |
1 files changed, 14 insertions, 6 deletions
diff --git a/src/main/portfolio.cpp b/src/main/portfolio.cpp index 4c542f548..e4b31f54d 100644 --- a/src/main/portfolio.cpp +++ b/src/main/portfolio.cpp @@ -25,9 +25,12 @@ namespace CVC4 { +/** Mutex to make sure at most one thread is winner */ boost::mutex mutex_done; + +/** Mutex / condition variable to notify main when winner data written */ boost::mutex mutex_main_wait; -boost::condition condition_var_main_wait; +boost::condition_variable condition_var_main_wait; bool global_flag_done; int global_winner; @@ -38,12 +41,16 @@ void runThread(int thread_id, boost::function<S()> threadFn, S& returnValue) returnValue = threadFn(); if( mutex_done.try_lock() ) { - if(global_flag_done == false) { - global_flag_done = true; - global_winner = thread_id; + if(global_flag_done == false) + { + { + boost::lock_guard<boost::mutex> lock(mutex_main_wait); + global_winner = thread_id; + global_flag_done = true; + } + condition_var_main_wait.notify_all(); // we want main thread to quit } mutex_done.unlock(); - condition_var_main_wait.notify_all(); // we want main thread to quit } } @@ -68,8 +75,9 @@ std::pair<int, S> runPortfolio(int numThreads, if(not driverFn.empty()) thread_driver = boost::thread(driverFn); + boost::unique_lock<boost::mutex> lock(mutex_main_wait); while(global_flag_done == false) - condition_var_main_wait.wait(mutex_main_wait); + condition_var_main_wait.wait(lock); if(not driverFn.empty()) { thread_driver.interrupt(); |