mc: add swarmed deadlock-detection

* spot/mc/Makefile.am, spot/mc/deadlock.hh,
spot/mc/mc.hh, tests/ltsmin/modelcheck.cc: here.

spot/mc/Makefile.am

@@ -21,7 +21,8 @@ AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS)
 AM_CXXFLAGS = $(WARNING_CXXFLAGS)
 
 mcdir = $(pkgincludedir)/mc
-mc_HEADERS = reachability.hh intersect.hh ec.hh unionfind.hh utils.hh mc.hh
+mc_HEADERS = reachability.hh intersect.hh ec.hh unionfind.hh utils.hh\
+	mc.hh deadlock.hh
 
 noinst_LTLIBRARIES = libmc.la
 

spot/mc/deadlock.hh

+// -*- coding: utf-8 -*-
+// Copyright (C) 2015, 2016, 2017 Laboratoire de Recherche et
+// Developpement de l'Epita
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 3 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+#pragma once
+
+#include <atomic>
+#include <chrono>
+#include <bricks/brick-hashset>
+#include <stdlib.h>
+#include <thread>
+#include <vector>
+#include <spot/misc/common.hh>
+#include <spot/kripke/kripke.hh>
+#include <spot/misc/fixpool.hh>
+#include <spot/misc/timer.hh>
+
+namespace spot
+{
+  /// \brief This object is returned by the algorithm below
+  struct SPOT_API deadlock_stats
+  {
+    unsigned states;            ///< \brief Number of states visited
+    unsigned transitions;       ///< \brief Number of transitions visited
+    unsigned instack_dfs;       ///< \brief Maximum DFS stack
+    bool has_deadlock;          ///< \brief Does the model contains a deadlock
+    unsigned walltime;          ///< \brief Walltime for this thread in ms
+  };
+
+  /// \brief This class aims to explore a model to detect wether it
+  /// contains a deadlock. This deadlock detection performs a DFS traversal
+  /// sharing information shared among multiple threads.
+  template<typename State, typename SuccIterator,
+           typename StateHash, typename StateEqual>
+  class swarmed_deadlock
+  {
+    /// \brief Describes the status of a state
+    enum st_status
+      {
+        UNKNOWN = 1,    // First time this state is discoverd by this thread
+        OPEN = 2,       // The state is currently processed by this thread
+        CLOSED = 4,     // All the successors of this state have been visited
+      };
+
+    /// \brief Describes the structure of a shared state
+    struct deadlock_pair
+    {
+      State st;                 ///< \brief the effective state
+      int* colors;              ///< \brief the colors (one per thread)
+    };
+
+    /// \brief The haser for the previous state.
+    struct pair_hasher
+    {
+      pair_hasher(const deadlock_pair&)
+      { }
+
+      pair_hasher() = default;
+
+      brick::hash::hash128_t
+      hash(const deadlock_pair& lhs) const
+      {
+        StateHash hash;
+        // Not modulo 31 according to brick::hashset specifications.
+        unsigned u = hash(lhs.st) % (1<<30);
+        return {u, u};
+      }
+
+      bool equal(const deadlock_pair& lhs,
+                 const deadlock_pair& rhs) const
+      {
+        StateEqual equal;
+        return equal(lhs.st, rhs.st);
+      }
+    };
+
+  public:
+
+    ///< \brief Shortcut to ease shared map manipulation
+    using shared_map = brick::hashset::FastConcurrent <deadlock_pair,
+                                                       pair_hasher>;
+
+    swarmed_deadlock(kripkecube<State, SuccIterator>& sys,
+                     shared_map& map, unsigned tid, std::atomic<bool>& stop):
+      sys_(sys), tid_(tid), map_(map),
+      nb_th_(std::thread::hardware_concurrency()),
+      p_(sizeof(int)*std::thread::hardware_concurrency()), stop_(stop)
+    {
+      SPOT_ASSERT(is_a_kripkecube(sys));
+    }
+
+    virtual ~swarmed_deadlock()
+    {
+    }
+
+    void setup()
+    {
+      tm_.start("DFS thread " + std::to_string(tid_));
+    }
+
+    bool push(State s)
+    {
+      // Prepare data for a newer allocation
+      int* ref = (int*) p_.allocate();
+      for (unsigned i = 0; i < nb_th_; ++i)
+        ref[i] = UNKNOWN;
+
+      // Try to insert the new state in the shared map.
+      auto it = map_.insert({s, ref});
+      bool b = it.isnew();
+
+      // Insertion failed, delete element
+      // FIXME Should we add a local cache to avoid useless allocations?
+      if (!b)
+        p_.deallocate(ref);
+
+      // The state has been mark dead by another thread
+      for (unsigned i = 0; !b && i < nb_th_; ++i)
+        if (it->colors[i] == static_cast<int>(CLOSED))
+          return false;
+
+      // The state has already been visited by the current thread
+      if (it->colors[tid_] == static_cast<int>(OPEN))
+        return false;
+
+      // Keep a ptr over the array of colors
+      refs_.push_back(it->colors);
+
+      // Mark state as visited.
+      it->colors[tid_] = OPEN;
+      ++states_;
+      return true;
+    }
+
+    bool pop()
+    {
+      // Track maximum dfs size
+      dfs_ = todo_.size()  > dfs_ ? todo_.size() : dfs_;
+
+      // Don't avoid pop but modify the status of the state
+      // during backtrack
+      refs_.back()[tid_] = CLOSED;
+      refs_.pop_back();
+      return true;
+    }
+
+    void finalize()
+    {
+      stop_ = true;
+      tm_.stop("DFS thread " + std::to_string(tid_));
+    }
+
+    unsigned states()
+    {
+      return states_;
+    }
+
+    unsigned transitions()
+    {
+      return transitions_;
+    }
+
+    void run()
+    {
+      setup();
+      State initial = sys_.initial(tid_);
+      if (SPOT_LIKELY(push(initial)))
+        {
+          todo_.push_back({initial, sys_.succ(initial, tid_), transitions_});
+        }
+      while (!todo_.empty() && !stop_.load(std::memory_order_relaxed))
+        {
+          if (todo_.back().it->done())
+            {
+              if (SPOT_LIKELY(pop()))
+                {
+                  deadlock_ = todo_.back().current_tr == transitions_;
+                  if (deadlock_)
+                    break;
+                  sys_.recycle(todo_.back().it, tid_);
+                  todo_.pop_back();
+                }
+            }
+          else
+            {
+              ++transitions_;
+              State dst = todo_.back().it->state();
+
+              if (SPOT_LIKELY(push(dst)))
+                {
+                  todo_.back().it->next();
+                  todo_.push_back({dst, sys_.succ(dst, tid_), transitions_});
+                }
+              else
+                {
+                  todo_.back().it->next();
+                }
+            }
+        }
+      finalize();
+    }
+
+    bool has_deadlock()
+    {
+      return deadlock_;
+    }
+
+    unsigned walltime()
+    {
+      return tm_.timer("DFS thread " + std::to_string(tid_)).walltime();
+    }
+
+    deadlock_stats stats()
+    {
+      return {states(), transitions(), dfs_, has_deadlock(), walltime()};
+    }
+
+  private:
+    struct todo__element
+    {
+      State s;
+      SuccIterator* it;
+      unsigned current_tr;
+    };
+    kripkecube<State, SuccIterator>& sys_; ///< \brief The system to check
+    std::vector<todo__element> todo_;      ///< \brief The DFS stack
+    unsigned transitions_ = 0;         ///< \brief Number of transitions
+    unsigned tid_;                     ///< \brief Thread's current ID
+    shared_map map_;                       ///< \brief Map shared by threads
+    spot::timer_map tm_;                   ///< \brief Time execution
+    unsigned states_ = 0;                  ///< \brief Number of states
+    unsigned dfs_ = 0;                     ///< \brief Maximum DFS stack size
+    /// \brief Maximum number of threads that can be handled by this algorithm
+    unsigned nb_th_ = 0;
+    fixed_size_pool p_;                    ///< \brief State Allocator
+    bool deadlock_ = false;                ///< \brief Deadlock detected?
+    std::atomic<bool>& stop_;              ///< \brief Stop-the-world boolean
+    /// \brief Stack that grows according to the todo stack. It avoid multiple
+    /// concurent access to the shared map.
+    std::vector<int*> refs_;
+  };
+}

