Stack-size portfolio fix. If using Boost 1.50, --thread-stack=MB is now supported.

diff --git a/configure.ac b/configure.ac
index 487ec7e3845aa471a700582bd28a0c4e8aa6b95a..6970a7ae2b68fe0a0051b2a60af4ebd1bf4a908e 100644 (file)
--- 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 1a5d2f8ac74eed65c4bd055b841ac934ded181c3..964ce07c11ff72e1387350ff607a0614b38f441c 100644 (file)
--- 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 2f75c88877f86503f97478152c95cff1361e248b..64e10cc531f8a0736eae71199396bac06aaf7623 100644 (file)
--- 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 fdb172c185dbdee714d5a3206d1022a726a3bb71..b9262bfa4d33e88682f8e0b455347911be9cd19a 100644 (file)
--- 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 ebf36b0cdc1ef0bf48b1376dd98a6814a7fee09c..0fd220dbe150335a247d4bede9b2d7bb972965c2 100644 (file)
--- 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 c2d313a4471c61ead1af1ec4c6bcc080ebb03b46..6b75780daf450c3ccb675c8c1c40d9e241ab1efc 100644 (file)
--- 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