Add mutex owner tests in pthread_mutex_lock/unlock

NEWS

@@ -1,3 +1,7 @@
+Version 1.2.0 release notes (DATE: TBD)
+==========================================
+* Check for recursive pthread_mutex_lock by a thread already holding that mutex lock.
+
 Version 1.1.0 release notes (Oct. 7, 2025)
 ==========================================
 

include/objects/MCMutex.h

@@ -7,6 +7,7 @@
 struct MCMutexShadow {
   pthread_mutex_t *systemIdentity;
   enum State { undefined, unlocked, locked, destroyed } state;
+  tid_t owner;
   explicit MCMutexShadow(pthread_mutex_t *systemIdentity)
     : systemIdentity(systemIdentity), state(undefined)
   {}
@@ -45,6 +46,7 @@ struct MCMutex : public MCVisibleObject {
   void unlock();
   void init();
   void deinit();
+  tid_t ownerTid() const;
 };
 
 #endif // INCLUDE_MCMINI_OBJECTS_MCMUTEX_HPP

src/objects/MCMutex.cpp

@@ -48,18 +48,21 @@ void
 MCMutex::lock(tid_t newOwner)
 {
   this->mutexShadow.state = MCMutexShadow::locked;
+  this->mutexShadow.owner = newOwner;
 }
 
 void
 MCMutex::unlock()
 {
   this->mutexShadow.state = MCMutexShadow::unlocked;
+  this->mutexShadow.owner = TID_INVALID;
 }
 
 void
 MCMutex::init()
 {
   this->mutexShadow.state = MCMutexShadow::unlocked;
+  this->mutexShadow.owner = TID_INVALID;
 }
 
 void
@@ -68,6 +71,12 @@ MCMutex::deinit()
   this->mutexShadow.state = MCMutexShadow::undefined;
 }
 
