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

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.4