portfolio: add stat to track time spent waiting for interrupted threads to stop

6 files changed, 33 insertions, 7 deletions

diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp
index 24469c668..7392b2b62 100644
--- a/src/main/command_executor_portfolio.cpp
+++ b/src/main/command_executor_portfolio.cpp
@@ -47,12 +47,14 @@ CommandExecutorPortfolio::CommandExecutorPortfolio
   d_channelsOut(),
   d_channelsIn(),
   d_ostringstreams(),
-  d_statLastWinner("portfolio::lastWinner")
+  d_statLastWinner("portfolio::lastWinner"),
+  d_statWaitTime("portfolio::waitTime")
 {
   assert(d_threadOptions.size() == d_numThreads);
 
   d_statLastWinner.setData(d_lastWinner);
   d_stats.registerStat_(&d_statLastWinner);
+  d_stats.registerStat_(&d_statWaitTime);
 
   /* Duplication, Individualisation */
   d_exprMgrs.push_back(&d_exprMgr);
@@ -86,6 +88,9 @@ CommandExecutorPortfolio::~CommandExecutorPortfolio()
   }
   d_exprMgrs.clear();
   d_smts.clear();
+
+  d_stats.unregisterStat_(&d_statLastWinner);
+  d_stats.unregisterStat_(&d_statWaitTime);
 }
 
 void CommandExecutorPortfolio::lemmaSharingInit()
@@ -283,6 +288,8 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
     assert(d_channelsOut.size() == d_numThreads
            || d_numThreads == 1);
     assert(d_smts.size() == d_numThreads);
+    assert( !d_statWaitTime.running() );
+
     boost::function<void()>
       smFn = d_numThreads <= 1 ? boost::function<void()>() :
              boost::bind(sharingManager<ChannelFormat>,
@@ -293,7 +300,10 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
 
     pair<int, bool> portfolioReturn =
         runPortfolio(d_numThreads, smFn, fns,
-                     d_options[options::waitToJoin]);
+                     d_options[options::waitToJoin], d_statWaitTime);
+
+    assert( d_statWaitTime.running() );
+    d_statWaitTime.stop();
 
     delete d_seq;
     d_seq = new CommandSequence();
diff --git a/src/main/command_executor_portfolio.h b/src/main/command_executor_portfolio.h
index a8d4a4213..91f9a5169 100644
--- a/src/main/command_executor_portfolio.h
+++ b/src/main/command_executor_portfolio.h
@@ -52,6 +52,7 @@ class CommandExecutorPortfolio : public CommandExecutor {
 
   // Stats
   ReferenceStat<int> d_statLastWinner;
+  TimerStat d_statWaitTime;
 
 public:
   CommandExecutorPortfolio(ExprManager &exprMgr,
diff --git a/src/main/portfolio.cpp b/src/main/portfolio.cpp
index 21c1b60a3..ebf36b0cd 100644
--- a/src/main/portfolio.cpp
+++ b/src/main/portfolio.cpp
@@ -21,8 +21,10 @@
 
 #include "smt/smt_engine.h"
 #include "util/result.h"
+#include "util/statistics_registry.h"
 #include "options/options.h"
 
+
 namespace CVC4 {
 
 /** Mutex to make sure at most one thread is winner */
@@ -60,7 +62,8 @@ template<typename T, typename S>
 std::pair<int, S> runPortfolio(int numThreads,
                                boost::function<T()> driverFn,
                                boost::function<S()> threadFns[],
-                               bool optionWaitToJoin) {
+                               bool optionWaitToJoin,
+                               TimerStat& statWaitTime) {
   boost::thread thread_driver;
   boost::thread* threads = new boost::thread[numThreads];
   S* threads_returnValue = new S[numThreads];
@@ -82,6 +85,8 @@ std::pair<int, S> runPortfolio(int numThreads,
     condition_var_main_wait.wait(lock);
   }
 
+  statWaitTime.start();
+
   if(not driverFn.empty()) {
     thread_driver.interrupt();
     thread_driver.join();
@@ -107,6 +112,7 @@ std::pair<int, bool>
 runPortfolio<void, bool>(int,
                          boost::function<void()>, 
                          boost::function<bool()>*,
-                         bool);
+                         bool,
+                         TimerStat&);
 
 }/* CVC4 namespace */
diff --git a/src/main/portfolio.h b/src/main/portfolio.h
index 61a4c055f..c2d313a44 100644
--- a/src/main/portfolio.h
+++ b/src/main/portfolio.h
@@ -22,14 +22,16 @@
 #include "smt/smt_engine.h"
 #include "expr/command.h"
 #include "options/options.h"
+#include "util/statistics_registry.h"
 
 namespace CVC4 {
 
 template<typename T, typename S>
 std::pair<int, S> runPortfolio(int numThreads, 
-                              boost::function<T()> driverFn,
-                              boost::function<S()> threadFns[],
-                              bool optionWaitToJoin);
+                               boost::function<T()> driverFn,
+                               boost::function<S()> threadFns[],
+                               bool optionWaitToJoin,
+                               TimerStat& statWaitTime);
 // as we have defined things, S=void would give compile errors
 // do we want to fix this? yes, no, maybe?
 
diff --git a/src/util/statistics_registry.cpp b/src/util/statistics_registry.cpp
index 67cc3a53c..61762b84d 100644
--- a/src/util/statistics_registry.cpp
+++ b/src/util/statistics_registry.cpp
@@ -119,6 +119,10 @@ void TimerStat::stop() {
   }
 }/* TimerStat::stop() */
 
+bool TimerStat::running() const {
+  return d_running;
+}/* TimerStat::running() */
+
 timespec TimerStat::getData() const {
   ::timespec data = d_data;
   if(__CVC4_USE_STATISTICS && d_running) {
diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h
index eb5245e25..bd33557d9 100644
--- a/src/util/statistics_registry.h
+++ b/src/util/statistics_registry.h
@@ -808,6 +808,9 @@ public:
    */
   void stop();
 
+  /** If the timer is currently running */
+  bool running() const;
+
   timespec getData() const;
 
   SExpr getValue() const;