Improve mc_report_undefined_behavior_on_fail with correct PENDING TRANSITIONS

NEWS

@@ -1,3 +1,7 @@
+Version 1.2.0 release notes (DATE: TBD)
+==========================================
+* Improved error msg when there is an invalid argument used in a thread operation.  The last transition in the stack was previously being omitted.
+
 Version 1.1.0 release notes (Oct. 7, 2025)
 ==========================================
 

src/MCStack.cpp

@@ -923,19 +923,36 @@ MCStack::simulateRunningTransition(
   const MCTransition &transition,
   MCSharedTransition *shmTransitionTypeInfo, void *shmTransitionData)
 {
-  // NOTE: You must grow the transition stack before
-  // the state stack for clock vector updates
-  // to occur properly
+  // The target process has just executed 'transition'.  Recall that a
+  // transition executes one visible operation (e.g., thread operation),
+  // followed by invisible operations, until the next visible operation.
+  // This function will update the model to reflect this transition.
+
+  // 1. Add this transition to the transition stack of the model.
+  // NOTE: You must grow the transition stack before the state stack for
+  //   clock vector updates to occur properly.
   this->growTransitionStackRunning(transition);
   this->growStateStackRunningTransition(transition);
 
-  // NOTE: After applying the transition, this `MCStack`
-  // object has moved into the NEXT state, meaning that
-  // e.g. asking the question "which threads are enabled
-  // now" would ultimate be being asked about the state
-  // that follows AFTER `transition` is executed
+  // 2. Add this transition to the transition stack of the model.
+  // NOTE: After applying the transition, this `MCStack` transition
+  //   object has moved into the NEXT state, meaning that, for example,
+  //   asking the question "which threads are enabled now" would ultimately
+  //   be asked about the state that follows AFTER `transition` is executed.
   this->virtuallyRunTransition(transition);
 
+  // 3. The next transition for tid must now be added to the model.
+  //    The target process had stopped before this next transition.
+  //    So, setNextTransition will look at the shared memory data
+  //    that communicates between  model and target process.
+  //    It will then call MCReadXXX, for XXX being the
+  //    next transition.  The model then saves this next transition,
+  //    so that later, the model checker can decide which threads
+  //    have a next transition that is enabled.
+  // NOTE: The function MCReadXXX may decide that the arguments
+  //   are invalid.  (See mc_report_undefined_behavior().)  If so,
+  //   MCReadXXX must itself call setNextTransitionForThread(), so that
+  //   "PENDING TRANSITIONS" will be displayed properly to the user.
   tid_t tid = transition.getThreadId();
   this->setNextTransitionForThread(tid, shmTransitionTypeInfo,
                                    shmTransitionData);

src/mcmini_private.cpp

@@ -829,6 +829,10 @@ mc_report_undefined_behavior(const char *msg)
           traceId, msg);
   programState->printTransitionStack();
   programState->printNextTransitions();
+  fprintf(stderr,
+        "*****************************************************************\n"
+        "*** SEE MESSAGE, ABOVE, FOR DESCRIPTION OF UNDEFINED BEHAVIOR ***\n"
+        "*****************************************************************\n");
   mc_exit(EXIT_FAILURE);
 }
 

src/transitions/cond/MCCondEnqueue.cpp

@@ -100,51 +100,92 @@ MCReadCondEnqueue(const MCSharedTransition *shmTransition,
          condThatExists -> shadow.state ==
            MCConditionVariable::Shadow::destroyed);
 
-  MC_REPORT_UNDEFINED_BEHAVIOR_ON_FAIL(
-    mutexThatExists->isLocked(),
-    "Attempting to wait on a condition variable with a mutex that is unlocked.");
+  // 1. We've now computed condThatExists and mutexThatExists
+  //    (i.e., the state of the condvar and mutex arguments to
+  //    pthread_cond_wait()).  Compute the nextTransition.
+  const tid_t threadThatRanId  = shmTransition->executor;
+  auto threadThatRan           = state->getThreadWithId(threadThatRanId);
+  MCTransition *nextTransition =
+    new MCCondEnqueue(threadThatRan, condThatExists, mutexThatExists);
 
