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
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_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 deallocate(void *ptr)
Recycle size bytes of memory.
Definition: fixpool.hh:132
void * allocate()
Allocate size bytes of memory.
Definition: fixpool.hh:88
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.4