+tid_t
+MCMutex::ownerTid() const
+{
+  return this->mutexShadow.owner;
+}
+
 bool
 MCMutex::canAcquire(tid_t thread) const
 {

src/transitions/mutex/MCMutexLock.cpp

@@ -80,17 +80,36 @@ MCReadMutexLock(const MCSharedTransition *shmTransition,
   assert(mutexThatExists -> mutexShadow.state == MCMutexShadow::unlocked ||
          mutexThatExists -> mutexShadow.state == MCMutexShadow::locked);
 
-  MC_REPORT_UNDEFINED_BEHAVIOR_ON_FAIL(
-    mutexThatExists != nullptr,
-    "Attempting to lock an uninitialized mutex");
+  // 1. We've now computed mutexThatExists (i.e., the state of the
+  //    mutex arguments to pthread_mutex_lock()).  Compute the nextTransition.
+  tid_t threadThatRanId = shmTransition->executor;
+  auto threadThatRan    = state->getThreadWithId(threadThatRanId);
+  MCTransition *nextTransition =
+    new MCMutexLock(threadThatRan, mutexThatExists);
+
+  // 2. Now test for undefined behaviors or invalid arguments.
+  //    If fail, then call setNextTransition on nextTransition, in order to
+  //    display correct results for programState->printNextTransitions().
+  if (mutexThatExists == nullptr) {
+    programState->setNextTransitionForThread(threadThatRanId, std::shared_ptr<MCTransition>(nextTransition));
+    mc_report_undefined_behavior(
+      "Attempting to lock an uninitialized mutex");
+  }
   if (mutexThatExists->isDestroyed()) {
-    MC_REPORT_UNDEFINED_BEHAVIOR(
+    programState->setNextTransitionForThread(threadThatRanId, std::shared_ptr<MCTransition>(nextTransition));
+    mc_report_undefined_behavior(
       "Attempting to lock a mutex that has been destroyed");
   }
 
-  tid_t threadThatRanId = shmTransition->executor;
-  auto threadThatRan    = state->getThreadWithId(threadThatRanId);
-  return new MCMutexLock(threadThatRan, mutexThatExists);
+  if (mutexThatExists->isLocked() &&
+      mutexThatExists->ownerTid() == threadThatRanId) {
+    programState->setNextTransitionForThread(threadThatRanId, std::shared_ptr<MCTransition>(nextTransition));
+    mc_report_undefined_behavior(
+      "Attempting to recursively lock a mutex already owned by this thread.");
+  }
+
+  // 3. Success (no undefined behavior or invalid args).  Return nextTransition.
+  return nextTransition;
 }
 
 std::shared_ptr<MCTransition>

src/transitions/mutex/MCMutexUnlock.cpp

@@ -14,17 +14,39 @@ MCReadMutexUnlock(const MCSharedTransition *shmTransition,
     mutexThatExists != nullptr,
     "Attempting to unlock an uninitialized mutex");
 
+  // 1. We've now computed mutexThatExists (i.e., the state of the
+  //    mutex arguments to pthread_mutex_lock()).  Compute the nextTransition.
+  tid_t threadThatRanId = shmTransition->executor;
+  auto threadThatRan    = state->getThreadWithId(threadThatRanId);
+  MCTransition *nextTransition =
+    new MCMutexUnlock(threadThatRan, mutexThatExists);
+
+  // 2. Now test for undefined behaviors or invalid arguments.
+  //    If fail, then call setNextTransition on nextTransition, in order to
+  //    display correct results for programState->printNextTransitions().
+  if (mutexThatExists == nullptr) {
+    programState->setNextTransitionForThread(threadThatRanId, std::shared_ptr<MCTransition>(nextTransition));
+    mc_report_undefined_behavior(
+      "Attempting to unlock an uninitialized mutex");
+  }
+  if (mutexThatExists->isDestroyed()) {
+    programState->setNextTransitionForThread(threadThatRanId, std::shared_ptr<MCTransition>(nextTransition));
+    mc_report_undefined_behavior(
+      "Attempting to unlock a mutex that has been destroyed");
+  }
   if (mutexThatExists->isUnlocked()) {
-    MC_REPORT_UNDEFINED_BEHAVIOR(
+    programState->setNextTransitionForThread(threadThatRanId, std::shared_ptr<MCTransition>(nextTransition));
+    mc_report_undefined_behavior(
       "Attempting to unlock a mutex that is already unlocked");
-  } else if (mutexThatExists->isDestroyed()) {
-    MC_REPORT_UNDEFINED_BEHAVIOR(
-      "Attempting to unlock a mutex that has been destroyed");
+  }
+  if (mutexThatExists->ownerTid() != threadThatRanId) {
+    programState->setNextTransitionForThread(threadThatRanId, std::shared_ptr<MCTransition>(nextTransition));
+    mc_report_undefined_behavior(
+      "Attempting to unlock a mutex that was locked by a different thread.");
   }
 
-  tid_t threadThatRanId = shmTransition->executor;
-  auto threadThatRan    = state->getThreadWithId(threadThatRanId);
-  return new MCMutexUnlock(threadThatRan, mutexThatExists);
+  // 3. Success (no undefined behavior or invalid args).  Return nextTransition.
+  return nextTransition;
 }
 
 std::shared_ptr<MCTransition>

test/invalid_thread_op_arg_program/mutex-lock-unlock-two-owners.cpp

@@ -0,0 +1,29 @@
+// BUG: One thread locks a mutex, and a second thread unlocks the mutex.
+#include <pthread.h>
+#include <semaphore.h>
+
+pthread_mutex_t lock;
+sem_t signal_sem;
+
+void* lock_thread(void* arg) {
+    pthread_mutex_lock(&lock);
+    sem_post(&signal_sem);
+    return NULL;
+}
+void* unlock_thread(void* arg) {
+    sem_wait(&signal_sem);
+    pthread_mutex_unlock(&lock);
+    return NULL;
+}
+int main() {
+    pthread_t t1, t2;
+    pthread_mutex_init(&lock, NULL);
+    sem_init(&signal_sem, 0, 0);
+    pthread_create(&t1, NULL, lock_thread, NULL);
+    pthread_create(&t2, NULL, unlock_thread, NULL);
+    pthread_join(t1, NULL);
+    pthread_join(t2, NULL);
+    sem_destroy(&signal_sem);
+    pthread_mutex_destroy(&lock);
+    return 0;
+}

test/invalid_thread_op_arg_program/mutex-recursive-lock.cpp

@@ -0,0 +1,16 @@
+// BUG: the thread tries to recursively lock a mutex that it owns.
+#include <pthread.h>
+
+void* lock_thread(void* arg) {
+    pthread_mutex_lock(&lock);
+    pthread_mutex_lock(&lock);
+    return NULL;
+}
+int main() {
+    pthread_t t1, t2;
+    pthread_mutex_init(&lock, NULL);
+    pthread_create(&t1, NULL, lock_thread, NULL);
+    pthread_join(t1, NULL);
+    pthread_mutex_destroy(&lock);
+    return 0;
+}