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.

spot/mc/bloemen.hh

@@ -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;
   };
 }

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<bool>& stop_;
+    bool finisher_ = false;
   };
 }

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<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;
   };
 }

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<int*> refs_;
+    bool finisher_ = false;
   };
 }

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;
   };
 }

spot/mc/mc.hh

@@ -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;
   }

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)