66 pair_hasher(
const deadlock_pair*)
69 pair_hasher() =
default;
71 brick::hash::hash128_t
72 hash(
const deadlock_pair* lhs)
const
76 unsigned u = hash(lhs->st) % (1<<30);
80 bool equal(
const deadlock_pair* lhs,
81 const deadlock_pair* rhs)
const
84 return equal(lhs->st, rhs->st);
88 static constexpr bool compute_deadlock =
89 std::is_same<std::true_type, Deadlock>::value;
94 using shared_map = brick::hashset::FastConcurrent <deadlock_pair*,
98 static shared_struct* make_shared_structure(
shared_map,
unsigned)
105 shared_map& map, shared_struct* ,
107 std::atomic<bool>& stop):
108 sys_(sys), tid_(tid), map_(map),
109 nb_th_(std::thread::hardware_concurrency()),
110 p_(sizeof(int)*std::thread::hardware_concurrency()),
111 p_pair_(sizeof(deadlock_pair)),
115 State, SuccIterator>::value,
116 "error: does not match the kripkecube requirements");
117 SPOT_ASSERT(nb_th_ > tid);
120 virtual ~swarmed_deadlock()
122 while (!todo_.empty())
124 sys_.recycle(todo_.back().it, tid_);
132 State initial = sys_.initial(tid_);
133 if (SPOT_LIKELY(push(initial)))
135 todo_.push_back({initial, sys_.succ(initial, tid_), transitions_});
137 while (!todo_.empty() && !stop_.load(std::memory_order_relaxed))
139 if (todo_.back().it->done())
141 if (SPOT_LIKELY(pop()))
143 deadlock_ = todo_.back().current_tr == transitions_;
144 if (compute_deadlock && deadlock_)
146 sys_.recycle(todo_.back().it, tid_);
153 State dst = todo_.back().it->state();
155 if (SPOT_LIKELY(push(dst)))
157 todo_.back().it->next();
158 todo_.push_back({dst, sys_.succ(dst, tid_), transitions_});
162 todo_.back().it->next();
171 tm_.start(
"DFS thread " + std::to_string(tid_));
177 int* ref = (
int*) p_.allocate();
178 for (
unsigned i = 0; i < nb_th_; ++i)
182 deadlock_pair* v = (deadlock_pair*) p_pair_.allocate();
185 auto it = map_.insert(v);
194 for (
unsigned i = 0; !b && i < nb_th_; ++i)
195 if ((*it)->colors[i] ==
static_cast<int>(CLOSED))
199 if ((*it)->colors[tid_] ==
static_cast<int>(OPEN))
203 refs_.push_back((*it)->colors);
206 (*it)->colors[tid_] = OPEN;
214 dfs_ = todo_.size() > dfs_ ? todo_.size() : dfs_;
218 refs_.back()[tid_] = CLOSED;
225 bool tst_val =
false;
227 bool exchanged = stop_.compare_exchange_strong(tst_val, new_val);
230 tm_.stop(
"DFS thread " + std::to_string(tid_));
243 unsigned transitions()
250 return tm_.timer(
"DFS thread " + std::to_string(tid_)).walltime();
255 if (compute_deadlock)
257 return "reachability";
267 if (compute_deadlock)
268 return deadlock_ ? mc_rvalue::DEADLOCK : mc_rvalue::NO_DEADLOCK;
269 return mc_rvalue::SUCCESS;
276 result += sys_.to_string(e.s, tid_);
287 kripkecube<State, SuccIterator>& sys_;
288 std::vector<todo_element> todo_;
289 unsigned transitions_ = 0;
293 unsigned states_ = 0;
297 fixed_size_pool<pool_type::Unsafe> p_;
298 fixed_size_pool<pool_type::Unsafe> p_pair_;
299 bool deadlock_ =
false;
300 std::atomic<bool>& stop_;
303 std::vector<int*> refs_;
304 bool finisher_ =
false;