-  MC_REPORT_UNDEFINED_BEHAVIOR_ON_FAIL(
-    !condThatExists->isDestroyed(),
-    "Attempting to wait on a destroyed condition variable.");
-
-  if (condThatExists->mutex != nullptr) {
-    MC_REPORT_UNDEFINED_BEHAVIOR_ON_FAIL(
-      *condThatExists->mutex == *mutexThatExists,
-      "Attempting to associate more than one mutex with a condition\n"
-      "variable is undefined behavior. Ensure that you're calling\n"
-      "pthread_cond_wait() with the same mutex.");
+  // 2. Now test for undefined behavior or invalid arguments.
+  //    If fail, then call setNextTransition on nextTransition, in order to
+  //    display correct results for programState->printNextTransitions().
+  if (mutexThatExists->isUnlocked()) {
+    programState->setNextTransitionForThread(threadThatRanId, std::shared_ptr<MCTransition>(nextTransition));
+    mc_report_undefined_behavior(
+      "Attempting to wait on a condition variable with a mutex that is unlocked.");
   }
 
-  const auto threadThatRanId = shmTransition->executor;
-  const auto mutexAssociatedWithConditionVariable =
-    condThatExists->mutex;
+  if (condThatExists->isDestroyed()) {
+    programState->setNextTransitionForThread(threadThatRanId, std::shared_ptr<MCTransition>(nextTransition));
+    mc_report_undefined_behavior(
+      "Attempting to wait on a destroyed condition variable.");
+  }
 
+#if 1
   // NOTE: It's possible (and likely) for a condition variable
   // to NOT already be associated with a mutex at this point.
   // E.g., the first call to pthread_cond_wait() will have a
   // condition variable that isn't associated with a mutex.
   //    mutexThatExists->mutexShadow.systemIdentity
-  if (mutexAssociatedWithConditionVariable) {
+  if (condThatExists->mutex != nullptr &&
+      *condThatExists->mutex != *mutexThatExists) {
+    programState->setNextTransitionForThread(threadThatRanId, std::shared_ptr<MCTransition>(nextTransition));
+    mc_report_undefined_behavior(
+      "Attempting to associate more than one mutex with a condition\n"
+      "variable is undefined behavior.\n"
+      "    NOTE: A different mutex was previously bound to this condition\n"
+      "ariable, and at least one thread is still blocked on that previous\n"
+      "mutex.  But pthread_cond_wait is attempting to bind a new mutex to\n"
+      "the condition variable, even while some thread is still blocked on\n"
+      "the first mutex.");
+  }
+#else
+  // FIXME: Remove this old code.  If fails to setNextTransitionForThread()
+  if (condThatExists->mutex != nullptr) {
     MC_REPORT_UNDEFINED_BEHAVIOR_ON_FAIL(
-      *mutexAssociatedWithConditionVariable == *mutexThatExists,
+      *condThatExists->mutex == *mutexThatExists,
+      "Attempting to associate more than one mutex with a condition\n"
+      "variable is undefined behavior.\n"
+      "    NOTE: A different mutex was previously bound to this condition\n"
+      "ariable, and at least one thread is still blocked on that previous\n"
+      "mutex.  But pthread_cond_wait is attempting to bind a new mutex to\n"
+      "the condition variable, even while some thread is still blocked on\n"
+      "the first mutex.");
+  }
+#endif
+
+#if 0
+  // FIXME:  Remove this old code.
+  //   This logic seems to be identical tothe previous MC_REPORT.
+  //   Originally, a temporary variable, CondAssociatedMutex was used
+  //   here instead of condThatExists->mutex.
+  if (condThatExists->mutex != nullptr) {
+    MC_REPORT_UNDEFINED_BEHAVIOR_ON_FAIL(
+      *condThatExists->mutex == *mutexThatExists,
       "A different mutex was previously bound to this condition variable,\n"
       "and at least one thread is still blocked on that previous mutex.\n"
       "But pthread_cond_wait is attempting to bind a new mutex to the\n"
       "condition variable, even while some thread is still blocked on\n"
       "the first mutex.");
   }
+#endif
+
+  // 3. There are no undefined behaviors or invalid arguments.
+  //    So, we succeeded.  Associate the condThatExists with the new mutex.
+  //    and then return the previously computed nextTransition.
 
   // 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()
   // enqueue call were dependent with a pthread_mutex_lock(). Note
   // that we ALSO must assign the mutex when the operation is APPLIED
   // to the condition variable
+  //    We don't associate the mutex earlier, because we needed to test
+  // the old condThatExists->mutex, in case of undefined behavior.
   condThatExists->mutex = mutexThatExists;
-  auto threadThatRan    = state->getThreadWithId(threadThatRanId);
-  return new MCCondEnqueue(threadThatRan, condThatExists,
-                           mutexThatExists);
+  return nextTransition;
 }
 
 std::shared_ptr<MCTransition>

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;
+}