1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
|
/********************* */
/*! \file portfolio.cpp
** \verbatim
** Original author: Morgan Deters
** Major contributors: Kshitij Bansal
** Minor contributors (to current version): none
** This file is part of the CVC4 project.
** Copyright (c) 2009-2013 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
** \brief Provides (somewhat) generic functionality to simulate a
** (potentially cooperative) race
**/
#include <boost/function.hpp>
#include <boost/thread.hpp>
#include <boost/bind.hpp>
#include <boost/thread/condition.hpp>
#include <boost/exception_ptr.hpp>
#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 */
boost::mutex mutex_done;
/** Mutex / condition variable to notify main when winner data written */
boost::mutex mutex_main_wait;
boost::condition_variable condition_var_main_wait;
bool global_flag_done;
int global_winner;
template<typename S>
void runThread(int thread_id, boost::function<S()> threadFn, S& returnValue)
{
/* Uncomment line to delay first thread, useful to unearth errors/debug */
// if(thread_id == 0) { sleep(1); }
returnValue = threadFn();
if( mutex_done.try_lock() ) {
if(global_flag_done == false)
{
{
boost::lock_guard<boost::mutex> lock(mutex_main_wait);
global_winner = thread_id;
global_flag_done = true;
}
condition_var_main_wait.notify_all(); // we want main thread to quit
}
mutex_done.unlock();
}
}
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) {
boost::thread thread_driver;
boost::thread* threads = new boost::thread[numThreads];
S* threads_returnValue = new S[numThreads];
global_flag_done = false;
global_winner = -1;
for(int t = 0; t < numThreads; ++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())
thread_driver = boost::thread(driverFn);
boost::unique_lock<boost::mutex> lock(mutex_main_wait);
while(global_flag_done == false) {
condition_var_main_wait.wait(lock);
}
statWaitTime.start();
if(not driverFn.empty()) {
thread_driver.interrupt();
thread_driver.join();
}
for(int t = 0; t < numThreads; ++t) {
if(optionWaitToJoin) {
threads[t].join();
}
}
std::pair<int, S> retval(global_winner, threads_returnValue[global_winner]);
delete[] threads;
delete[] threads_returnValue;
return retval;
}
// instantiation
template
std::pair<int, bool>
runPortfolio<void, bool>(int,
boost::function<void()>,
boost::function<bool()>*,
size_t,
bool,
TimerStat&);
}/* CVC4 namespace */
|
