Commit 030733a7 authored by Etienne Renault's avatar Etienne Renault

WIP Ugly but working for two threads

parent 29aab0b3
Pipeline #19272 failed with stage
in 16 minutes and 45 seconds
...@@ -151,6 +151,8 @@ namespace spot ...@@ -151,6 +151,8 @@ namespace spot
cspins_state state() const; cspins_state state() const;
cube condition() const; cube condition() const;
void reset () { current_ = 0;}
private: private:
/// \brief Compute the real index in the successor vector /// \brief Compute the real index in the successor vector
unsigned compute_index() const; unsigned compute_index() const;
......
...@@ -49,6 +49,12 @@ namespace spot ...@@ -49,6 +49,12 @@ namespace spot
: st(initial) : st(initial)
{ } { }
~deadlock_state()
{
//std::cout << "~deadlock" << st << '\n';
// delete[] st;
}
deadlock_state() = default; deadlock_state() = default;
bool operator==(const deadlock_state& other) const bool operator==(const deadlock_state& other) const
...@@ -100,13 +106,24 @@ namespace spot ...@@ -100,13 +106,24 @@ namespace spot
bool push(deadlock_state& s) bool push(deadlock_state& s)
{ {
auto it = map_.insert(s.st, brick_state_hasher());
if (!it.isnew()) // COMMENT Do not insert systematically. If a state
return false; // A is in the bloom filter the state will nonetheless
if (bloom_filter_.contains(state_hash_(s.st))) // be inserted...
return false; // auto it = map_.insert(s.st, brick_state_hasher());
++states_; // Check first if the state is already in either the map
return true; // or the bloom filter.
auto it = map_.find(s.st, brick_state_hasher());
if (!it.valid())
{
auto it = map_.insert(s.st, brick_state_hasher());
++states_;
return true;
}
// if (bloom_filter_.contains(state_hash_(s.st)))
// return false;
return false;
} }
void pop() void pop()
...@@ -120,16 +137,74 @@ namespace spot ...@@ -120,16 +137,74 @@ namespace spot
//if (SPOT_UNLIKELY(deadlock_)) //if (SPOT_UNLIKELY(deadlock_))
// return; // return;
map_.erase(elem.st, brick_state_hasher()); std::cout << "ERASE\n";
auto st = elem.st.st;
// COMMENT: insert first in bloom_filter to avoid inconsistencies.
bloom_filter_.insert(state_hash_(elem.st.st)); bloom_filter_.insert(state_hash_(elem.st.st));
// bool b = map_.erase(elem.st, brick_state_hasher());
// std::cout << "Yuhu" << b << std::endl;
// COMMENT: invalid read comes from here (only in multithreaded
// computation) Why that?
// probably because
// - thread 1 inserts A
// - thread 2 check wether or not A is already inserted
// - during this time thread 1 decide to delete A
// Even if brick hash_table support simultaneous insert/delete operation
// these operation are OK only for elements in the hash table not for
// references handled by these element.
// delete[] st; <---- invalid read.
// How to wait that the element is no longer accessed?
{
bool b = map_.erase(st, brick_state_hasher());
auto it2 = map_.find(st, brick_state_hasher());
int nb = map_.count(st, brick_state_hasher());
std::cout << "Yuhu" << b << " "
<< nb << " "
<< it2.valid()
<< it2.isnew()
<< std::endl;
// PROBLEM HERE
// Ugly how can we resolve that?
std::this_thread::sleep_for(std::chrono::milliseconds(200));
it2 = map_.find(st, brick_state_hasher());
nb = map_.count(st, brick_state_hasher());
std::cout << "Yuhu" << b << " "
<< nb << " "
<< it2.valid()
<< it2.isnew()
<< std::endl;
delete[] st;
}
auto& it = elem.it; auto& it = elem.it;
// COMMENT: Here you have to reset the iterator, otherwise, and since
// you use it elsewhere, you may miss some state to delete.
it->reset();
while (!it->done()) while (!it->done())
{ {
delete[] it->state(); delete[] it->state(); // Probably same problem as above
it->next(); it->next();
} }
delete it; delete it;
todo_.pop_back(); todo_.pop_back();
} }
...@@ -141,17 +216,17 @@ namespace spot ...@@ -141,17 +216,17 @@ namespace spot
void dealloc() void dealloc()
{ {
while (!todo_.empty()) // while (!todo_.empty())
{ // {
auto& it = todo_.back().it; // auto& it = todo_.back().it;
while (!it->done()) // while (!it->done())
{ // {
delete[] it->state(); // delete[] it->state();
it->next(); // it->next();
} // }
delete it; // delete it;
todo_.pop_back(); // todo_.pop_back();
} // }
} }
unsigned states() unsigned states()
...@@ -171,31 +246,34 @@ namespace spot ...@@ -171,31 +246,34 @@ namespace spot
auto it = sys_.succ(initial.st, tid_); auto it = sys_.succ(initial.st, tid_);
if (SPOT_LIKELY(push(initial))) if (SPOT_LIKELY(push(initial)))
todo_.push_back({initial, it, transitions_}); todo_.push_back({initial, it, transitions_});
pop();
while (!todo_.empty() && !stop_.load(std::memory_order_relaxed))
{
if (todo_.back().it->done()) // // while (!todo_.empty() && !stop_.load(std::memory_order_relaxed))
{ // {
pop(); // // if (todo_.back().it->done())
if (deadlock_) // // {
break; // // pop();
} // // // if (deadlock_)
else // // // break;
{ // // }
++transitions_; // // else
State dst = todo_.back().it->state(); // {
deadlock_state next{dst}; // ++transitions_;
// State dst = todo_.back().it->state();
if (SPOT_LIKELY(push(next))) // deadlock_state next{dst};
todo_.push_back({next, sys_.succ(dst, tid_), transitions_});
else // if (SPOT_LIKELY(push(next)))
delete[] todo_.back().it->state(); // todo_.push_back({next, sys_.succ(dst, tid_), transitions_});
// // else
todo_.back().it->next(); // // delete[] todo_.back().it->state();
}
}
// // todo_.back().it->next();
delete[] initial.st; // }
//}
//delete[] initial.st;
finalize(); finalize();
} }
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment