mirror of
https://github.com/Z3Prover/z3
synced 2025-04-11 03:33:35 +00:00
this one is for you Nuno
- pull request might have new bugs given that build is broken. - this test doesn't expose race conditions under simple tests, yet. It is a starting point. - run under cuzz (app-verifier) should expose races, this is what it was made for.
This commit is contained in:
parent
96e871c826
commit
0a7e003709
|
@ -1,9 +1,51 @@
|
|||
// test driver for scoped timer.
|
||||
// fixes are required to be fuzzed
|
||||
// with single and multi-threaded mode and short timeouts.
|
||||
// run it with app-verifier (becuzz yes ...)
|
||||
|
||||
#include "util/scoped_timer.h"
|
||||
#include "util/util.h"
|
||||
#include "util/vector.h"
|
||||
#include "util/trace.h"
|
||||
#include <thread>
|
||||
|
||||
class test_scoped_eh : public event_handler {
|
||||
std::atomic<bool> m_called = false;
|
||||
public:
|
||||
void operator()(event_handler_caller_t id) override {
|
||||
m_caller_id = id;
|
||||
m_called = true;
|
||||
}
|
||||
bool called() const { return m_called; }
|
||||
};
|
||||
|
||||
static void worker_thread(unsigned tid) {
|
||||
for (unsigned i = 0; i < 100; ++i) {
|
||||
test_scoped_eh eh;
|
||||
scoped_timer sc(1, &eh);
|
||||
unsigned_vector v;
|
||||
for (unsigned j = 0; j < (2 << 25); ++j) {
|
||||
v.push_back(j);
|
||||
if (eh.called()) {
|
||||
// IF_VERBOSE(0, verbose_stream() << tid << " " << i << " " << j << "\n");
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void tst_scoped_timer() {
|
||||
|
||||
std::cout << "sequential test\n";
|
||||
worker_thread(0);
|
||||
|
||||
std::cout << "thread test\n";
|
||||
unsigned num_threads = 3;
|
||||
vector<std::thread> threads(num_threads);
|
||||
for (unsigned i = 0; i < num_threads; ++i)
|
||||
threads[i] = std::thread([&, i]() { worker_thread(i); });
|
||||
|
||||
for (auto& th : threads)
|
||||
th.join();
|
||||
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue