diff options
| -rw-r--r-- | configure.ac | 24 | ||||
| -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 |
6 files changed, 53 insertions, 2 deletions
diff --git a/configure.ac b/configure.ac index 487ec7e38..6970a7ae2 100644 --- a/configure.ac +++ b/configure.ac @@ -1045,7 +1045,31 @@ fi AM_CONDITIONAL([CVC4_BUILD_PCVC4], [test "$with_portfolio" = yes]) if test "$with_portfolio" = yes; then CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_PORTFOLIO" + + # see if Boost has thread attributes (should be any version >= 1.50.0) + # non-fatal error if not, but we won't support --thread-stack option + AC_MSG_CHECKING([whether Boost threads support thread attrs]) + AC_LANG_PUSH([C++]) + cvc4_save_CPPFLAGS="$CPPFLAGS" + cvc4_save_LIBS="$LIBS" + cvc4_save_LDFLAGS="$LDFLAGS" + CPPFLAGS="$CPPFLAGS $BOOST_CPPFLAGS" + LIBS="$LIBS $BOOST_THREAD_LIBS" + LDFLAGS="$LDFLAGS $BOOST_THREAD_LDFLAGS" + AC_LINK_IFELSE([AC_LANG_PROGRAM([#include <boost/thread.hpp>], + [boost::thread::attributes attrs; attrs.set_stack_size(10 * 1024 * 1024);])], + [cvc4_boost_has_thread_attr=1; + AC_MSG_RESULT([yes])], + [cvc4_boost_has_thread_attr=0; + AC_MSG_RESULT([no])]) + CPPFLAGS="$cvc4_save_CPPFLAGS" + LIBS="$cvc4_save_LIBS" + LDFLAGS="$cvc4_save_LDFLAGS" + AC_LANG_POP([C++]) +else + cvc4_boost_has_thread_attr=0 fi +AC_DEFINE_UNQUOTED([BOOST_HAS_THREAD_ATTR], $cvc4_boost_has_thread_attr, [Define to 1 if Boost threading library has support for thread attributes]) # Check for libreadline (defined in config/readline.m4) AC_ARG_WITH([readline], [AS_HELP_STRING([--with-readline], [support the readline library])], [], [with_readline=check]) 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 |