Commit 75a0a853 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 310def3e
......@@ -436,9 +436,10 @@ namespace spot
shared_map& map, /* useless here */
iterable_uf<State, StateHash, StateEqual>* uf,
unsigned tid,
std::atomic<bool>& /*useless here*/):
std::atomic<bool>& stop):
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),
State, SuccIterator>::value,
......@@ -457,7 +458,7 @@ namespace spot
while (!todo_.empty())
{
bloemen_recursive_start:
while (true)
while (!stop_.load(std::memory_order_relaxed))
{
bool sccfound = false;
uf_element* v_prime = uf_.pick_from_list(todo_.back(), &sccfound);
......@@ -510,9 +511,19 @@ namespace spot
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_));
}
bool finisher()
{
return finisher_;
}
unsigned states()
{
return states_;
......@@ -561,5 +572,7 @@ namespace spot
unsigned transitions_ = 0; ///< \brief Number of transitions visited
unsigned sccs_ = 0; ///< \brief Number of SCC visited
spot::timer_map tm_; ///< \brief Time execution
std::atomic<bool>& stop_;
bool finisher_ = false;
};
}
......@@ -579,9 +579,19 @@ namespace spot
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_));
}
bool finisher()
{
return finisher_;
}
unsigned states()
{
return states_;
......@@ -632,5 +642,6 @@ namespace spot
bool is_empty_ = true;
spot::timer_map tm_; ///< \brief Time execution
std::atomic<bool>& stop_;
bool finisher_ = false;
};
}
......@@ -236,9 +236,19 @@ namespace spot
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_));
}
bool finisher()
{
return finisher_;
}
unsigned states()
{
return states_;
......@@ -508,5 +518,6 @@ namespace spot
std::vector<product_state> Rp_; ///< \brief Rp stack
std::vector<product_state> Rp_acc_; ///< \brief Rp acc stack
product_state cycle_start_; ///< \brief Begining of a cycle
bool finisher_ = false;
};
}
......@@ -222,10 +222,19 @@ namespace spot
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_));
}
bool finisher()
{
return finisher_;
}
unsigned states()
{
return states_;
......@@ -292,5 +301,6 @@ namespace spot
/// \brief Stack that grows according to the todo stack. It avoid multiple
/// concurent access to the shared map.
std::vector<int*> refs_;
bool finisher_ = false;
};
}
......@@ -230,9 +230,19 @@ namespace spot
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_));
}
bool finisher()
{
return finisher_;
}
unsigned int states()
{
return dfs_number;
......@@ -415,5 +425,6 @@ namespace spot
unsigned sccs_;
unsigned dfs_;
spot::timer_map tm_;
bool finisher_ = false;
};
}
......@@ -60,6 +60,7 @@ namespace spot
std::vector<unsigned> transitions; ///< \brief Number of transitions visited
std::vector<int> sccs; ///< \brief Number of SCCs or -1
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
};
......@@ -112,12 +113,15 @@ namespace spot
<< " - Walltime (ms):\t" << es.walltime[i] <<'\n'
<< " - States:\t\t" << es.states[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] << ','
<< es.states[i] << ',' << es.transitions[i] << ','
<< es.value[i] << "\n\n";
<< es.sccs[i] << ',' << es.value[i]
<< ',' << es.finisher[i] << "\n\n";
}
return os;
}
......
......@@ -117,6 +117,7 @@ namespace spot
result.transitions.emplace_back(swarmed[i]->transitions());
result.sccs.emplace_back(swarmed[i]->sccs());
result.value.emplace_back(swarmed[i]->result());
result.finisher.emplace_back(swarmed[i]->finisher());
}
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