spot/mc/mc.hh

@@ -19,13 +19,16 @@
 
 #pragma once
 
+#include <functional>
 #include <string>
 #include <thread>
 #include <tuple>
 #include <vector>
 #include <spot/kripke/kripke.hh>
 #include <spot/mc/ec.hh>
+#include <spot/mc/deadlock.hh>
 #include <spot/misc/common.hh>
+#include <spot/misc/timer.hh>
 
 namespace spot
 {
@@ -60,7 +63,7 @@ namespace spot
 
     bool has_ctrx = false;
     std::string trace = "";
-     std::vector<istats> stats;
+    std::vector<istats> stats;
     for (unsigned i = 0; i < sys->get_threads(); ++i)
       {
         has_ctrx |= ecs[i].counterexample_found();
@@ -71,4 +74,82 @@ namespace spot
       }
     return std::make_tuple(has_ctrx, trace, stats);
   }
+
+  /// \bief Check wether the system contains a deadlock. The algorithm
+  /// spawns multiple threads performing a classical swarming DFS. As
+  /// soon one thread detects a deadlock all the other threads are stopped.
+  template<typename kripke_ptr, typename State,
+           typename Iterator, typename Hash, typename Equal>
+  static std::tuple<bool, std::vector<deadlock_stats>, spot::timer_map>
+  has_deadlock(kripke_ptr sys)
+  {
+    spot::timer_map tm;
+    using algo_name = spot::swarmed_deadlock<State, Iterator, Hash, Equal>;
+
+    unsigned  nbth = sys->get_threads();
+    typename algo_name::shared_map map;
+    std::atomic<bool> stop(false);
+
+    tm.start("Initialisation");
+    std::vector<algo_name*> swarmed(nbth);
+    for (unsigned i = 0; i < nbth; ++i)
+      swarmed[i] = new algo_name(*sys, map, i, stop);
+    tm.stop("Initialisation");
+
+    std::mutex iomutex;
+    std::atomic<bool> barrier(true);
+    std::vector<std::thread> threads(nbth);
+    for (unsigned i = 0; i < nbth; ++i)
+      {
+        threads[i] = std::thread ([&swarmed, &iomutex, i, & barrier]
+        {
+#if defined(unix) || defined(__unix__) || defined(__unix)
+            {
+              std::lock_guard<std::mutex> iolock(iomutex);
+              std::cout << "Thread #" << i
+                        << ": on CPU " << sched_getcpu() << '\n';
+            }
+#endif
+
+            // Wait all threads to be instanciated.
+            while (barrier)
+              continue;
+            swarmed[i]->run();
+         });
+
+#if defined(unix) || defined(__unix__) || defined(__unix)
+        //  Pins threads to a dedicated core.
+        cpu_set_t cpuset;
+        CPU_ZERO(&cpuset);
+        CPU_SET(i, &cpuset);
+        int rc = pthread_setaffinity_np(threads[i].native_handle(),
+                                        sizeof(cpu_set_t), &cpuset);
+        if (rc != 0)
+          {
+            std::lock_guard<std::mutex> iolock(iomutex);
+            std::cerr << "Error calling pthread_setaffinity_np: " << rc << '\n';
+          }
+#endif
+      }
+
+    tm.start("Run");
+    barrier.store(false);
+
+    for (auto& t : threads)
+      t.join();
+    tm.stop("Run");
+
+    std::vector<deadlock_stats> stats;
+    bool has_deadlock = false;
+    for (unsigned i = 0; i < sys->get_threads(); ++i)
+      {
+        has_deadlock |= swarmed[i]->has_deadlock();
+        stats.push_back(swarmed[i]->stats());
+      }
+
+    for (unsigned i = 0; i < nbth; ++i)
+      delete swarmed[i];
+
+    return std::make_tuple(has_deadlock, stats, tm);
+  }
 }

