diff --git a/spot/mc/bloemen.hh b/spot/mc/bloemen.hh index 5d3c8739f..1a37a71be 100644 --- a/spot/mc/bloemen.hh +++ b/spot/mc/bloemen.hh @@ -436,9 +436,10 @@ namespace spot shared_map& map, /* useless here */ iterable_uf* uf, unsigned tid, - std::atomic& /*useless here*/): + std::atomic& 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::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& stop_; + bool finisher_ = false; }; } diff --git a/spot/mc/bloemen_ec.hh b/spot/mc/bloemen_ec.hh index d9f644d8c..831c20b64 100644 --- a/spot/mc/bloemen_ec.hh +++ b/spot/mc/bloemen_ec.hh @@ -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& stop_; + bool finisher_ = false; }; } diff --git a/spot/mc/cndfs.hh b/spot/mc/cndfs.hh index 2e2708038..9b414764f 100644 --- a/spot/mc/cndfs.hh +++ b/spot/mc/cndfs.hh @@ -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 Rp_; ///< \brief Rp stack std::vector Rp_acc_; ///< \brief Rp acc stack product_state cycle_start_; ///< \brief Begining of a cycle + bool finisher_ = false; }; } diff --git a/spot/mc/deadlock.hh b/spot/mc/deadlock.hh index 949dfd623..90c6c0556 100644 --- a/spot/mc/deadlock.hh +++ b/spot/mc/deadlock.hh @@ -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 refs_; + bool finisher_ = false; }; } diff --git a/spot/mc/lpar13.hh b/spot/mc/lpar13.hh index aa2cc7d72..029fa3095 100644 --- a/spot/mc/lpar13.hh +++ b/spot/mc/lpar13.hh @@ -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; }; } diff --git a/spot/mc/mc.hh b/spot/mc/mc.hh index 64b449143..aaf196bcd 100644 --- a/spot/mc/mc.hh +++ b/spot/mc/mc.hh @@ -60,6 +60,7 @@ namespace spot std::vector transitions; ///< \brief Number of transitions visited std::vector sccs; ///< \brief Number of SCCs or -1 std::vector value; ///< \brief The return status + std::vector 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; } diff --git a/spot/mc/mc_instanciator.hh b/spot/mc/mc_instanciator.hh index 4333a87cc..7f7e5123b 100644 --- a/spot/mc/mc_instanciator.hh +++ b/spot/mc/mc_instanciator.hh @@ -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)