From b4e8ea46bed824f1403b1dddcf56a0e8a56bb380 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Tue, 24 Jun 2014 18:44:15 -0400
Subject: Stack-size portfolio fix.  If using Boost 1.50, --thread-stack=MB is
 now supported.

---
 src/main/command_executor_portfolio.cpp |  5 ++++-
 src/main/driver_unified.cpp             |  1 +
 src/main/options                        |  2 ++
 src/main/portfolio.cpp                  | 22 +++++++++++++++++++++-
 src/main/portfolio.h                    |  1 +
 5 files changed, 29 insertions(+), 2 deletions(-)

(limited to 'src')

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
-- 
cgit v1.2.3