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

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