spot  2.12.2
bloemen_ec.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 <utility>
28 #include <spot/misc/common.hh>
29 #include <spot/kripke/kripke.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/intersect.hh>
35 #include <spot/mc/mc.hh>
36 
37 namespace spot
38 {
39  template<typename State,
40  typename StateHash,
41  typename StateEqual>
43  {
44 
45  public:
46  enum class uf_status { LIVE, LOCK, DEAD };
47  enum class list_status { BUSY, LOCK, DONE };
48  enum class claim_status { CLAIM_FOUND, CLAIM_NEW, CLAIM_DEAD };
49 
51  struct uf_element
52  {
54  State st_kripke;
56  unsigned st_prop;
60  std::mutex acc_mutex_;
62  std::atomic<uf_element*> parent;
64  std::atomic<unsigned> worker_;
66  std::atomic<uf_element*> next_;
68  std::atomic<uf_status> uf_status_;
70  std::atomic<list_status> list_status_;
71  };
72 
75  {
77  { }
78 
79  uf_element_hasher() = default;
80 
81  brick::hash::hash128_t
82  hash(const uf_element* lhs) const
83  {
84  StateHash hash;
85  // Not modulo 31 according to brick::hashset specifications.
86  unsigned u = hash(lhs->st_kripke) % (1<<30);
87  u = wang32_hash(lhs->st_prop) ^ u;
88  u = u % (1<<30);
89  return {u, u};
90  }
91 
92  bool equal(const uf_element* lhs,
93  const uf_element* rhs) const
94  {
95  StateEqual equal;
96  return (lhs->st_prop == rhs->st_prop)
97  && equal(lhs->st_kripke, rhs->st_kripke);
98  }
99  };
100 
102  using shared_map = brick::hashset::FastConcurrent <uf_element*,
104 
106  map_(uf.map_), tid_(uf.tid_), size_(std::thread::hardware_concurrency()),
107  nb_th_(std::thread::hardware_concurrency()), inserted_(0),
108  p_(sizeof(uf_element))
109  { }
110 
111  iterable_uf_ec(shared_map& map, unsigned tid):
112  map_(map), tid_(tid), size_(std::thread::hardware_concurrency()),
113  nb_th_(std::thread::hardware_concurrency()), inserted_(0),
114  p_(sizeof(uf_element))
115  { }
116 
117  ~iterable_uf_ec() {}
118 
119  std::pair<claim_status, uf_element*>
120  make_claim(State kripke, unsigned prop)
121  {
122  unsigned w_id = (1U << tid_);
123 
124  // Setup and try to insert the new state in the shared map.
125  uf_element* v = (uf_element*) p_.allocate();
126  new (v) (uf_element); // required, otherwise the mutex is unitialized
127  v->st_kripke = kripke;
128  v->st_prop = prop;
129  v->acc = {};
130  v->parent = v;
131  v->next_ = v;
132  v->worker_ = 0;
133  v->uf_status_ = uf_status::LIVE;
134  v->list_status_ = list_status::BUSY;
135 
136  auto it = map_.insert({v});
137  bool b = it.isnew();
138 
139  // Insertion failed, delete element
140  // FIXME Should we add a local cache to avoid useless allocations?
141  if (!b)
142  p_.deallocate(v);
143  else
144  ++inserted_;
145 
146  uf_element* a_root = find(*it);
147  if (a_root->uf_status_.load() == uf_status::DEAD)
148  return {claim_status::CLAIM_DEAD, *it};
149 
150  if ((a_root->worker_.load() & w_id) != 0)
151  return {claim_status::CLAIM_FOUND, *it};
152 
153  atomic_fetch_or(&(a_root->worker_), w_id);
154  while (a_root->parent.load() != a_root)
155  {
156  a_root = find(a_root);
157  atomic_fetch_or(&(a_root->worker_), w_id);
158  }
159 
160  return {claim_status::CLAIM_NEW, *it};
161  }
162 
163  uf_element* find(uf_element* a)
164  {
165  uf_element* parent = a->parent.load();
166  uf_element* x = a;
167  uf_element* y;
168 
169  while (x != parent)
170  {
171  y = parent;
172  parent = y->parent.load();
173  if (parent == y)
174  return y;
175  x->parent.store(parent);
176  x = parent;
177  parent = x->parent.load();
178  }
179  return x;
180  }
181 
182  bool sameset(uf_element* a, uf_element* b)
183  {
184  while (true)
185  {
186  uf_element* a_root = find(a);
187  uf_element* b_root = find(b);
188  if (a_root == b_root)
189  return true;
190 
191  if (a_root->parent.load() == a_root)
192  return false;
193  }
194  }
195 
196  bool lock_root(uf_element* a)
197  {
198  uf_status expected = uf_status::LIVE;
199  if (a->uf_status_.load() == expected)
200  {
201  if (std::atomic_compare_exchange_strong
202  (&(a->uf_status_), &expected, uf_status::LOCK))
203  {
204  if (a->parent.load() == a)
205  return true;
206  unlock_root(a);
207  }
208  }
209  return false;
210  }
211 
212  inline void unlock_root(uf_element* a)
213  {
214  a->uf_status_.store(uf_status::LIVE);
215  }
216 
217  uf_element* lock_list(uf_element* a)
218  {
219  uf_element* a_list = a;
220  while (true)
221  {
222  bool dontcare = false;
223  a_list = pick_from_list(a_list, &dontcare);
224  if (a_list == nullptr)
225  {
226  return nullptr;
227  }
228 
229  auto expected = list_status::BUSY;
230  bool b = std::atomic_compare_exchange_strong
231  (&(a_list->list_status_), &expected, list_status::LOCK);
232 
233  if (b)
234  return a_list;
235 
236  a_list = a_list->next_.load();
237  }
238  }
239 
240  void unlock_list(uf_element* a)
241  {
242  a->list_status_.store(list_status::BUSY);
243  }
244 
245  acc_cond::mark_t
246  unite(uf_element* a, uf_element* b, acc_cond::mark_t acc)
247  {
248  uf_element* a_root;
249  uf_element* b_root;
250  uf_element* q;
251  uf_element* r;
252 
253  do
254  {
255  a_root = find(a);
256  b_root = find(b);
257 
258  if (a_root == b_root)
259  {
260  // Update acceptance condition
261  {
262  std::lock_guard<std::mutex> rlock(a_root->acc_mutex_);
263  acc |= a_root->acc;
264  a_root->acc = acc;
265  }
266 
267  while (a_root->parent.load() != a_root)
268  {
269  a_root = find(a_root);
270  std::lock_guard<std::mutex> rlock(a_root->acc_mutex_);
271  acc |= a_root->acc;
272  a_root->acc = acc;
273  }
274  return acc;
275  }
276 
277  r = std::max(a_root, b_root);
278  q = std::min(a_root, b_root);
279  }
280  while (!lock_root(q));
281 
282  uf_element* a_list = lock_list(a);
283  if (a_list == nullptr)
284  {
285  unlock_root(q);
286  return acc;
287  }
288 
289  uf_element* b_list = lock_list(b);
290  if (b_list == nullptr)
291  {
292  unlock_list(a_list);
293  unlock_root(q);
294  return acc;
295  }
296 
297  SPOT_ASSERT(a_list->list_status_.load() == list_status::LOCK);
298  SPOT_ASSERT(b_list->list_status_.load() == list_status::LOCK);
299 
300  // Swapping
301  uf_element* a_next = a_list->next_.load();
302  uf_element* b_next = b_list->next_.load();
303  SPOT_ASSERT(a_next != nullptr);
304  SPOT_ASSERT(b_next != nullptr);
305 
306  a_list->next_.store(b_next);
307  b_list->next_.store(a_next);
308  q->parent.store(r);
309 
310  // Update workers
311  unsigned q_worker = q->worker_.load();
312  unsigned r_worker = r->worker_.load();
313  if ((q_worker|r_worker) != r_worker)
314  {
315  atomic_fetch_or(&(r->worker_), q_worker);
316  while (r->parent.load() != r)
317  {
318  r = find(r);
319  atomic_fetch_or(&(r->worker_), q_worker);
320  }
321  }
322 
323  // Update acceptance condition
324  {
325  std::lock_guard<std::mutex> rlock(r->acc_mutex_);
326  std::lock_guard<std::mutex> qlock(q->acc_mutex_);
327  acc |= r->acc | q->acc;
328  r->acc = q->acc = acc;
329  }
330 
331  while (r->parent.load() != r)
332  {
333  r = find(r);
334  std::lock_guard<std::mutex> rlock(r->acc_mutex_);
335  std::lock_guard<std::mutex> qlock(q->acc_mutex_);
336  acc |= r->acc | q->acc;
337  r->acc = acc;
338  }
339 
340  unlock_list(a_list);
341  unlock_list(b_list);
342  unlock_root(q);
343  return acc;
344  }
345 
346  uf_element* pick_from_list(uf_element* u, bool* sccfound)
347  {
348  uf_element* a = u;
349  while (true)
350  {
351  list_status a_status;
352  while (true)
353  {
354  a_status = a->list_status_.load();
355 
356  if (a_status == list_status::BUSY)
357  return a;
358 
359  if (a_status == list_status::DONE)
360  break;
361  }
362 
363  uf_element* b = a->next_.load();
364 
365  // ------------------------------ NO LAZY : start
366  // if (b == u)
367  // {
368  // uf_element* a_root = find(a);
369  // uf_status status = a_root->uf_status_.load();
370  // while (status != uf_status::DEAD)
371  // {
372  // if (status == uf_status::LIVE)
373  // *sccfound = std::atomic_compare_exchange_strong
374  // (&(a_root->uf_status_), &status, uf_status::DEAD);
375  // status = a_root->uf_status_.load();
376  // }
377  // return nullptr;
378  // }
379  // a = b;
380  // ------------------------------ NO LAZY : end
381 
382  if (a == b)
383  {
384  uf_element* a_root = find(u);
385  uf_status status = a_root->uf_status_.load();
386  while (status != uf_status::DEAD)
387  {
388  if (status == uf_status::LIVE)
389  *sccfound = std::atomic_compare_exchange_strong
390  (&(a_root->uf_status_), &status, uf_status::DEAD);
391  status = a_root->uf_status_.load();
392  }
393  return nullptr;
394  }
395 
396  list_status b_status;
397  while (true)
398  {
399  b_status = b->list_status_.load();
400 
401  if (b_status == list_status::BUSY)
402  return b;
403 
404  if (b_status == list_status::DONE)
405  break;
406  }
407 
408  SPOT_ASSERT(b_status == list_status::DONE);
409  SPOT_ASSERT(a_status == list_status::DONE);
410 
411  uf_element* c = b->next_.load();
412  a->next_.store(c);
413  a = c;
414  }
415  }
416 
417  void remove_from_list(uf_element* a)
418  {
419  while (true)
420  {
421  list_status a_status = a->list_status_.load();
422 
423  if (a_status == list_status::DONE)
424  break;
425 
426  if (a_status == list_status::BUSY)
427  std::atomic_compare_exchange_strong
428  (&(a->list_status_), &a_status, list_status::DONE);
429  }
430  }
431 
432  unsigned inserted()
433  {
434  return inserted_;
435  }
436 
437  private:
438  iterable_uf_ec() = default;
439 
440  shared_map map_;
441  unsigned tid_;
442  unsigned size_;
443  unsigned nb_th_;
444  unsigned inserted_;
445  fixed_size_pool<pool_type::Unsafe> p_;
446  };
447 
451  template<typename State, typename SuccIterator,
452  typename StateHash, typename StateEqual>
454  {
455  private:
456  swarmed_bloemen_ec() = delete;
457  public:
458 
460  using uf_element = typename uf::uf_element;
461 
462  using shared_struct = uf;
463  using shared_map = typename uf::shared_map;
464 
465  static shared_struct* make_shared_structure(shared_map m, unsigned i)
466  {
467  return new uf(m, i);
468  }
469 
471  twacube_ptr twa,
472  shared_map& map, /* useless here */
474  unsigned tid,
475  std::atomic<bool>& stop):
476  sys_(sys), twa_(twa), uf_(*uf), tid_(tid),
477  nb_th_(std::thread::hardware_concurrency()),
478  stop_(stop)
479  {
480  static_assert(spot::is_a_kripkecube_ptr<decltype(&sys),
481  State, SuccIterator>::value,
482  "error: does not match the kripkecube requirements");
483  }
484 
485  ~swarmed_bloemen_ec() = default;
486 
487  void run()
488  {
489  setup();
490  State init_kripke = sys_.initial(tid_);
491  unsigned init_twa = twa_->get_initial();
492  auto pair = uf_.make_claim(init_kripke, init_twa);
493  todo_.push_back(pair.second);
494  Rp_.push_back(pair.second);
495  ++states_;
496 
497  while (!todo_.empty())
498  {
499  bloemen_recursive_start:
500  while (!stop_.load(std::memory_order_relaxed))
501  {
502  bool sccfound = false;
503  uf_element* v_prime = uf_.pick_from_list(todo_.back(), &sccfound);
504  if (v_prime == nullptr)
505  {
506  // The SCC has been explored!
507  sccs_ += sccfound;
508  break;
509  }
510 
511  auto it_kripke = sys_.succ(v_prime->st_kripke, tid_);
512  auto it_prop = twa_->succ(v_prime->st_prop);
513  forward_iterators(sys_, twa_, it_kripke, it_prop, true, tid_);
514  while (!it_kripke->done())
515  {
516  auto w = uf_.make_claim(it_kripke->state(),
517  twa_->trans_storage(it_prop, tid_)
518  .dst);
519  auto trans_acc = twa_->trans_storage(it_prop, tid_).acc_;
520  ++transitions_;
521  if (w.first == uf::claim_status::CLAIM_NEW)
522  {
523  todo_.push_back(w.second);
524  Rp_.push_back(w.second);
525  ++states_;
526  sys_.recycle(it_kripke, tid_);
527  goto bloemen_recursive_start;
528  }
529  else if (w.first == uf::claim_status::CLAIM_FOUND)
530  {
531  acc_cond::mark_t scc_acc = trans_acc;
532 
533  // This operation is mandatory to update acceptance marks.
534  // Otherwise, when w.second and todo.back() are
535  // already in the same set, the acceptance condition will
536  // not be added.
537  scc_acc |= uf_.unite(w.second, w.second, scc_acc);
538 
539  while (!uf_.sameset(todo_.back(), w.second))
540  {
541  uf_element* r = Rp_.back();
542  Rp_.pop_back();
543  uf_.unite(r, Rp_.back(), scc_acc);
544  }
545 
546 
547  {
548  auto root = uf_.find(w.second);
549  std::lock_guard<std::mutex> lock(root->acc_mutex_);
550  scc_acc = root->acc;
551  }
552 
553  // cycle found in SCC and it contains acceptance condition
554  if (twa_->acc().accepting(scc_acc))
555  {
556  sys_.recycle(it_kripke, tid_);
557  stop_ = true;
558  is_empty_ = false;
559  tm_.stop("DFS thread " + std::to_string(tid_));
560  return;
561  }
562  }
563  forward_iterators(sys_, twa_, it_kripke, it_prop,
564  false, tid_);
565  }
566  uf_.remove_from_list(v_prime);
567  sys_.recycle(it_kripke, tid_);
568  }
569 
570  if (todo_.back() == Rp_.back())
571  Rp_.pop_back();
572  todo_.pop_back();
573  }
574  finalize();
575  }
576 
577  void setup()
578  {
579  tm_.start("DFS thread " + std::to_string(tid_));
580  }
581 
582  void finalize()
583  {
584  bool tst_val = false;
585  bool new_val = true;
586  bool exchanged = stop_.compare_exchange_strong(tst_val, new_val);
587  if (exchanged)
588  finisher_ = true;
589  tm_.stop("DFS thread " + std::to_string(tid_));
590  }
591 
592  bool finisher()
593  {
594  return finisher_;
595  }
596 
597  unsigned states()
598  {
599  return states_;
600  }
601 
602  unsigned transitions()
603  {
604  return transitions_;
605  }
606 
607  unsigned walltime()
608  {
609  return tm_.timer("DFS thread " + std::to_string(tid_)).walltime();
610  }
611 
612  std::string name()
613  {
614  return "bloemen_ec";
615  }
616 
617  int sccs()
618  {
619  return sccs_;
620  }
621 
622  mc_rvalue result()
623  {
624  return is_empty_ ? mc_rvalue::EMPTY : mc_rvalue::NOT_EMPTY;
625  }
626 
627  std::string trace()
628  {
629  return "Not implemented";
630  }
631 
632  private:
634  twacube_ptr twa_;
635  std::vector<uf_element*> todo_;
636  std::vector<uf_element*> Rp_;
638  unsigned tid_;
639  unsigned nb_th_;
640  unsigned inserted_ = 0;
641  unsigned states_ = 0;
642  unsigned transitions_ = 0;
643  unsigned sccs_ = 0;
644  bool is_empty_ = true;
645  spot::timer_map tm_;
646  std::atomic<bool>& stop_;
647  bool finisher_ = false;
648  };
649 }
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_ec.hh:43
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_ec.hh:454
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
A Transition-based ω-Automaton.
Definition: twa.hh:619
size_t wang32_hash(size_t key)
Thomas Wang's 32 bit hash function.
Definition: hashfunc.hh:37
Definition: automata.hh:26
mc_rvalue
Definition: mc.hh:43
@ NOT_EMPTY
The product is not empty.
@ EMPTY
The product is empty.
An acceptance mark.
Definition: acc.hh:84
The hasher for the previous uf_element. Shortcut to ease shared map manipulation.
Definition: bloemen_ec.hh:75
Represents a Union-Find element.
Definition: bloemen_ec.hh:52
State st_kripke
the kripke state handled by the element
Definition: bloemen_ec.hh:54
std::mutex acc_mutex_
mutex for acceptance condition
Definition: bloemen_ec.hh:60
std::atomic< uf_element * > parent
reference to the pointer
Definition: bloemen_ec.hh:62
std::atomic< unsigned > worker_
The set of worker for a given state.
Definition: bloemen_ec.hh:64
unsigned st_prop
the prop state handled by the element
Definition: bloemen_ec.hh:56
acc_cond::mark_t acc
acceptance conditions of the union
Definition: bloemen_ec.hh:58
std::atomic< uf_status > uf_status_
current status for the element
Definition: bloemen_ec.hh:68
std::atomic< uf_element * > next_
next element for work stealing
Definition: bloemen_ec.hh:66

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