mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 02:15:19 +00:00
fix race condition in cooperate
This commit is contained in:
parent
6a0708fc8e
commit
37882f5afa
|
@ -17,24 +17,17 @@ Notes:
|
|||
|
||||
--*/
|
||||
|
||||
#ifndef SINGLE_THREAD
|
||||
|
||||
#include "util/cooperate.h"
|
||||
#include "util/trace.h"
|
||||
#include "util/debug.h"
|
||||
#include <thread>
|
||||
#include <atomic>
|
||||
#include <mutex>
|
||||
#include <thread>
|
||||
|
||||
struct cooperation_lock {
|
||||
std::recursive_mutex m_lock;
|
||||
char const * m_task;
|
||||
std::thread::id m_owner_thread;
|
||||
cooperation_lock() {
|
||||
m_task = nullptr;
|
||||
}
|
||||
~cooperation_lock() {
|
||||
}
|
||||
};
|
||||
|
||||
static cooperation_lock g_lock;
|
||||
static std::mutex lock;
|
||||
static std::atomic<std::thread::id> owner_thread;
|
||||
|
||||
bool cooperation_ctx::g_cooperate = false;
|
||||
|
||||
|
@ -42,17 +35,17 @@ void cooperation_ctx::checkpoint(char const * task) {
|
|||
SASSERT(cooperation_ctx::enabled());
|
||||
|
||||
std::thread::id tid = std::this_thread::get_id();
|
||||
if (g_lock.m_owner_thread == tid) {
|
||||
g_lock.m_owner_thread = std::thread::id();
|
||||
g_lock.m_lock.unlock();
|
||||
if (owner_thread == tid) {
|
||||
owner_thread = std::thread::id();
|
||||
lock.unlock();
|
||||
}
|
||||
|
||||
// this critical section is used to force the owner thread to give a chance to
|
||||
// another thread to get the lock
|
||||
std::this_thread::yield();
|
||||
g_lock.m_lock.lock();
|
||||
lock.lock();
|
||||
TRACE("cooperate_detail", tout << task << ", tid: " << tid << "\n";);
|
||||
CTRACE("cooperate", g_lock.m_task != task, tout << "moving to task: " << task << "\n";);
|
||||
g_lock.m_owner_thread = tid;
|
||||
owner_thread = tid;
|
||||
}
|
||||
|
||||
#endif
|
||||
|
|
|
@ -16,10 +16,9 @@ Author:
|
|||
Notes:
|
||||
|
||||
--*/
|
||||
#ifndef COOPERATE_H_
|
||||
#define COOPERATE_H_
|
||||
#pragma once
|
||||
|
||||
#ifndef _NO_OMP_
|
||||
#ifndef SINGLE_THREAD
|
||||
|
||||
class cooperation_ctx {
|
||||
static bool g_cooperate;
|
||||
|
@ -35,5 +34,3 @@ inline void cooperate(char const * task) {
|
|||
#else
|
||||
inline void cooperate(char const *) {}
|
||||
#endif
|
||||
|
||||
#endif
|
||||
|
|
Loading…
Reference in a new issue