24 #include <spot/bricks/brick-hashset>
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/mc.hh>
43 template<
typename State,
typename SuccIterator,
44 typename StateHash,
typename StateEqual,
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)
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;
This class allows to ensure (at compile time) if a given parameter is of type kripkecube....
Definition: kripke.hh:72
This class is a template representation of a Kripke structure. It is composed of two template paramet...
Definition: kripke.hh:41
This class aims to explore a model to detect wether it contains a deadlock. This deadlock detection p...
Definition: deadlock.hh:47
brick::hashset::FastConcurrent< deadlock_pair *, pair_hasher > shared_map
<
Definition: deadlock.hh:95
A map of timer, where each timer has a name.
Definition: timer.hh:229
Definition: automata.hh:27
mc_rvalue
Definition: mc.hh:44
@ NO_DEADLOCK
No deadlock has been found.
@ DEADLOCK
A deadlock has been found.
@ SUCCESS
The Algorithm finished normally.