spot  2.12
deadlock.hh
1 // -*- coding: utf-8 -*-
2 // Copyright (C) by the Spot authors, see the AUTHORS file for details.
3 //
4 // This file is part of Spot, a model checking library.
5 //
6 // Spot is free software; you can redistribute it and/or modify it
7 // under the terms of the GNU General Public License as published by
8 // the Free Software Foundation; either version 3 of the License, or
9 // (at your option) any later version.
10 //
11 // Spot is distributed in the hope that it will be useful, but WITHOUT
12 // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
13 // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
14 // License for more details.
15 //
16 // You should have received a copy of the GNU General Public License
17 // along with this program. If not, see <http://www.gnu.org/licenses/>.
18 
19 #pragma once
20 
21 #include <atomic>
22 #include <chrono>
23 #include <spot/bricks/brick-hashset>
24 #include <stdlib.h>
25 #include <thread>
26 #include <vector>
27 #include <spot/misc/common.hh>
28 #include <spot/kripke/kripke.hh>
29 #include <spot/misc/fixpool.hh>
30 #include <spot/misc/timer.hh>
31 #include <spot/twacube/twacube.hh>
32 #include <spot/twacube/fwd.hh>
33 #include <spot/mc/mc.hh>
34 
35 namespace spot
36 {
42  template<typename State, typename SuccIterator,
43  typename StateHash, typename StateEqual,
44  typename Deadlock>
45  class SPOT_API swarmed_deadlock
46  {
48  enum st_status
49  {
50  UNKNOWN = 1, // First time this state is discoverd by this thread
51  OPEN = 2, // The state is currently processed by this thread
52  CLOSED = 4, // All the successors of this state have been visited
53  };
54 
56  struct deadlock_pair
57  {
58  State st;
59  int* colors;
60  };
61 
63  struct pair_hasher
64  {
65  pair_hasher(const deadlock_pair*)
66  { }
67 
68  pair_hasher() = default;
69 
70  brick::hash::hash128_t
71  hash(const deadlock_pair* lhs) const
72  {
73  StateHash hash;
74  // Not modulo 31 according to brick::hashset specifications.
75  unsigned u = hash(lhs->st) % (1<<30);
76  return {u, u};
77  }
78 
79  bool equal(const deadlock_pair* lhs,
80  const deadlock_pair* rhs) const
81  {
82  StateEqual equal;
83  return equal(lhs->st, rhs->st);
84  }
85  };
86 
87  static constexpr bool compute_deadlock =
88  std::is_same<std::true_type, Deadlock>::value;
89 
90  public:
91 
93  using shared_map = brick::hashset::FastConcurrent <deadlock_pair*,
94  pair_hasher>;
95  using shared_struct = shared_map;
96 
97  static shared_struct* make_shared_structure(shared_map, unsigned)
98  {
99  return nullptr; // Useless
100  }
101 
103  twacube_ptr, /* useless here */
104  shared_map& map, shared_struct* /* useless here */,
105  unsigned tid,
106  std::atomic<bool>& stop):
107  sys_(sys), tid_(tid), map_(map),
108  nb_th_(std::thread::hardware_concurrency()),
109  p_(sizeof(int)*std::thread::hardware_concurrency()),
110  p_pair_(sizeof(deadlock_pair)),
111  stop_(stop)
112  {
113  static_assert(spot::is_a_kripkecube_ptr<decltype(&sys),
114  State, SuccIterator>::value,
115  "error: does not match the kripkecube requirements");
116  SPOT_ASSERT(nb_th_ > tid);
117  }
118 
119  virtual ~swarmed_deadlock()
120  {
121  while (!todo_.empty())
122  {
123  sys_.recycle(todo_.back().it, tid_);
124  todo_.pop_back();
125  }
126  }
127 
128  void run()
129  {
130  setup();
131  State initial = sys_.initial(tid_);
132  if (SPOT_LIKELY(push(initial)))
133  {
134  todo_.push_back({initial, sys_.succ(initial, tid_), transitions_});
135  }
136  while (!todo_.empty() && !stop_.load(std::memory_order_relaxed))
137  {
138  if (todo_.back().it->done())
139  {
140  if (SPOT_LIKELY(pop()))
141  {
142  deadlock_ = todo_.back().current_tr == transitions_;
143  if (compute_deadlock && deadlock_)
144  break;
145  sys_.recycle(todo_.back().it, tid_);
146  todo_.pop_back();
147  }
148  }
149  else
150  {
151  ++transitions_;
152  State dst = todo_.back().it->state();
153 
154  if (SPOT_LIKELY(push(dst)))
155  {
156  todo_.back().it->next();
157  todo_.push_back({dst, sys_.succ(dst, tid_), transitions_});
158  }
159  else
160  {
161  todo_.back().it->next();
162  }
163  }
164  }
165  finalize();
166  }
167 
168  void setup()
169  {
170  tm_.start("DFS thread " + std::to_string(tid_));
171  }
172 
173  bool push(State s)
174  {
175  // Prepare data for a newer allocation
176  int* ref = (int*) p_.allocate();
177  for (unsigned i = 0; i < nb_th_; ++i)
178  ref[i] = UNKNOWN;
179 
180  // Try to insert the new state in the shared map.
181  deadlock_pair* v = (deadlock_pair*) p_pair_.allocate();
182  v->st = s;
183  v->colors = ref;
184  auto it = map_.insert(v);
185  bool b = it.isnew();
186 
187  // Insertion failed, delete element
188  // FIXME Should we add a local cache to avoid useless allocations?
189  if (!b)
190  p_.deallocate(ref);
191 
192  // The state has been mark dead by another thread
193  for (unsigned i = 0; !b && i < nb_th_; ++i)
194  if ((*it)->colors[i] == static_cast<int>(CLOSED))
195  return false;
196 
197  // The state has already been visited by the current thread
198  if ((*it)->colors[tid_] == static_cast<int>(OPEN))
199  return false;
200 
201  // Keep a ptr over the array of colors
202  refs_.push_back((*it)->colors);
203 
204  // Mark state as visited.
205  (*it)->colors[tid_] = OPEN;
206  ++states_;
207  return true;
208  }
209 
210  bool pop()
211  {
212  // Track maximum dfs size
213  dfs_ = todo_.size() > dfs_ ? todo_.size() : dfs_;
214 
215  // Don't avoid pop but modify the status of the state
216  // during backtrack
217  refs_.back()[tid_] = CLOSED;
218  refs_.pop_back();
219  return true;
220  }
221 
222  void finalize()
223  {
224  bool tst_val = false;
225  bool new_val = true;
226  bool exchanged = stop_.compare_exchange_strong(tst_val, new_val);
227  if (exchanged)
228  finisher_ = true;
229  tm_.stop("DFS thread " + std::to_string(tid_));
230  }
231 
232  bool finisher()
233  {
234  return finisher_;
235  }
236 
237  unsigned states()
238  {
239  return states_;
240  }
241 
242  unsigned transitions()
243  {
244  return transitions_;
245  }
246 
247  unsigned walltime()
248  {
249  return tm_.timer("DFS thread " + std::to_string(tid_)).walltime();
250  }
251 
252  std::string name()
253  {
254  if (compute_deadlock)
255  return "deadlock";
256  return "reachability";
257  }
258 
259  int sccs()
260  {
261  return -1;
262  }
263 
264  mc_rvalue result()
265  {
266  if (compute_deadlock)
267  return deadlock_ ? mc_rvalue::DEADLOCK : mc_rvalue::NO_DEADLOCK;
268  return mc_rvalue::SUCCESS;
269  }
270 
271  std::string trace()
272  {
273  std::string result;
274  for (auto& e: todo_)
275  result += sys_.to_string(e.s, tid_);
276  return result;
277  }
278 
279  private:
280  struct todo_element
281  {
282  State s;
283  SuccIterator* it;
284  unsigned current_tr;
285  };
286  kripkecube<State, SuccIterator>& sys_;
287  std::vector<todo_element> todo_;
288  unsigned transitions_ = 0;
289  unsigned tid_;
290  shared_map map_;
291  spot::timer_map tm_;
292  unsigned states_ = 0;
293  unsigned dfs_ = 0;
295  unsigned nb_th_ = 0;
296  fixed_size_pool<pool_type::Unsafe> p_;
297  fixed_size_pool<pool_type::Unsafe> p_pair_;
298  bool deadlock_ = false;
299  std::atomic<bool>& stop_;
302  std::vector<int*> refs_;
303  bool finisher_ = false;
304  };
305 }
This class allows to ensure (at compile time) if a given parameter is of type kripkecube....
Definition: kripke.hh:71
This class is a template representation of a Kripke structure. It is composed of two template paramet...
Definition: kripke.hh:40
This class aims to explore a model to detect wether it contains a deadlock. This deadlock detection p...
Definition: deadlock.hh:46
brick::hashset::FastConcurrent< deadlock_pair *, pair_hasher > shared_map
<
Definition: deadlock.hh:94
A map of timer, where each timer has a name.
Definition: timer.hh:225
Definition: automata.hh:26
mc_rvalue
Definition: mc.hh:43
@ NO_DEADLOCK
No deadlock has been found.
@ DEADLOCK
A deadlock has been found.
@ SUCCESS
The Algorithm finished normally.

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Fri Feb 27 2015 10:00:07 for spot by doxygen 1.9.1