From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Tue, 24 Jun 2014 22:44:15 +0000 (-0400)
Subject: Stack-size portfolio fix.  If using Boost 1.50, --thread-stack=MB is now supported.
X-Git-Tag: cvc5-1.0.0~6728^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b4e8ea46bed824f1403b1dddcf56a0e8a56bb380;p=cvc5.git

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

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