Fix commit dfe4e77: check hasWaiters() in Enqueue

 * We were checking hasWaiters() in MCCondWait, and if no waiters,
   we set the mutex to NULL, associated with that condition variable.
   That corrupted the stack.  We now check in MCCondEnqueue that if
   hasWaiters() is true, then the old mutex associated with the
   condition variable is the same as the new mutex being associated with it.

Author: gc00

NEWS

@@ -1,3 +1,8 @@
+Version 1.2.0 release notes (DATE: TBD)
+==========================================
+* A long-standing bug affecting condition variables was removed.
+* The experimental livelock support was improved using a new heuristic.
+
 Version 1.1.0 release notes (Oct. 7, 2025)
 ==========================================
 

src/transitions/cond/MCCondEnqueue.cpp

@@ -177,6 +177,19 @@ MCCondEnqueue::dynamicCopyInState(const MCStack *state) const
 void
 MCCondEnqueue::applyToState(MCStack *state)
 {
+  // POSIX standard says that the dynamic binding of a condition variable
+  // to a mutex is removed when the last thread waiting on that cond var is
+  // unblocked (i.e., has re-acquired the associated mutex of the cond var).
+  if (this->conditionVariable->hasWaiters() &&
+      this->conditionVariable->mutex != this->mutex) {
+    mcprintf("\n*** ERROR (pthread_cond_wait/traceId: %d):\n"
+             "*** pthread_cond_wait() was called with a new mutex,\n"
+             "***   even though a different thread had called\n"
+             "***   pthread_cond_wait() on a different mutex and that thread\n"
+             "***   was still waiting on this same condition variable.\n",
+             traceId);
+    mc_stop_model_checking(EXIT_FAILURE);
+  }
   /* Insert this thread into the waiting queue */
   this->conditionVariable->addWaiter(this->getThreadId());
   this->conditionVariable->mutex = this->mutex;

src/transitions/cond/MCCondWait.cpp

@@ -79,12 +79,6 @@ MCCondWait::applyToState(MCStack *state)
   const tid_t threadId = this->getThreadId();
   this->conditionVariable->mutex->lock(threadId);
   this->conditionVariable->removeWaiter(threadId);
-  // POSIX standard says that the dynamic binding of a condition variable
-  // to a mutex is removed when the last thread waiting on that cond var is
-  // unblocked (i.e., has re-acquired the associated mutex of the cond var).
-  if (! this->conditionVariable->hasWaiters()) {
-    this->conditionVariable->mutex = nullptr;
-  }
 }
 
 bool