spot  2.12
bloemen.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 <stdlib.h>
24 #include <thread>
25 #include <vector>
26 #include <utility>
27 #include <spot/bricks/brick-hashset>
28 #include <spot/kripke/kripke.hh>
29 #include <spot/misc/common.hh>
30 #include <spot/misc/fixpool.hh>
31 #include <spot/misc/timer.hh>
32 #include <spot/twacube/twacube.hh>
33 #include <spot/twacube/fwd.hh>
34 #include <spot/mc/mc.hh>
35 
36 namespace spot
37 {
38  template<typename State,
39  typename StateHash,
40  typename StateEqual>
42  {
43 
44  public:
45  enum class uf_status { LIVE, LOCK, DEAD };
46  enum class list_status { BUSY, LOCK, DONE };
47  enum class claim_status { CLAIM_FOUND, CLAIM_NEW, CLAIM_DEAD };
48 
50  struct uf_element
51  {
53  State st_;
55  std::atomic<uf_element*> parent;
57  std::atomic<unsigned> worker_;
59  std::atomic<uf_element*> next_;
61  std::atomic<uf_status> uf_status_;
63  std::atomic<list_status> list_status_;
64  };
65 
68  {
70  { }
71 
72  uf_element_hasher() = default;
73 
74  brick::hash::hash128_t
75  hash(const uf_element* lhs) const
76  {
77  StateHash hash;
78  // Not modulo 31 according to brick::hashset specifications.
79  unsigned u = hash(lhs->st_) % (1<<30);
80  return {u, u};
81  }
82 
83  bool equal(const uf_element* lhs,
84  const uf_element* rhs) const
85  {
86  StateEqual equal;
87  return equal(lhs->st_, rhs->st_);
88  }
89  };
90 
92  using shared_map = brick::hashset::FastConcurrent <uf_element*,
94 
96  map_(uf.map_), tid_(uf.tid_), size_(std::thread::hardware_concurrency()),
97  nb_th_(std::thread::hardware_concurrency()), inserted_(0),
98  p_(sizeof(uf_element))
99  { }
100 
101 
102  iterable_uf(shared_map& map, unsigned tid):
103  map_(map), tid_(tid), size_(std::thread::hardware_concurrency()),
104  nb_th_(std::thread::hardware_concurrency()), inserted_(0),
105  p_(sizeof(uf_element))
106  {
107  }
108 
109  ~iterable_uf() {}
110 
111  std::pair<claim_status, uf_element*>
112  make_claim(State a)
113  {
114  unsigned w_id = (1U << tid_);
115 
116  // Setup and try to insert the new state in the shared map.
117  uf_element* v = (uf_element*) p_.allocate();
118  v->st_ = a;
119  v->parent = v;
120  v->next_ = v;
121  v->worker_ = 0;
122  v->uf_status_ = uf_status::LIVE;
123  v->list_status_ = list_status::BUSY;
124 
125  auto it = map_.insert({v});
126  bool b = it.isnew();
127 
128  // Insertion failed, delete element
129  // FIXME: Should we add a local cache to avoid useless allocations?
130  if (!b)
131  p_.deallocate(v);
132  else
133  ++inserted_;
134 
135  uf_element* a_root = find(*it);
136  if (a_root->uf_status_.load() == uf_status::DEAD)
137  return {claim_status::CLAIM_DEAD, *it};
138 
139  if ((a_root->worker_.load() & w_id) != 0)
140  return {claim_status::CLAIM_FOUND, *it};
141 
142  atomic_fetch_or(&(a_root->worker_), w_id);
143  while (a_root->parent.load() != a_root)
144  {
145  a_root = find(a_root);
146  atomic_fetch_or(&(a_root->worker_), w_id);
147  }
148 
149  return {claim_status::CLAIM_NEW, *it};
150  }
151 
152  uf_element* find(uf_element* a)
153  {
154  uf_element* parent = a->parent.load();
155  uf_element* x = a;
156  uf_element* y;
157 
158  while (x != parent)
159  {
160  y = parent;
161  parent = y->parent.load();
162  if (parent == y)
163  return y;
164  x->parent.store(parent);
165  x = parent;
166  parent = x->parent.load();
167  }
168  return x;
169  }
170 
171  bool sameset(uf_element* a, uf_element* b)
172  {
173  while (true)
174  {
175  uf_element* a_root = find(a);
176  uf_element* b_root = find(b);
177  if (a_root == b_root)
178  return true;
179 
180  if (a_root->parent.load() == a_root)
181  return false;
182  }
183  }
184 
185  bool lock_root(uf_element* a)
186  {
187  uf_status expected = uf_status::LIVE;
188  if (a->uf_status_.load() == expected)
189  {
190  if (std::atomic_compare_exchange_strong
191  (&(a->uf_status_), &expected, uf_status::LOCK))
192  {
193  if (a->parent.load() == a)
194  return true;
195  unlock_root(a);
196  }
197  }
198  return false;
199  }
200 
201  inline void unlock_root(uf_element* a)
202  {
203  a->uf_status_.store(uf_status::LIVE);
204  }
205 
206  uf_element* lock_list(uf_element* a)
207  {
208  uf_element* a_list = a;
209  while (true)
210  {
211  bool dontcare = false;
212  a_list = pick_from_list(a_list, &dontcare);
213  if (a_list == nullptr)
214  {
215  return nullptr;
216  }
217 
218  auto expected = list_status::BUSY;
219  bool b = std::atomic_compare_exchange_strong
220  (&(a_list->list_status_), &expected, list_status::LOCK);
221 
222  if (b)
223  return a_list;
224 
225  a_list = a_list->next_.load();
226  }
227  }
228 
229  void unlock_list(uf_element* a)
230  {
231  a->list_status_.store(list_status::BUSY);
232  }
233 
234  void unite(uf_element* a, uf_element* b)
235  {
236  uf_element* a_root;
237  uf_element* b_root;
238  uf_element* q;
239  uf_element* r;
240 
241  while (true)
242  {
243  a_root = find(a);
244  b_root = find(b);
245 
246  if (a_root == b_root)
247  return;
248 
249  r = std::max(a_root, b_root);
250  q = std::min(a_root, b_root);
251 
252  if (!lock_root(q))
253  continue;
254 
255  break;
256  }
257 
258  uf_element* a_list = lock_list(a);
259  if (a_list == nullptr)
260  {
261  unlock_root(q);
262  return;
263  }
264 
265  uf_element* b_list = lock_list(b);
266  if (b_list == nullptr)
267  {
268  unlock_list(a_list);
269  unlock_root(q);
270  return;
271  }
272 
273  SPOT_ASSERT(a_list->list_status_.load() == list_status::LOCK);
274  SPOT_ASSERT(b_list->list_status_.load() == list_status::LOCK);
275 
276  // Swapping
277  uf_element* a_next = a_list->next_.load();
278  uf_element* b_next = b_list->next_.load();
279  SPOT_ASSERT(a_next != nullptr);
280  SPOT_ASSERT(b_next != nullptr);
281 
282  a_list->next_.store(b_next);
283  b_list->next_.store(a_next);
284  q->parent.store(r);
285 
286  // Update workers
287  unsigned q_worker = q->worker_.load();
288  unsigned r_worker = r->worker_.load();
289  if ((q_worker|r_worker) != r_worker)
290  {
291  atomic_fetch_or(&(r->worker_), q_worker);
292  while (r->parent.load() != r)
293  {
294  r = find(r);
295  atomic_fetch_or(&(r->worker_), q_worker);
296  }
297  }
298 
299  unlock_list(a_list);
300  unlock_list(b_list);
301  unlock_root(q);
302  }
303 
304  uf_element* pick_from_list(uf_element* u, bool* sccfound)
305  {
306  uf_element* a = u;
307  while (true)
308  {
309  list_status a_status;
310  while (true)
311  {
312  a_status = a->list_status_.load();
313 
314  if (a_status == list_status::BUSY)
315  {
316  return a;
317  }
318 
319  if (a_status == list_status::DONE)
320  break;
321  }
322 
323  uf_element* b = a->next_.load();
324 
325  // ------------------------------ NO LAZY : start
326  // if (b == u)
327  // {
328  // uf_element* a_root = find(a);
329  // uf_status status = a_root->uf_status_.load();
330  // while (status != uf_status::DEAD)
331  // {
332  // if (status == uf_status::LIVE)
333  // *sccfound = std::atomic_compare_exchange_strong
334  // (&(a_root->uf_status_), &status, uf_status::DEAD);
335  // status = a_root->uf_status_.load();
336  // }
337  // return nullptr;
338  // }
339  // a = b;
340  // ------------------------------ NO LAZY : end
341 
342  if (a == b)
343  {
344  uf_element* a_root = find(u);
345  uf_status status = a_root->uf_status_.load();
346  while (status != uf_status::DEAD)
347  {
348  if (status == uf_status::LIVE)
349  *sccfound = std::atomic_compare_exchange_strong
350  (&(a_root->uf_status_), &status, uf_status::DEAD);
351  status = a_root->uf_status_.load();
352  }
353  return nullptr;
354  }
355 
356  list_status b_status;
357  while (true)
358  {
359  b_status = b->list_status_.load();
360 
361  if (b_status == list_status::BUSY)
362  {
363  return b;
364  }
365 
366  if (b_status == list_status::DONE)
367  break;
368  }
369 
370  SPOT_ASSERT(b_status == list_status::DONE);
371  SPOT_ASSERT(a_status == list_status::DONE);
372 
373  uf_element* c = b->next_.load();
374  a->next_.store(c);
375  a = c;
376  }
377  }
378 
379  void remove_from_list(uf_element* a)
380  {
381  while (true)
382  {
383  list_status a_status = a->list_status_.load();
384 
385  if (a_status == list_status::DONE)
386  break;
387 
388  if (a_status == list_status::BUSY)
389  std::atomic_compare_exchange_strong
390  (&(a->list_status_), &a_status, list_status::DONE);
391  }
392  }
393 
394  unsigned inserted()
395  {
396  return inserted_;
397  }
398 
399  private:
400  iterable_uf() = default;
401 
402  shared_map map_;
403  unsigned tid_;
404  unsigned size_;
405  unsigned nb_th_;
406  unsigned inserted_;
407  fixed_size_pool<pool_type::Unsafe> p_;
408  };
409 
413  template<typename State, typename SuccIterator,
414  typename StateHash, typename StateEqual>
416  {
417  private:
418  swarmed_bloemen() = delete;
419 
420  public:
421 
423  using uf_element = typename uf::uf_element;
424 
425  using shared_struct = uf;
426  using shared_map = typename uf::shared_map;
427 
428  static shared_struct* make_shared_structure(shared_map m, unsigned i)
429  {
430  return new uf(m, i);
431  }
432 
434  twacube_ptr, /* useless here */
435  shared_map& map, /* useless here */
437  unsigned tid,
438  std::atomic<bool>& stop):
439  sys_(sys), uf_(*uf), tid_(tid),
440  nb_th_(std::thread::hardware_concurrency()),
441  stop_(stop)
442  {
443  static_assert(spot::is_a_kripkecube_ptr<decltype(&sys),
444  State, SuccIterator>::value,
445  "error: does not match the kripkecube requirements");
446  }
447 
448  void run()
449  {
450  setup();
451  State init = sys_.initial(tid_);
452  auto pair = uf_.make_claim(init);
453  todo_.push_back(pair.second);
454  Rp_.push_back(pair.second);
455  ++states_;
456 
457  while (!todo_.empty())
458  {
459  bloemen_recursive_start:
460  while (!stop_.load(std::memory_order_relaxed))
461  {
462  bool sccfound = false;
463  uf_element* v_prime = uf_.pick_from_list(todo_.back(), &sccfound);
464  if (v_prime == nullptr)
465  {
466  // The SCC has been explored!
467  sccs_ += sccfound;
468  break;
469  }
470 
471  auto it = sys_.succ(v_prime->st_, tid_);
472  while (!it->done())
473  {
474  auto w = uf_.make_claim(it->state());
475  it->next();
476  ++transitions_;
477  if (w.first == uf::claim_status::CLAIM_NEW)
478  {
479  todo_.push_back(w.second);
480  Rp_.push_back(w.second);
481  ++states_;
482  sys_.recycle(it, tid_);
483  goto bloemen_recursive_start;
484  }
485  else if (w.first == uf::claim_status::CLAIM_FOUND)
486  {
487  while (!uf_.sameset(todo_.back(), w.second))
488  {
489  uf_element* r = Rp_.back();
490  Rp_.pop_back();
491  uf_.unite(r, Rp_.back());
492  }
493  }
494  }
495  uf_.remove_from_list(v_prime);
496  sys_.recycle(it, tid_);
497  }
498 
499  if (todo_.back() == Rp_.back())
500  Rp_.pop_back();
501  todo_.pop_back();
502  }
503  finalize();
504  }
505 
506  void setup()
507  {
508  tm_.start("DFS thread " + std::to_string(tid_));
509  }
510 
511  void finalize()
512  {
513  bool tst_val = false;
514  bool new_val = true;
515  bool exchanged = stop_.compare_exchange_strong(tst_val, new_val);
516  if (exchanged)
517  finisher_ = true;
518  tm_.stop("DFS thread " + std::to_string(tid_));
519  }
520 
521  bool finisher()
522  {
523  return finisher_;
524  }
525 
526  unsigned states()
527  {
528  return states_;
529  }
530 
531  unsigned transitions()
532  {
533  return transitions_;
534  }
535 
536  unsigned walltime()
537  {
538  return tm_.timer("DFS thread " + std::to_string(tid_)).walltime();
539  }
540 
541  std::string name()
542  {
543  return "bloemen_scc";
544  }
545 
546  int sccs()
547  {
548  return sccs_;
549  }
550 
551  mc_rvalue result()
552  {
553  return mc_rvalue::SUCCESS;
554  }
555 
556  std::string trace()
557  {
558  // Returning a trace has no sense in this algorithm
559  return "";
560  }
561 
562  private:
564  std::vector<uf_element*> todo_;
565  std::vector<uf_element*> Rp_;
567  unsigned tid_;
568  unsigned nb_th_;
569  unsigned inserted_ = 0;
570  unsigned states_ = 0;
571  unsigned transitions_ = 0;
572  unsigned sccs_ = 0;
573  spot::timer_map tm_;
574  std::atomic<bool>& stop_;
575  bool finisher_ = false;
576  };
577 }
void * allocate()
Allocate size bytes of memory.
Definition: fixpool.hh:88
void deallocate(void *ptr)
Recycle size bytes of memory.
Definition: fixpool.hh:132
This class allows to ensure (at compile time) if a given parameter is of type kripkecube....
Definition: kripke.hh:71
Definition: bloemen.hh:42
This class is a template representation of a Kripke structure. It is composed of two template paramet...
Definition: kripke.hh:40
This class implements the SCC decomposition algorithm of bloemen as described in PPOPP'16....
Definition: bloemen.hh:416
A map of timer, where each timer has a name.
Definition: timer.hh:225
void stop(const std::string &name)
Stop timer name.
Definition: timer.hh:245
void start(const std::string &name)
Start a timer with name name.
Definition: timer.hh:234
const spot::timer & timer(const std::string &name) const
Return the timer name.
Definition: timer.hh:270
std::chrono::milliseconds::rep walltime() const
Return cumulative wall time.
Definition: timer.hh:203
Definition: automata.hh:26
mc_rvalue
Definition: mc.hh:43
@ SUCCESS
The Algorithm finished normally.
The hasher for the previous uf_element. Shortcut to ease shared map manipulation.
Definition: bloemen.hh:68
Represents a Union-Find element.
Definition: bloemen.hh:51
std::atomic< unsigned > worker_
The set of worker for a given state.
Definition: bloemen.hh:57
State st_
the state handled by the element
Definition: bloemen.hh:53
std::atomic< uf_element * > parent
reference to the pointer
Definition: bloemen.hh:55
std::atomic< uf_element * > next_
next element for work stealing
Definition: bloemen.hh:59
std::atomic< uf_status > uf_status_
current status for the element
Definition: bloemen.hh:61

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