From 7ae1a338a7917c3dd944aa09e222b818c895c281 Mon Sep 17 00:00:00 2001 From: Anthony Romano Date: Mon, 11 Jul 2022 09:26:11 -0700 Subject: [PATCH] parallel-tactic: fix deadlocking race between shutdown and get_task (#6152) 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 --- src/solver/parallel_tactic.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/solver/parallel_tactic.cpp b/src/solver/parallel_tactic.cpp index c79f52084..1d24ed1e6 100644 --- a/src/solver/parallel_tactic.cpp +++ b/src/solver/parallel_tactic.cpp @@ -113,9 +113,9 @@ class parallel_tactic : public tactic { void shutdown() { if (!m_shutdown) { + std::lock_guard lock(m_mutex); m_shutdown = true; m_cond.notify_all(); - std::lock_guard lock(m_mutex); for (solver_state* st : m_active) { st->m().limit().cancel(); } @@ -147,7 +147,9 @@ class parallel_tactic : public tactic { } { std::unique_lock lock(m_mutex); - m_cond.wait(lock); + if (!m_shutdown) { + m_cond.wait(lock); + } } dec_wait(); }