Commit 31efc7ab authored by Etienne Renault's avatar Etienne Renault

mc: keep information about the finisher

* spot/mc/bloemen.hh,
spot/mc/bloemen_ec.hh,
spot/mc/cndfs.hh,
spot/mc/deadlock.hh,
spot/mc/lpar13.hh,
spot/mc/mc.hh,
spot/mc/mc_instanciator.hh: Here.
parent 40b312a7
...@@ -436,9 +436,10 @@ namespace spot ...@@ -436,9 +436,10 @@ namespace spot
shared_map& map, /* useless here */ shared_map& map, /* useless here */
iterable_uf<State, StateHash, StateEqual>* uf, iterable_uf<State, StateHash, StateEqual>* uf,
unsigned tid, unsigned tid,
std::atomic<bool>& /*useless here*/): std::atomic<bool>& stop):
sys_(sys), uf_(*uf), tid_(tid), sys_(sys), uf_(*uf), tid_(tid),
nb_th_(std::thread::hardware_concurrency()) nb_th_(std::thread::hardware_concurrency()),
stop_(stop)
{ {
static_assert(spot::is_a_kripkecube_ptr<decltype(&sys), static_assert(spot::is_a_kripkecube_ptr<decltype(&sys),
State, SuccIterator>::value, State, SuccIterator>::value,
...@@ -457,7 +458,7 @@ namespace spot ...@@ -457,7 +458,7 @@ namespace spot
while (!todo_.empty()) while (!todo_.empty())
{ {
bloemen_recursive_start: bloemen_recursive_start:
while (true) while (!stop_.load(std::memory_order_relaxed))
{ {
bool sccfound = false; bool sccfound = false;
uf_element* v_prime = uf_.pick_from_list(todo_.back(), &sccfound); uf_element* v_prime = uf_.pick_from_list(todo_.back(), &sccfound);
...@@ -510,9 +511,19 @@ namespace spot ...@@ -510,9 +511,19 @@ namespace spot
void finalize() void finalize()
{ {
bool tst_val = false;
bool new_val = true;
bool exchanged = stop_.compare_exchange_strong(tst_val, new_val);
if (exchanged)
finisher_ = true;
tm_.stop("DFS thread " + std::to_string(tid_)); tm_.stop("DFS thread " + std::to_string(tid_));
} }
bool finisher()
{
return finisher_;
}
unsigned states() unsigned states()
{ {
return states_; return states_;
...@@ -561,5 +572,7 @@ namespace spot ...@@ -561,5 +572,7 @@ namespace spot
unsigned transitions_ = 0; ///< \brief Number of transitions visited unsigned transitions_ = 0; ///< \brief Number of transitions visited
unsigned sccs_ = 0; ///< \brief Number of SCC visited unsigned sccs_ = 0; ///< \brief Number of SCC visited
spot::timer_map tm_; ///< \brief Time execution spot::timer_map tm_; ///< \brief Time execution
std::atomic<bool>& stop_;
bool finisher_ = false;
}; };
} }
...@@ -579,9 +579,19 @@ namespace spot ...@@ -579,9 +579,19 @@ namespace spot
void finalize() void finalize()
{ {
bool tst_val = false;
bool new_val = true;
bool exchanged = stop_.compare_exchange_strong(tst_val, new_val);
if (exchanged)
finisher_ = true;
tm_.stop("DFS thread " + std::to_string(tid_)); tm_.stop("DFS thread " + std::to_string(tid_));
} }
bool finisher()
{
return finisher_;
}
unsigned states() unsigned states()
{ {
return states_; return states_;
...@@ -632,5 +642,6 @@ namespace spot ...@@ -632,5 +642,6 @@ namespace spot
bool is_empty_ = true; bool is_empty_ = true;
spot::timer_map tm_; ///< \brief Time execution spot::timer_map tm_; ///< \brief Time execution
std::atomic<bool>& stop_; std::atomic<bool>& stop_;
bool finisher_ = false;
}; };
} }
...@@ -236,9 +236,19 @@ namespace spot ...@@ -236,9 +236,19 @@ namespace spot
void finalize() void finalize()
{ {
bool tst_val = false;
bool new_val = true;
bool exchanged = stop_.compare_exchange_strong(tst_val, new_val);
if (exchanged)
finisher_ = true;
tm_.stop("DFS thread " + std::to_string(tid_)); tm_.stop("DFS thread " + std::to_string(tid_));
} }
bool finisher()
{
return finisher_;
}
unsigned states() unsigned states()
{ {
return states_; return states_;
...@@ -508,5 +518,6 @@ namespace spot ...@@ -508,5 +518,6 @@ namespace spot
std::vector<product_state> Rp_; ///< \brief Rp stack std::vector<product_state> Rp_; ///< \brief Rp stack
std::vector<product_state> Rp_acc_; ///< \brief Rp acc stack std::vector<product_state> Rp_acc_; ///< \brief Rp acc stack
product_state cycle_start_; ///< \brief Begining of a cycle product_state cycle_start_; ///< \brief Begining of a cycle
bool finisher_ = false;
}; };
} }
...@@ -222,10 +222,19 @@ namespace spot ...@@ -222,10 +222,19 @@ namespace spot
void finalize() void finalize()
{ {
stop_ = true; bool tst_val = false;
bool new_val = true;
bool exchanged = stop_.compare_exchange_strong(tst_val, new_val);
if (exchanged)
finisher_ = true;
tm_.stop("DFS thread " + std::to_string(tid_)); tm_.stop("DFS thread " + std::to_string(tid_));
} }
bool finisher()
{
return finisher_;
}
unsigned states() unsigned states()
{ {
return states_; return states_;
...@@ -292,5 +301,6 @@ namespace spot ...@@ -292,5 +301,6 @@ namespace spot
/// \brief Stack that grows according to the todo stack. It avoid multiple /// \brief Stack that grows according to the todo stack. It avoid multiple
/// concurent access to the shared map. /// concurent access to the shared map.
std::vector<int*> refs_; std::vector<int*> refs_;
bool finisher_ = false;
}; };
} }
...@@ -230,9 +230,19 @@ namespace spot ...@@ -230,9 +230,19 @@ namespace spot
void finalize() void finalize()
{ {
bool tst_val = false;
bool new_val = true;
bool exchanged = stop_.compare_exchange_strong(tst_val, new_val);
if (exchanged)
finisher_ = true;
tm_.stop("DFS thread " + std::to_string(tid_)); tm_.stop("DFS thread " + std::to_string(tid_));
} }
bool finisher()
{
return finisher_;
}
unsigned int states() unsigned int states()
{ {
return dfs_number; return dfs_number;
...@@ -415,5 +425,6 @@ namespace spot ...@@ -415,5 +425,6 @@ namespace spot
unsigned sccs_; unsigned sccs_;
unsigned dfs_; unsigned dfs_;
spot::timer_map tm_; spot::timer_map tm_;
bool finisher_ = false;
}; };
} }
...@@ -60,6 +60,7 @@ namespace spot ...@@ -60,6 +60,7 @@ namespace spot
std::vector<unsigned> transitions; ///< \brief Number of transitions visited std::vector<unsigned> transitions; ///< \brief Number of transitions visited
std::vector<int> sccs; ///< \brief Number of SCCs or -1 std::vector<int> sccs; ///< \brief Number of SCCs or -1
std::vector<mc_rvalue> value; ///< \brief The return status std::vector<mc_rvalue> value; ///< \brief The return status
std::vector<bool> finisher; ///< \brief Is it the finisher thread?
std::string trace; ///< \brief The output trace std::string trace; ///< \brief The output trace
}; };
...@@ -112,12 +113,15 @@ namespace spot ...@@ -112,12 +113,15 @@ namespace spot
<< " - Walltime (ms):\t" << es.walltime[i] <<'\n' << " - Walltime (ms):\t" << es.walltime[i] <<'\n'
<< " - States:\t\t" << es.states[i] << '\n' << " - States:\t\t" << es.states[i] << '\n'
<< " - Transitions:\t" << es.transitions[i] << '\n' << " - Transitions:\t" << es.transitions[i] << '\n'
<< " - Result:\t\t" << es.value[i] << '\n'; << " - Result:\t\t" << es.value[i] << '\n'
<< " - SCCs:\t\t" << es.sccs[i] << '\n';
os << "CSV: tid,algorithm,walltime,states,transitions,result\n" os << "CSV: tid,algorithm,walltime,states,transitions,"
"sccs,result,finisher\n"
<< "@th_" << i << ',' << es.name[i] << ',' << es.walltime[i] << ',' << "@th_" << i << ',' << es.name[i] << ',' << es.walltime[i] << ','
<< es.states[i] << ',' << es.transitions[i] << ',' << es.states[i] << ',' << es.transitions[i] << ','
<< es.value[i] << "\n\n"; << es.sccs[i] << ',' << es.value[i]
<< ',' << es.finisher[i] << "\n\n";
} }
return os; return os;
} }
......
...@@ -117,6 +117,7 @@ namespace spot ...@@ -117,6 +117,7 @@ namespace spot
result.transitions.emplace_back(swarmed[i]->transitions()); result.transitions.emplace_back(swarmed[i]->transitions());
result.sccs.emplace_back(swarmed[i]->sccs()); result.sccs.emplace_back(swarmed[i]->sccs());
result.value.emplace_back(swarmed[i]->result()); result.value.emplace_back(swarmed[i]->result());
result.finisher.emplace_back(swarmed[i]->finisher());
} }
if (trace) if (trace)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment