src/main/command_executor_portfolio.cpp

   1 /*********************                                                        */
   2 /*! \file command_executor_portfolio.cpp
   3  ** \verbatim
   4  ** Original author: Morgan Deters
   5  ** Major contributors: Kshitij Bansal
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2013  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** information.\endverbatim
  11  **
  12  ** \brief An additional layer between commands and invoking them.
  13  **
  14  ** The portfolio executer branches check-sat queries to several
  15  ** threads.
  16  **/
  17
  18 #include <boost/thread.hpp>
  19 #include <boost/thread/condition.hpp>
  20 #include <boost/exception_ptr.hpp>
  21 #include <boost/lexical_cast.hpp>
  22 #include <string>
  23
  24 #include "expr/command.h"
  25 #include "expr/pickler.h"
  26 #include "main/command_executor_portfolio.h"
  27 #include "main/main.h"
  28 #include "main/options.h"
  29 #include "main/portfolio.h"
  30 #include "options/options.h"
  31 #include "smt/options.h"
  32
  33 #include "cvc4autoconfig.h"
  34
  35 #if HAVE_UNISTD_H
  36 #  include <unistd.h>
  37 #endif /* HAVE_UNISTD_H */
  38
  39 using namespace std;
  40
  41 namespace CVC4 {
  42 namespace main {
  43
  44 CommandExecutorPortfolio::CommandExecutorPortfolio
  45 (ExprManager &exprMgr, Options &options, vector<Options>& tOpts):
  46   CommandExecutor(exprMgr, options),
  47   d_numThreads(options[options::threads]),
  48   d_smts(),
  49   d_seq(new CommandSequence()),
  50   d_threadOptions(tOpts),
  51   d_vmaps(),
  52   d_lastWinner(0),
  53   d_channelsOut(),
  54   d_channelsIn(),
  55   d_ostringstreams(),
  56   d_statLastWinner("portfolio::lastWinner"),
  57   d_statWaitTime("portfolio::waitTime")
  58 {
  59   assert(d_threadOptions.size() == d_numThreads);
  60
  61   d_statLastWinner.setData(d_lastWinner);
  62   d_stats.registerStat_(&d_statLastWinner);
  63   d_stats.registerStat_(&d_statWaitTime);
  64
  65   /* Duplication, Individualisation */
  66   d_exprMgrs.push_back(&d_exprMgr);
  67   for(unsigned i = 1; i < d_numThreads; ++i) {
  68     d_exprMgrs.push_back(new ExprManager(d_threadOptions[i]));
  69   }
  70
  71   // Create the SmtEngine(s)
  72   d_smts.push_back(d_smtEngine);
  73   for(unsigned i = 1; i < d_numThreads; ++i) {
  74     d_smts.push_back(new SmtEngine(d_exprMgrs[i]));
  75   }
  76
  77   assert(d_vmaps.size() == 0);
  78   for(unsigned i = 0; i < d_numThreads; ++i) {
  79     d_vmaps.push_back(new ExprManagerMapCollection());
  80   }
  81 }
  82
  83 CommandExecutorPortfolio::~CommandExecutorPortfolio()
  84 {
  85   assert(d_seq != NULL);
  86   delete d_seq;
  87
  88   assert(d_smts.size() == d_numThreads);
  89   for(unsigned i = 1; i < d_numThreads; ++i) {
  90     // the 0-th one is responsibility of parent class
  91
  92     delete d_smts[i];
  93     delete d_exprMgrs[i];
  94   }
  95   d_exprMgrs.clear();
  96   d_smts.clear();
  97
  98   d_stats.unregisterStat_(&d_statLastWinner);
  99   d_stats.unregisterStat_(&d_statWaitTime);
 100 }
 101
 102 void CommandExecutorPortfolio::lemmaSharingInit()
 103 {
 104   /* Sharing channels */
 105   assert(d_channelsIn.size() == 0);
 106   assert(d_channelsOut.size() == 0);
 107
 108   if(d_numThreads == 1) {
 109     // Disable sharing
 110     d_threadOptions[0].set(options::sharingFilterByLength, 0);
 111   } else {
 112     // Setup sharing channels
 113     const unsigned int sharingChannelSize = 1000000;
 114
 115     for(unsigned i = 0; i < d_numThreads; ++i){
 116       d_channelsOut.push_back
 117         (new SynchronizedSharedChannel<ChannelFormat>(sharingChannelSize));
 118       d_channelsIn.push_back
 119         (new SynchronizedSharedChannel<ChannelFormat>(sharingChannelSize));
 120     }
 121
 122     /* Lemma I/O channels */
 123     for(unsigned i = 0; i < d_numThreads; ++i) {
 124       string tag = "thread #" +
 125         boost::lexical_cast<string>(d_threadOptions[i][options::thread_id]);
 126       d_threadOptions[i].set
 127         (options::lemmaOutputChannel,
 128          new PortfolioLemmaOutputChannel(tag, d_channelsOut[i], d_exprMgrs[i],
 129                                          d_vmaps[i]->d_from, d_vmaps[i]->d_to));
 130       d_threadOptions[i].set
 131         (options::lemmaInputChannel,
 132          new PortfolioLemmaInputChannel(tag, d_channelsIn[i], d_exprMgrs[i],
 133                                         d_vmaps[i]->d_from, d_vmaps[i]->d_to));
 134     }
 135
 136     /* Output to string stream  */
 137     assert(d_ostringstreams.size() == 0);
 138     for(unsigned i = 0; i < d_numThreads; ++i) {
 139       d_ostringstreams.push_back(new ostringstream);
 140       d_threadOptions[i].set(options::out, d_ostringstreams[i]);
 141
 142       // important even for muzzled builds (to get result output right)
 143       *d_threadOptions[i][options::out]
 144         << Expr::setlanguage(d_threadOptions[i][options::outputLanguage]);
 145     }
 146   }
 147 }/* CommandExecutorPortfolio::lemmaSharingInit() */
 148
 149 void CommandExecutorPortfolio::lemmaSharingCleanup()
 150 {
 151   assert(d_numThreads == d_options[options::threads]);
 152
 153   if(d_numThreads == 1)
 154     return;
 155
 156   // Channel cleanup
 157   assert(d_channelsIn.size() == d_numThreads);
 158   assert(d_channelsOut.size() == d_numThreads);
 159   for(unsigned i = 0; i < d_numThreads; ++i) {
 160     delete d_channelsIn[i];
 161     delete d_channelsOut[i];
 162     d_threadOptions[i].set(options::lemmaInputChannel, NULL);
 163     d_threadOptions[i].set(options::lemmaOutputChannel, NULL);
 164   }
 165   d_channelsIn.clear();
 166   d_channelsOut.clear();
 167
 168   // sstreams cleanup (if used)
 169   if(d_ostringstreams.size() != 0) {
 170     assert(d_ostringstreams.size() == d_numThreads);
 171     for(unsigned i = 0; i < d_numThreads; ++i) {
 172       d_threadOptions[i].set(options::out, d_options[options::out]);
 173       delete d_ostringstreams[i];
 174     }
 175     d_ostringstreams.clear();
 176   }
 177
 178 }/* CommandExecutorPortfolio::lemmaSharingCleanup() */
 179
 180
 181 bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
 182 {
 183   /**
 184    * save the command and if check sat or query command, run a
 185    * porfolio of SMT solvers.
 186    */
 187
 188   int mode = 0;
 189   // mode = 0 : run command on lastWinner, saving the command
 190   // to be run on all others
 191   //
 192   // mode = 1 : run a race of the command, update lastWinner
 193   //
 194   // mode = 2 : run _only_ the lastWinner thread, not saving the
 195   // command
 196
 197   if(dynamic_cast<CheckSatCommand*>(cmd) != NULL ||
 198      dynamic_cast<QueryCommand*>(cmd) != NULL) {
 199     mode = 1;
 200   } else if(dynamic_cast<GetValueCommand*>(cmd) != NULL ||
 201             dynamic_cast<GetAssignmentCommand*>(cmd) != NULL ||
 202             dynamic_cast<GetModelCommand*>(cmd) != NULL ||
 203             dynamic_cast<GetProofCommand*>(cmd) != NULL ||
 204             dynamic_cast<GetUnsatCoreCommand*>(cmd) != NULL ||
 205             dynamic_cast<GetAssertionsCommand*>(cmd) != NULL ||
 206             dynamic_cast<GetInfoCommand*>(cmd) != NULL ||
 207             dynamic_cast<GetOptionCommand*>(cmd) != NULL ||
 208             false) {
 209     mode = 2;
 210   }
 211
 212   Debug("portfolio::outputmode") << "Mode is " << mode
 213                                  << "lastWinner is " << d_lastWinner
 214                                  << "d_seq is " << d_seq << std::endl;
 215
 216   if(mode == 0) {
 217     d_seq->addCommand(cmd->clone());
 218     Command* cmdExported =
 219       d_lastWinner == 0 ?
 220       cmd : cmd->exportTo(d_exprMgrs[d_lastWinner], *(d_vmaps[d_lastWinner]) );
 221     bool ret = smtEngineInvoke(d_smts[d_lastWinner],
 222                                cmdExported,
 223                                d_options[options::verbosity] >= -1 ? d_threadOptions[d_lastWinner][options::out] : NULL);
 224     if(d_lastWinner != 0) delete cmdExported;
 225     return ret;
 226   } else if(mode == 1) {               // portfolio
 227     d_seq->addCommand(cmd->clone());
 228
 229     // We currently don't support changing number of threads for each
 230     // command, but things have been architected in a way so that this
 231     // can be achieved without a lot of work.
 232     Command *seqs[d_numThreads];
 233
 234     if(d_lastWinner == 0)
 235       seqs[0] = cmd;
 236     else
 237       seqs[0] = d_seq;
 238
 239     /* variable maps and exporting */
 240     for(unsigned i = 1; i < d_numThreads; ++i) {
 241       /**
 242        * vmaps[i].d_from [x] = y means
 243        *    that in thread #0's expr manager id is y
 244        *    and  in thread #i's expr manager id is x
 245        * opposite for d_to
 246        *
 247        * d_from[x] : in a sense gives the id if converting *from* it to
 248        *             first thread
 249        */
 250       try {
 251         seqs[i] =
 252           int(i) == d_lastWinner ?
 253           cmd->exportTo(d_exprMgrs[i], *(d_vmaps[i])) :
 254           d_seq->exportTo(d_exprMgrs[i], *(d_vmaps[i]) );
 255       } catch(ExportUnsupportedException& e) {
 256         if(d_options[options::fallbackSequential]) {
 257           Notice() << "Unsupported theory encountered, switching to sequential mode.";
 258           return CommandExecutor::doCommandSingleton(cmd);
 259         }
 260         else
 261           throw Exception("Certain theories (e.g., datatypes) are (currently) unsupported in portfolio\n"
 262                           "mode. Please see option --fallback-sequential to make this a soft error.");
 263       }
 264     }
 265
 266     /**
 267      * Create identity variable map for the first thread, with only
 268      * those variables which have a corresponding variable in
 269      * another thread. (TODO: Also assert, all threads have the same
 270      * set of variables mapped.)
 271      */
 272     if(d_numThreads >= 2) {
 273       for(typeof(d_vmaps[1]->d_to.begin()) i=d_vmaps[1]->d_to.begin();
 274           i!=d_vmaps[1]->d_to.end(); ++i) {
 275         (d_vmaps[0]->d_from)[i->first] = i->first;
 276       }
 277       d_vmaps[0]->d_to = d_vmaps[0]->d_from;
 278     }
 279
 280     lemmaSharingInit();
 281
 282     /* Portfolio */
 283     boost::function<bool()>* fns = new boost::function<bool()>[d_numThreads];
 284     for(unsigned i = 0; i < d_numThreads; ++i) {
 285       fns[i] = boost::bind(smtEngineInvoke,
 286                            d_smts[i],
 287                            seqs[i],
 288                            d_options[options::verbosity] >= -1 ? d_threadOptions[i][options::out] : NULL
 289                            );
 290     }
 291
 292     assert(d_channelsIn.size() == d_numThreads
 293            || d_numThreads == 1);
 294     assert(d_channelsOut.size() == d_numThreads
 295            || d_numThreads == 1);
 296     assert(d_smts.size() == d_numThreads);
 297     assert( !d_statWaitTime.running() );
 298
 299     boost::function<void()>
 300       smFn = d_numThreads <= 1 ? boost::function<void()>() :
 301              boost::bind(sharingManager<ChannelFormat>,
 302                          d_numThreads,
 303                          &d_channelsOut[0],
 304                          &d_channelsIn[0],
 305                          &d_smts[0]);
 306
 307     uint64_t threadStackSize = d_options[options::threadStackSize];
 308     threadStackSize *= 1024 * 1024;
 309
 310     pair<int, bool> portfolioReturn =
 311         runPortfolio(d_numThreads, smFn, fns, threadStackSize,
 312                      d_options[options::waitToJoin], d_statWaitTime);
 313
 314 #ifdef CVC4_STATISTICS_ON
 315     assert( d_statWaitTime.running() );
 316     d_statWaitTime.stop();
 317 #endif /* CVC4_STATISTICS_ON */
 318
 319     delete d_seq;
 320     d_seq = new CommandSequence();
 321
 322     d_lastWinner = portfolioReturn.first;
 323     d_result = d_smts[d_lastWinner]->getStatusOfLastCommand();
 324
 325     if(d_ostringstreams.size() != 0) {
 326       assert(d_numThreads == d_options[options::threads]);
 327       assert(portfolioReturn.first >= 0);
 328       assert(unsigned(portfolioReturn.first) < d_numThreads);
 329
 330       if(Debug.isOn("treat-unknown-error")) {
 331         if(d_ostringstreams[portfolioReturn.first]->str() == "unknown\n") {
 332           *d_options[options::out]
 333             << "portfolioReturn = (" << portfolioReturn.first << ", " << portfolioReturn.second
 334             << ")\n";
 335           for(unsigned i = 0; i < d_numThreads; ++i)
 336             *d_options[options::out]
 337               << "thread " << i << ": " << d_ostringstreams[i]->str() << std::endl;
 338           throw Exception("unknown encountered");
 339         }
 340       }
 341
 342       *d_options[options::out]
 343         << d_ostringstreams[portfolioReturn.first]->str()
 344         << std::flush;
 345
 346 #ifdef CVC4_COMPETITION_MODE
 347       // There's some hang-up in thread destruction?
 348       // Anyway for SMT-COMP we don't care, just exit now.
 349       _exit(0);
 350 #endif /* CVC4_COMPETITION_MODE */
 351     }
 352
 353     /* cleanup this check sat specific stuff */
 354     lemmaSharingCleanup();
 355
 356     delete[] fns;
 357
 358     bool status = portfolioReturn.second;
 359
 360     // dump the model/proof if option is set
 361     if(status) {
 362       if( d_options[options::produceModels] &&
 363           d_options[options::dumpModels] &&
 364           ( d_result.asSatisfiabilityResult() == Result::SAT ||
 365             (d_result.isUnknown() && d_result.whyUnknown() == Result::INCOMPLETE) ) ) {
 366         Command* gm = new GetModelCommand();
 367         status = doCommandSingleton(gm);
 368       } else if( d_options[options::proof] &&
 369                  d_options[options::dumpProofs] &&
 370                  d_result.asSatisfiabilityResult() == Result::UNSAT ) {
 371         Command* gp = new GetProofCommand();
 372         status = doCommandSingleton(gp);
 373       } else if( d_options[options::dumpInstantiations] &&
 374                  d_result.asSatisfiabilityResult() == Result::UNSAT ) {
 375         Command* gi = new GetInstantiationsCommand();
 376         status = doCommandSingleton(gi);
 377       }
 378     }
 379
 380     return status;
 381   } else if(mode == 2) {
 382     Command* cmdExported =
 383       d_lastWinner == 0 ?
 384       cmd : cmd->exportTo(d_exprMgrs[d_lastWinner], *(d_vmaps[d_lastWinner]) );
 385     bool ret = smtEngineInvoke(d_smts[d_lastWinner],
 386                                cmdExported,
 387                                d_options[options::verbosity] >= -1 ? d_threadOptions[d_lastWinner][options::out] : NULL);
 388     if(d_lastWinner != 0) delete cmdExported;
 389     return ret;
 390   } else {
 391     // Unreachable();
 392     assert(false);
 393     return false;
 394   }
 395
 396 }/* CommandExecutorPortfolio::doCommandSingleton() */
 397
 398 void CommandExecutorPortfolio::flushStatistics(std::ostream& out) const {
 399   assert(d_numThreads == d_exprMgrs.size() && d_exprMgrs.size() == d_smts.size());
 400   for(size_t i = 0; i < d_numThreads; ++i) {
 401     string emTag = "thread#"
 402       + boost::lexical_cast<string>(d_threadOptions[i][options::thread_id]);
 403     Statistics stats = d_exprMgrs[i]->getStatistics();
 404     stats.setPrefix(emTag);
 405     stats.flushInformation(out);
 406
 407     string smtTag = "thread#"
 408       + boost::lexical_cast<string>(d_threadOptions[i][options::thread_id]);
 409     stats = d_smts[i]->getStatistics();
 410     stats.setPrefix(smtTag);
 411     stats.flushInformation(out);
 412   }
 413   d_stats.flushInformation(out);
 414 }
 415
 416 }/* CVC4::main namespace */
 417 }/* CVC4 namespace */