spot 2.11.6.dev
Loading...
Searching...
No Matches
bloemen_ec.hh
1// -*- coding: utf-8 -*-
2// Copyright (C) 2015-2020, 2022 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
38namespace 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
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 do
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 acc |= a_root->acc;
265 a_root->acc = 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 acc |= a_root->acc;
273 a_root->acc = 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 while (!lock_root(q));
282
283 uf_element* a_list = lock_list(a);
284 if (a_list == nullptr)
285 {
286 unlock_root(q);
287 return acc;
288 }
289
290 uf_element* b_list = lock_list(b);
291 if (b_list == nullptr)
292 {
293 unlock_list(a_list);
294 unlock_root(q);
295 return acc;
296 }
297
298 SPOT_ASSERT(a_list->list_status_.load() == list_status::LOCK);
299 SPOT_ASSERT(b_list->list_status_.load() == list_status::LOCK);
300
301 // Swapping
302 uf_element* a_next = a_list->next_.load();
303 uf_element* b_next = b_list->next_.load();
304 SPOT_ASSERT(a_next != nullptr);
305 SPOT_ASSERT(b_next != nullptr);
306
307 a_list->next_.store(b_next);
308 b_list->next_.store(a_next);
309 q->parent.store(r);
310
311 // Update workers
312 unsigned q_worker = q->worker_.load();
313 unsigned r_worker = r->worker_.load();
314 if ((q_worker|r_worker) != r_worker)
315 {
316 atomic_fetch_or(&(r->worker_), q_worker);
317 while (r->parent.load() != r)
318 {
319 r = find(r);
320 atomic_fetch_or(&(r->worker_), q_worker);
321 }
322 }
323
324 // Update acceptance condition
325 {
326 std::lock_guard<std::mutex> rlock(r->acc_mutex_);
327 std::lock_guard<std::mutex> qlock(q->acc_mutex_);
328 acc |= r->acc | q->acc;
329 r->acc = q->acc = acc;
330 }
331
332 while (r->parent.load() != r)
333 {
334 r = find(r);
335 std::lock_guard<std::mutex> rlock(r->acc_mutex_);
336 std::lock_guard<std::mutex> qlock(q->acc_mutex_);
337 acc |= r->acc | q->acc;
338 r->acc = acc;
339 }
340
341 unlock_list(a_list);
342 unlock_list(b_list);
343 unlock_root(q);
344 return acc;
345 }
346
347 uf_element* pick_from_list(uf_element* u, bool* sccfound)
348 {
349 uf_element* a = u;
350 while (true)
351 {
352 list_status a_status;
353 while (true)
354 {
355 a_status = a->list_status_.load();
356
357 if (a_status == list_status::BUSY)
358 return a;
359
360 if (a_status == list_status::DONE)
361 break;
362 }
363
364 uf_element* b = a->next_.load();
365
366 // ------------------------------ NO LAZY : start
367 // if (b == u)
368 // {
369 // uf_element* a_root = find(a);
370 // uf_status status = a_root->uf_status_.load();
371 // while (status != uf_status::DEAD)
372 // {
373 // if (status == uf_status::LIVE)
374 // *sccfound = std::atomic_compare_exchange_strong
375 // (&(a_root->uf_status_), &status, uf_status::DEAD);
376 // status = a_root->uf_status_.load();
377 // }
378 // return nullptr;
379 // }
380 // a = b;
381 // ------------------------------ NO LAZY : end
382
383 if (a == b)
384 {
385 uf_element* a_root = find(u);
386 uf_status status = a_root->uf_status_.load();
387 while (status != uf_status::DEAD)
388 {
389 if (status == uf_status::LIVE)
390 *sccfound = std::atomic_compare_exchange_strong
391 (&(a_root->uf_status_), &status, uf_status::DEAD);
392 status = a_root->uf_status_.load();
393 }
394 return nullptr;
395 }
396
397 list_status b_status;
398 while (true)
399 {
400 b_status = b->list_status_.load();
401
402 if (b_status == list_status::BUSY)
403 return b;
404
405 if (b_status == list_status::DONE)
406 break;
407 }
408
409 SPOT_ASSERT(b_status == list_status::DONE);
410 SPOT_ASSERT(a_status == list_status::DONE);
411
412 uf_element* c = b->next_.load();
413 a->next_.store(c);
414 a = c;
415 }
416 }
417
418 void remove_from_list(uf_element* a)
419 {
420 while (true)
421 {
422 list_status a_status = a->list_status_.load();
423
424 if (a_status == list_status::DONE)
425 break;
426
427 if (a_status == list_status::BUSY)
428 std::atomic_compare_exchange_strong
429 (&(a->list_status_), &a_status, list_status::DONE);
430 }
431 }
432
433 unsigned inserted()
434 {
435 return inserted_;
436 }
437
438 private:
439 iterable_uf_ec() = default;
440
441 shared_map map_;
442 unsigned tid_;
443 unsigned size_;
444 unsigned nb_th_;
445 unsigned inserted_;
446 fixed_size_pool<pool_type::Unsafe> p_;
447 };
448
452 template<typename State, typename SuccIterator,
453 typename StateHash, typename StateEqual>
455 {
456 private:
457 swarmed_bloemen_ec() = delete;
458 public:
459
461 using uf_element = typename uf::uf_element;
462
463 using shared_struct = uf;
464 using shared_map = typename uf::shared_map;
465
466 static shared_struct* make_shared_structure(shared_map m, unsigned i)
467 {
468 return new uf(m, i);
469 }
470
472 twacube_ptr twa,
473 shared_map& map, /* useless here */
475 unsigned tid,
476 std::atomic<bool>& stop):
477 sys_(sys), twa_(twa), uf_(*uf), tid_(tid),
478 nb_th_(std::thread::hardware_concurrency()),
479 stop_(stop)
480 {
481 static_assert(spot::is_a_kripkecube_ptr<decltype(&sys),
482 State, SuccIterator>::value,
483 "error: does not match the kripkecube requirements");
484 }
485
486 ~swarmed_bloemen_ec() = default;
487
488 void run()
489 {
490 setup();
491 State init_kripke = sys_.initial(tid_);
492 unsigned init_twa = twa_->get_initial();
493 auto pair = uf_.make_claim(init_kripke, init_twa);
494 todo_.push_back(pair.second);
495 Rp_.push_back(pair.second);
496 ++states_;
497
498 while (!todo_.empty())
499 {
500 bloemen_recursive_start:
501 while (!stop_.load(std::memory_order_relaxed))
502 {
503 bool sccfound = false;
504 uf_element* v_prime = uf_.pick_from_list(todo_.back(), &sccfound);
505 if (v_prime == nullptr)
506 {
507 // The SCC has been explored!
508 sccs_ += sccfound;
509 break;
510 }
511
512 auto it_kripke = sys_.succ(v_prime->st_kripke, tid_);
513 auto it_prop = twa_->succ(v_prime->st_prop);
514 forward_iterators(sys_, twa_, it_kripke, it_prop, true, tid_);
515 while (!it_kripke->done())
516 {
517 auto w = uf_.make_claim(it_kripke->state(),
518 twa_->trans_storage(it_prop, tid_)
519 .dst);
520 auto trans_acc = twa_->trans_storage(it_prop, tid_).acc_;
521 ++transitions_;
522 if (w.first == uf::claim_status::CLAIM_NEW)
523 {
524 todo_.push_back(w.second);
525 Rp_.push_back(w.second);
526 ++states_;
527 sys_.recycle(it_kripke, tid_);
528 goto bloemen_recursive_start;
529 }
530 else if (w.first == uf::claim_status::CLAIM_FOUND)
531 {
532 acc_cond::mark_t scc_acc = trans_acc;
533
534 // This operation is mandatory to update acceptance marks.
535 // Otherwise, when w.second and todo.back() are
536 // already in the same set, the acceptance condition will
537 // not be added.
538 scc_acc |= uf_.unite(w.second, w.second, scc_acc);
539
540 while (!uf_.sameset(todo_.back(), w.second))
541 {
542 uf_element* r = Rp_.back();
543 Rp_.pop_back();
544 uf_.unite(r, Rp_.back(), scc_acc);
545 }
546
547
548 {
549 auto root = uf_.find(w.second);
550 std::lock_guard<std::mutex> lock(root->acc_mutex_);
551 scc_acc = root->acc;
552 }
553
554 // cycle found in SCC and it contains acceptance condition
555 if (twa_->acc().accepting(scc_acc))
556 {
557 sys_.recycle(it_kripke, tid_);
558 stop_ = true;
559 is_empty_ = false;
560 tm_.stop("DFS thread " + std::to_string(tid_));
561 return;
562 }
563 }
564 forward_iterators(sys_, twa_, it_kripke, it_prop,
565 false, tid_);
566 }
567 uf_.remove_from_list(v_prime);
568 sys_.recycle(it_kripke, tid_);
569 }
570
571 if (todo_.back() == Rp_.back())
572 Rp_.pop_back();
573 todo_.pop_back();
574 }
575 finalize();
576 }
577
578 void setup()
579 {
580 tm_.start("DFS thread " + std::to_string(tid_));
581 }
582
583 void finalize()
584 {
585 bool tst_val = false;
586 bool new_val = true;
587 bool exchanged = stop_.compare_exchange_strong(tst_val, new_val);
588 if (exchanged)
589 finisher_ = true;
590 tm_.stop("DFS thread " + std::to_string(tid_));
591 }
592
593 bool finisher()
594 {
595 return finisher_;
596 }
597
598 unsigned states()
599 {
600 return states_;
601 }
602
603 unsigned transitions()
604 {
605 return transitions_;
606 }
607
608 unsigned walltime()
609 {
610 return tm_.timer("DFS thread " + std::to_string(tid_)).walltime();
611 }
612
613 std::string name()
614 {
615 return "bloemen_ec";
616 }
617
618 int sccs()
619 {
620 return sccs_;
621 }
622
623 mc_rvalue result()
624 {
625 return is_empty_ ? mc_rvalue::EMPTY : mc_rvalue::NOT_EMPTY;
626 }
627
628 std::string trace()
629 {
630 return "Not implemented";
631 }
632
633 private:
635 twacube_ptr twa_;
636 std::vector<uf_element*> todo_;
637 std::vector<uf_element*> Rp_;
639 unsigned tid_;
640 unsigned nb_th_;
641 unsigned inserted_ = 0;
642 unsigned states_ = 0;
643 unsigned transitions_ = 0;
644 unsigned sccs_ = 0;
645 bool is_empty_ = true;
646 spot::timer_map tm_;
647 std::atomic<bool>& stop_;
648 bool finisher_ = false;
649 };
650}
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_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:455
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:85
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.8