From 4427d8f23a91ea3506559b3b64b8cb195cf93bb5 Mon Sep 17 00:00:00 2001 From: Jonas Oberhauser Date: Wed, 28 Feb 2024 10:57:08 +0100 Subject: [PATCH] Fix false positive liveness in executions blocked for reasons other than liveness When pruning redundant executions from the search space it can happen that some other thread is waiting for a store that would be sent by the pruning thread (doing e.g., assume(false)) if the pruning didn't happen. Since the execution should be ignored, we should not report liveness violations in such executions. --- src/GenMCDriver.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/GenMCDriver.cpp b/src/GenMCDriver.cpp index b511c55b8..bf91962ca 100644 --- a/src/GenMCDriver.cpp +++ b/src/GenMCDriver.cpp @@ -1400,6 +1400,8 @@ void GenMCDriver::checkLiveness() /* Collect all threads blocked at spinloops */ std::vector spinBlocked; for (auto i = 0U; i < g.getNumThreads(); i++) { + if (llvm::isa(g.getLastThreadLabel(i)) || llvm::isa(g.getLastThreadLabel(i)) || llvm::isa(g.getLastThreadLabel(i))) + return; if (llvm::isa(g.getLastThreadLabel(i))) spinBlocked.push_back(i); }