diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-06-25 12:39:49 -0400 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-06-25 12:39:49 -0400 |
commit | 6895bd23a22fd63c74a40c17e1a73075d8fdf916 (patch) | |
tree | 10a92f259d198b08fb7885ecbe35a4f229d79aab /src | |
parent | 71155acfab0003572d508861526b83554451aaf7 (diff) | |
parent | b4e8ea46bed824f1403b1dddcf56a0e8a56bb380 (diff) |
Merge pull request #43 from mdeters/threadstack
stack-size portfolio fix. boost 1.50 now required
"The intended behavior is this. If Boost threading library is available and portfolio is requested, we do a try-link during configure that sees if we can set a thread attribute. If that compiles and links, we set a #define in cvc4autoconfig.h. There's a new option --thread-stack=N, with N given in megabytes. 0 is default for the platform (which can be based on ulimit I guess as I mentioned in an email). If --thread-stack=N is given to sequential CVC4, it's an error. If it's given to pcvc4 and N > 0 and there isn't support in that Boost version for it, it's an error."
Diffstat (limited to 'src')
-rw-r--r-- | src/main/command_executor_portfolio.cpp | 5 | ||||
-rw-r--r-- | src/main/driver_unified.cpp | 1 | ||||
-rw-r--r-- | src/main/options | 2 | ||||
-rw-r--r-- | src/main/portfolio.cpp | 22 | ||||
-rw-r--r-- | src/main/portfolio.h | 1 |
5 files changed, 29 insertions, 2 deletions
diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp index 1a5d2f8ac..964ce07c1 100644 --- a/src/main/command_executor_portfolio.cpp +++ b/src/main/command_executor_portfolio.cpp @@ -304,8 +304,11 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) &d_channelsIn[0], &d_smts[0]); + uint64_t threadStackSize = d_options[options::threadStackSize]; + threadStackSize *= 1024 * 1024; + pair<int, bool> portfolioReturn = - runPortfolio(d_numThreads, smFn, fns, + runPortfolio(d_numThreads, smFn, fns, threadStackSize, d_options[options::waitToJoin], d_statWaitTime); #ifdef CVC4_STATISTICS_ON diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 2f75c8887..64e10cc53 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -133,6 +133,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { # ifndef PORTFOLIO_BUILD if( opts.wasSetByUser(options::threads) || + opts.wasSetByUser(options::threadStackSize) || ! opts[options::threadArgv].empty() ) { throw OptionException("Thread options cannot be used with sequential CVC4. Please build and use the portfolio binary `pcvc4'."); } diff --git a/src/main/options b/src/main/options index fdb172c18..b9262bfa4 100644 --- a/src/main/options +++ b/src/main/options @@ -28,6 +28,8 @@ option threads --threads=N unsigned :default 2 :predicate greater(0) Total number of threads for portfolio option - --threadN=string void :handler CVC4::main::threadN :handler-include "main/options_handlers.h" configures portfolio thread N (0..#threads-1) +option threadStackSize --thread-stack=N unsigned :default 0 + stack size for worker threads in MB (0 means use Boost/thread lib default) option threadArgv std::vector<std::string> :include <vector> <string> Thread configuration (a string to be passed to parseOptions) option thread_id int :default -1 diff --git a/src/main/portfolio.cpp b/src/main/portfolio.cpp index ebf36b0cd..0fd220dbe 100644 --- a/src/main/portfolio.cpp +++ b/src/main/portfolio.cpp @@ -62,6 +62,7 @@ template<typename T, typename S> std::pair<int, S> runPortfolio(int numThreads, boost::function<T()> driverFn, boost::function<S()> threadFns[], + uint64_t stackSize, bool optionWaitToJoin, TimerStat& statWaitTime) { boost::thread thread_driver; @@ -72,9 +73,27 @@ std::pair<int, S> runPortfolio(int numThreads, global_winner = -1; for(int t = 0; t < numThreads; ++t) { - threads[t] = + +#if BOOST_HAS_THREAD_ATTR + boost::thread::attributes attrs; + + if(stackSize > 0) { + attrs.set_stack_size(stackSize); + } + + threads[t] = + boost::thread(attrs, boost::bind(runThread<S>, t, threadFns[t], + boost::ref(threads_returnValue[t]) ) ); +#else /* BOOST_HAS_THREAD_ATTR */ + if(stackSize > 0) { + throw OptionException("cannot specify a stack size for worker threads; requires CVC4 to be built with Boost thread library >= 1.50.0"); + } + + threads[t] = boost::thread(boost::bind(runThread<S>, t, threadFns[t], boost::ref(threads_returnValue[t]) ) ); +#endif /* BOOST_HAS_THREAD_ATTR */ + } if(not driverFn.empty()) @@ -112,6 +131,7 @@ std::pair<int, bool> runPortfolio<void, bool>(int, boost::function<void()>, boost::function<bool()>*, + uint64_t, bool, TimerStat&); diff --git a/src/main/portfolio.h b/src/main/portfolio.h index c2d313a44..6b75780da 100644 --- a/src/main/portfolio.h +++ b/src/main/portfolio.h @@ -30,6 +30,7 @@ template<typename T, typename S> std::pair<int, S> runPortfolio(int numThreads, boost::function<T()> driverFn, boost::function<S()> threadFns[], + size_t stackSize, bool optionWaitToJoin, TimerStat& statWaitTime); // as we have defined things, S=void would give compile errors |