65 pair_hasher(
const deadlock_pair*)
68 pair_hasher() =
default;
70 brick::hash::hash128_t
71 hash(
const deadlock_pair* lhs)
const
75 unsigned u = hash(lhs->st) % (1<<30);
79 bool equal(
const deadlock_pair* lhs,
80 const deadlock_pair* rhs)
const
83 return equal(lhs->st, rhs->st);
87 static constexpr bool compute_deadlock =
88 std::is_same<std::true_type, Deadlock>::value;
93 using shared_map = brick::hashset::FastConcurrent <deadlock_pair*,
97 static shared_struct* make_shared_structure(
shared_map,
unsigned)
104 shared_map& map, shared_struct* ,
106 std::atomic<bool>& stop):
107 sys_(sys), tid_(tid), map_(map),
108 nb_th_(std::thread::hardware_concurrency()),
109 p_(sizeof(int)*std::thread::hardware_concurrency()),
110 p_pair_(sizeof(deadlock_pair)),
114 State, SuccIterator>::value,
115 "error: does not match the kripkecube requirements");
116 SPOT_ASSERT(nb_th_ > tid);
119 virtual ~swarmed_deadlock()
121 while (!todo_.empty())
123 sys_.recycle(todo_.back().it, tid_);
131 State initial = sys_.initial(tid_);
132 if (SPOT_LIKELY(push(initial)))
134 todo_.push_back({initial, sys_.succ(initial, tid_), transitions_});
136 while (!todo_.empty() && !stop_.load(std::memory_order_relaxed))
138 if (todo_.back().it->done())
140 if (SPOT_LIKELY(pop()))
142 deadlock_ = todo_.back().current_tr == transitions_;
143 if (compute_deadlock && deadlock_)
145 sys_.recycle(todo_.back().it, tid_);
152 State dst = todo_.back().it->state();
154 if (SPOT_LIKELY(push(dst)))
156 todo_.back().it->next();
157 todo_.push_back({dst, sys_.succ(dst, tid_), transitions_});
161 todo_.back().it->next();
170 tm_.start(
"DFS thread " + std::to_string(tid_));
176 int* ref = (
int*) p_.allocate();
177 for (
unsigned i = 0; i < nb_th_; ++i)
181 deadlock_pair* v = (deadlock_pair*) p_pair_.allocate();
184 auto it = map_.insert(v);
193 for (
unsigned i = 0; !b && i < nb_th_; ++i)
194 if ((*it)->colors[i] ==
static_cast<int>(CLOSED))
198 if ((*it)->colors[tid_] ==
static_cast<int>(OPEN))
202 refs_.push_back((*it)->colors);
205 (*it)->colors[tid_] = OPEN;
213 dfs_ = todo_.size() > dfs_ ? todo_.size() : dfs_;
217 refs_.back()[tid_] = CLOSED;
224 bool tst_val =
false;
226 bool exchanged = stop_.compare_exchange_strong(tst_val, new_val);
229 tm_.stop(
"DFS thread " + std::to_string(tid_));
242 unsigned transitions()
249 return tm_.timer(
"DFS thread " + std::to_string(tid_)).walltime();
254 if (compute_deadlock)
256 return "reachability";
266 if (compute_deadlock)
267 return deadlock_ ? mc_rvalue::DEADLOCK : mc_rvalue::NO_DEADLOCK;
268 return mc_rvalue::SUCCESS;
275 result += sys_.to_string(e.s, tid_);
286 kripkecube<State, SuccIterator>& sys_;
287 std::vector<todo_element> todo_;
288 unsigned transitions_ = 0;
292 unsigned states_ = 0;
296 fixed_size_pool<pool_type::Unsafe> p_;
297 fixed_size_pool<pool_type::Unsafe> p_pair_;
298 bool deadlock_ =
false;
299 std::atomic<bool>& stop_;
302 std::vector<int*> refs_;
303 bool finisher_ =
false;