mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 12:58:44 +00:00
Code Activity

parallel-tactic: fix deadlocking race between shutdown and get_task (#6152)

Browse source 
Deadlock/Race is as follows:
  1. get_task() reads m_shutdown == false and enters loop body
  2. shutdown() is called; sets m_shutdown = true
  3. shutdown() calls m_cond.notify_all()
  4. get_task() finds no task in try_get_task()
  5. get_task() calls m_cond.wait(), missing the notification
  6. solve() waits forever on join()

Provided patch wraps (2) and (3) with the condition variable lock so that
step (5) cannot miss the notification.

Co-authored-by: Anthony Romano <anthony@forallsecure.com>
This commit is contained in:
Anthony Romano 2022-07-11 09:26:11 -07:00 committed by GitHub
parent 99212a2726
commit 7ae1a338a7
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 4 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/solver/parallel_tactic.cpp
View file

@ -113,9 +113,9 @@ class parallel_tactic : public tactic {
void shutdown() { void shutdown() {
if (!m_shutdown) { if (!m_shutdown) {
std::lock_guard<std::mutex> lock(m_mutex);
m_shutdown = true; m_shutdown = true;
m_cond.notify_all(); m_cond.notify_all();
std::lock_guard<std::mutex> lock(m_mutex);
for (solver_state* st : m_active) { for (solver_state* st : m_active) {
st->m().limit().cancel(); st->m().limit().cancel();
} }
@ -147,8 +147,10 @@ class parallel_tactic : public tactic {
} }
{ {
std::unique_lock<std::mutex> lock(m_mutex); std::unique_lock<std::mutex> lock(m_mutex);
if (!m_shutdown) {
m_cond.wait(lock); m_cond.wait(lock);
} }
}
dec_wait(); dec_wait();
} }
return nullptr; return nullptr;