Fix commit dfe4e77b: check hasWaiters() in Enqueue

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

@@ -135,6 +135,18 @@ MCReadCondEnqueue(const MCSharedTransition *shmTransition,
       "the first mutex.");
   }
 
+  // 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 (condThatExists->hasWaiters() && condThatExists->mutex != nullptr) {
+    MC_REPORT_UNDEFINED_BEHAVIOR_ON_FAIL(
+      *condThatExists->mutex == *mutexThatExists,
+      "There were still threads waiting on a previous mutex associated\n"
+      "with this condition variable.  Attempting to associate more than one\n"
+      "mutex with a condition variable is undefined behavior. Ensure that\n"
+      "you're calling pthread_cond_wait() with the same mutex.");
+  }
+
   // NOTE: We have to associate the mutex with the condition
   // variable when the transition is encountered; otherwise,
   // we wouldn't be able to determine if, e.g., a pthread_cond_wait()

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

test/invalid_thread_op_arg_program/condvar-two-mutexes.c

@@ -0,0 +1,96 @@
+#include <assert.h>
+#include <stdio.h>
+#include <stdlib.h>
+#include <pthread.h>
+#include <unistd.h> 
+
+#define NUM_WRITERS 3
+#define ITERATIONS 1
+
+int shared_data = 0; 
+int writer_count_db1 = 0;
+int writer_count_db2 = 0;
+int waiting_writer_count_db1 = 0;
+int waiting_writer_count_db2 = 0;
+pthread_mutex_t mutex_lock_db1; 
+pthread_mutex_t mutex_lock_db2; 
+// One condition variable, but two mutexes
+pthread_cond_t writers_cond; 
+
+void *writer(void *not_used) {
+  for (int i = 0; i < ITERATIONS; i++) {
+    // We're doing two acquire-release paradigms,
+    //   but with one condition variable and two mutexes.
+    //   This is a bug.
+
+    // ACQUIRE for db1
+    pthread_mutex_lock(&mutex_lock_db1);
+    waiting_writer_count_db1++;
+    while (writer_count_db1 > 0) {
+      pthread_cond_wait(&writers_cond, &mutex_lock_db1);
+    }
+    waiting_writer_count_db1--;
+    assert(writer_count_db1 == 0);
+    writer_count_db1++;
+    pthread_mutex_unlock(&mutex_lock_db1);
+    // USE (DO_TASK) for db1
+    shared_data++;
+    usleep(200000);
+    printf("I wrote to db #1\n"); 
+    // RELEASE for db1
+    pthread_mutex_lock(&mutex_lock_db1);
+    writer_count_db1--;
+    assert(writer_count_db1 == 0);
+    if (waiting_writer_count_db1 > 0) {
+      pthread_cond_signal(&writers_cond); 
+    }
+    pthread_mutex_unlock(&mutex_lock_db1);
+    usleep(500000); 
+
+    // ACQUIRE for db2
+    pthread_mutex_lock(&mutex_lock_db2);
+    waiting_writer_count_db2++;
+    while (writer_count_db2 > 0) {
+      pthread_cond_wait(&writers_cond, &mutex_lock_db2);
+    }
+    waiting_writer_count_db2--;
+    assert(writer_count_db2 == 0);
+    writer_count_db2++;
+    pthread_mutex_unlock(&mutex_lock_db2);
+    // USE (DO_TASK) for db2
+    shared_data++;
+    usleep(200000);
+    printf("I wrote to db #2\n"); 
+    // RELEASE for db2
+    pthread_mutex_lock(&mutex_lock_db2);
+    writer_count_db2--;
+    assert(writer_count_db2 == 0);
+    if (waiting_writer_count_db2 > 0) {
+      pthread_cond_signal(&writers_cond); 
+    }
+    pthread_mutex_unlock(&mutex_lock_db2);
+    usleep(500000); 
+  }
+  return NULL;
+}
+
+int main() {
+  pthread_t writers[NUM_WRITERS];
+  int writer_ids[NUM_WRITERS];
+  pthread_mutex_init(&mutex_lock_db1, NULL);
+  pthread_mutex_init(&mutex_lock_db2, NULL);
+  pthread_cond_init(&writers_cond, NULL);
+  for (int i = 0; i < NUM_WRITERS; i++) {
+    writer_ids[i] = i + 1;
+    if (pthread_create(&writers[i], NULL, writer, &writer_ids[i]) != 0) {
+      return 1;
+    }
+  }
+  for (int i = 0; i < NUM_WRITERS; i++) {
+    pthread_join(writers[i], NULL);
+  }
+  pthread_mutex_destroy(&mutex_lock_db1);
+  pthread_mutex_destroy(&mutex_lock_db2);
+  pthread_cond_destroy(&writers_cond);
+  return 0;
+}