tests/ltsmin/modelcheck.cc

@@ -72,6 +72,7 @@ struct mc_options_
   bool kripke_output = false;
   unsigned nb_threads = 1;
   bool csv = false;
+  bool has_deadlock = false;
 } mc_options;
 
 
@@ -107,6 +108,10 @@ parse_opt_finput(int key, char* arg, struct argp_state*)
     case 'f':
       mc_options.formula = arg;
       break;
+    case 'h':
+      mc_options.has_deadlock = true;
+      mc_options.selfloopize = false;
+      break;
     case 'k':
       mc_options.kripke_output = true;
       break;
@@ -147,6 +152,10 @@ static const argp_option options[] =
       "check if the model meets its specification. "
       "Return 1 if a counterexample is found."
       , 0 },
+    { "has-deadlock", 'h', nullptr, 0,
+      "check if the model has a deadlock. "
+      "Return 1 if the model contains a deadlock."
+      , 0 },
     { "parallel", 'p', "INT", 0, "use INT threads (when possible)", 0 },
     { "selfloopize", 's', "STRING", 0,
       "use STRING as property for marking deadlock "
@@ -280,7 +289,6 @@ static int checked_main()
         }
     }
 
-
   if (mc_options.nb_threads == 1 &&
       mc_options.formula != nullptr &&
       mc_options.model != nullptr)
