spot 2.10.6.dev
deadlock.hh
1// -*- coding: utf-8 -*-
2// Copyright (C) 2015, 2016, 2017, 2018, 2019, 2020 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 <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>
35
36namespace spot
37{
43 template<typename State, typename SuccIterator,
44 typename StateHash, typename StateEqual,
45 typename Deadlock>
46 class SPOT_API swarmed_deadlock
47 {
49 enum st_status
50 {
51 UNKNOWN = 1, // First time this state is discoverd by this thread
52 OPEN = 2, // The state is currently processed by this thread
53 CLOSED = 4, // All the successors of this state have been visited
54 };
55
57 struct deadlock_pair
58 {
59 State st;
60 int* colors;
61 };
62
64 struct pair_hasher
65 {
66 pair_hasher(const deadlock_pair*)
67 { }
68
69 pair_hasher() = default;
70
71 brick::hash::hash128_t
72 hash(const deadlock_pair* lhs) const
73 {
74 StateHash hash;
75 // Not modulo 31 according to brick::hashset specifications.
76 unsigned u = hash(lhs->st) % (1<<30);
77 return {u, u};
78 }
79
80 bool equal(const deadlock_pair* lhs,
81 const deadlock_pair* rhs) const
82 {
83 StateEqual equal;
84 return equal(lhs->st, rhs->st);
85 }
86 };
87
88 static constexpr bool compute_deadlock =
89 std::is_same<std::true_type, Deadlock>::value;
90
91 public:
92
94 using shared_map = brick::hashset::FastConcurrent <deadlock_pair*,
95 pair_hasher>;
96 using shared_struct = shared_map;
97
98 static shared_struct* make_shared_structure(shared_map, unsigned)
99 {
100 return nullptr; // Useless
101 }
102
104 twacube_ptr, /* useless here */
105 shared_map& map, shared_struct* /* useless here */,
106 unsigned tid,
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)),
112 stop_(stop)
113 {
114 static_assert(spot::is_a_kripkecube_ptr<decltype(&sys),
115 State, SuccIterator>::value,
116 "error: does not match the kripkecube requirements");
117 SPOT_ASSERT(nb_th_ > tid);
118 }
119
120 virtual ~swarmed_deadlock()
121 {
122 while (!todo_.empty())
123 {
124 sys_.recycle(todo_.back().it, tid_);
125 todo_.pop_back();
126 }
127 }
128
129 void run()
130 {
131 setup();
132 State initial = sys_.initial(tid_);
133 if (SPOT_LIKELY(push(initial)))
134 {
135 todo_.push_back({initial, sys_.succ(initial, tid_), transitions_});
136 }
137 while (!todo_.empty() && !stop_.load(std::memory_order_relaxed))
138 {
139 if (todo_.back().it->done())
140 {
141 if (SPOT_LIKELY(pop()))
142 {
143 deadlock_ = todo_.back().current_tr == transitions_;
144 if (compute_deadlock && deadlock_)
145 break;
146 sys_.recycle(todo_.back().it, tid_);
147 todo_.pop_back();
148 }
149 }
150 else
151 {
152 ++transitions_;
153 State dst = todo_.back().it->state();
154
155 if (SPOT_LIKELY(push(dst)))
156 {
157 todo_.back().it->next();
158 todo_.push_back({dst, sys_.succ(dst, tid_), transitions_});
159 }
160 else
161 {
162 todo_.back().it->next();
163 }
164 }
165 }
166 finalize();
167 }
168
169 void setup()
170 {
171 tm_.start("DFS thread " + std::to_string(tid_));
172 }
173
174 bool push(State s)
175 {
176 // Prepare data for a newer allocation
177 int* ref = (int*) p_.allocate();
178 for (unsigned i = 0; i < nb_th_; ++i)
179 ref[i] = UNKNOWN;
180
181 // Try to insert the new state in the shared map.
182 deadlock_pair* v = (deadlock_pair*) p_pair_.allocate();
183 v->st = s;
184 v->colors = ref;
185 auto it = map_.insert(v);
186 bool b = it.isnew();
187
188 // Insertion failed, delete element
189 // FIXME Should we add a local cache to avoid useless allocations?
190 if (!b)
191 p_.deallocate(ref);
192
193 // The state has been mark dead by another thread
194 for (unsigned i = 0; !b && i < nb_th_; ++i)
195 if ((*it)->colors[i] == static_cast<int>(CLOSED))
196 return false;
197
198 // The state has already been visited by the current thread
199 if ((*it)->colors[tid_] == static_cast<int>(OPEN))
200 return false;
201
202 // Keep a ptr over the array of colors
203 refs_.push_back((*it)->colors);
204
205 // Mark state as visited.
206 (*it)->colors[tid_] = OPEN;
207 ++states_;
208 return true;
209 }
210
211 bool pop()
212 {
213 // Track maximum dfs size
214 dfs_ = todo_.size() > dfs_ ? todo_.size() : dfs_;
215
216 // Don't avoid pop but modify the status of the state
217 // during backtrack
218 refs_.back()[tid_] = CLOSED;
219 refs_.pop_back();
220 return true;
221 }
222
223 void finalize()
224 {
225 bool tst_val = false;
226 bool new_val = true;
227 bool exchanged = stop_.compare_exchange_strong(tst_val, new_val);
228 if (exchanged)
229 finisher_ = true;
230 tm_.stop("DFS thread " + std::to_string(tid_));
231 }
232
233 bool finisher()
234 {
235 return finisher_;
236 }
237
238 unsigned states()
239 {
240 return states_;
241 }
242
243 unsigned transitions()
244 {
245 return transitions_;
246 }
247
248 unsigned walltime()
249 {
250 return tm_.timer("DFS thread " + std::to_string(tid_)).walltime();
251 }
252
253 std::string name()
254 {
255 if (compute_deadlock)
256 return "deadlock";
257 return "reachability";
258 }
259
260 int sccs()
261 {
262 return -1;
263 }
264
265 mc_rvalue result()
266 {
267 if (compute_deadlock)
268 return deadlock_ ? mc_rvalue::DEADLOCK : mc_rvalue::NO_DEADLOCK;
269 return mc_rvalue::SUCCESS;
270 }
271
272 std::string trace()
273 {
274 std::string result;
275 for (auto& e: todo_)
276 result += sys_.to_string(e.s, tid_);
277 return result;
278 }
279
280 private:
281 struct todo_element
282 {
283 State s;
284 SuccIterator* it;
285 unsigned current_tr;
286 };
287 kripkecube<State, SuccIterator>& sys_;
288 std::vector<todo_element> todo_;
289 unsigned transitions_ = 0;
290 unsigned tid_;
291 shared_map map_;
292 spot::timer_map tm_;
293 unsigned states_ = 0;
294 unsigned dfs_ = 0;
296 unsigned nb_th_ = 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;
305 };
306}
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.

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