@@ -503,6 +511,104 @@ static int checked_main()
         }
     }
 
+
+    if (mc_options.has_deadlock &&  mc_options.model != nullptr)
+    {
+      assert(!mc_options.selfloopize);
+      unsigned int hc = std::thread::hardware_concurrency();
+      if (mc_options.nb_threads > hc)
+        std::cerr << "Warning: you require " << mc_options.nb_threads
+                  << " threads, but your computer only support " << hc
+                  << ". This could slow down parallel algorithms.\n";
+
+      tm.start("load kripkecube");
+      spot::ltsmin_kripkecube_ptr modelcube = nullptr;
+      try
+        {
+           modelcube = spot::ltsmin_model::load(mc_options.model)
+             .kripkecube({}, deadf, mc_options.compress,
+                         mc_options.nb_threads);
+        }
+      catch (std::runtime_error& e)
+        {
+          std::cerr << e.what() << '\n';
+        }
+      tm.stop("load kripkecube");
+
+      int memused = spot::memusage();
+      tm.start("deadlock check");
+      auto res = spot::has_deadlock<spot::ltsmin_kripkecube_ptr,
+                                    spot::cspins_state,
+                                    spot::cspins_iterator,
+                                    spot::cspins_state_hash,
+                                    spot::cspins_state_equal>(modelcube);
+      tm.stop("deadlock check");
+      memused = spot::memusage() - memused;
+
+      if (!modelcube)
+        {
+          exit_code = 2;
+          goto safe_exit;
+        }
+
+      // Display statistics
+      unsigned smallest = 0;
+      for (unsigned i = 0; i < std::get<1>(res).size(); ++i)
+        {
+          if (std::get<1>(res)[i].states < std::get<1>(res)[smallest].states)
+            smallest = i;
+
+          std::cout << "\n---- Thread number : " << i << '\n';
+          std::cout << std::get<1>(res)[i].states << " unique states visited\n";
+          std::cout << std::get<1>(res)[i].transitions
+                    << " transitions explored\n";
+          std::cout << std::get<1>(res)[i].instack_dfs
+                    << " items max in DFS search stack\n";
+          std::cout << std::get<1>(res)[i].walltime
+                    << " milliseconds\n";
+
+          if (mc_options.csv)
+            {
+              std::cout << "Find following the csv: "
+                        << "thread_id,walltimems,type,"
+                        << "states,transitions\n";
+              std::cout << "@th_" << i << ','
+                        << std::get<1>(res)[i].walltime << ','
+                        << (std::get<1>(res)[i].has_deadlock ?
+                            "DEADLOCK," : "NO-DEADLOCK,")
+                        << std::get<1>(res)[i].states << ','
+                        << std::get<1>(res)[i].transitions
+                        << std::endl;
+            }
+        }
+
+      if (mc_options.csv)
+        {
+          std::cout << "\nSummary :\n";
+          if (!std::get<0>(res))
+            std::cout << "No no deadlock found!\n";
+          else
+            {
+              std::cout << "A deadlock exists!\n";
+              exit_code = 1;
+            }
+
+          std::cout << "Find following the csv: "
+                    << "model,walltimems,memused,type,"
+                    << "states,transitions\n";
+
+          std::cout << '#'
+                    << split_filename(mc_options.model)
+                    << ','
+                    << tm.timer("deadlock check").walltime() << ','
+                    << memused << ','
+                    << (std::get<0>(res) ? "DEADLOCK," : "NO-DEADLOCK,")
+                    << std::get<1>(res)[smallest].states << ','
+                    << std::get<1>(res)[smallest].transitions
+                    << '\n';
+        }
+    }
+
  safe_exit:
   if (mc_options.use_timer)
     tm.print(std::cout);