From 6ca17d5a5b7f77e71d543d1fc2468b54e77b6cc1 Mon Sep 17 00:00:00 2001 From: Gene Cooperman Date: Mon, 22 Dec 2025 03:05:29 -0500 Subject: [PATCH 1/2] Fix commit dfe4e77b: 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. --- NEWS | 5 +++++ src/transitions/cond/MCCondEnqueue.cpp | 12 ++++++++++++ src/transitions/cond/MCCondWait.cpp | 6 ------ 3 files changed, 17 insertions(+), 6 deletions(-) diff --git a/NEWS b/NEWS index 3697ba6c..c6c6df3f 100644 --- a/NEWS +++ b/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) ========================================== diff --git a/src/transitions/cond/MCCondEnqueue.cpp b/src/transitions/cond/MCCondEnqueue.cpp index 47696fee..39bbc811 100644 --- a/src/transitions/cond/MCCondEnqueue.cpp +++ b/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() diff --git a/src/transitions/cond/MCCondWait.cpp b/src/transitions/cond/MCCondWait.cpp index 32c8cd7f..f05500b8 100644 --- a/src/transitions/cond/MCCondWait.cpp +++ b/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 From 504a38a80d4316c980026205b018ab4bbda8db4c Mon Sep 17 00:00:00 2001 From: Gene Cooperman Date: Tue, 23 Dec 2025 13:37:56 -0500 Subject: [PATCH 2/2] Add test program: condvar-two-mutexes.c --- .../condvar-two-mutexes.c | 96 +++++++++++++++++++ 1 file changed, 96 insertions(+) create mode 100644 test/invalid_thread_op_arg_program/condvar-two-mutexes.c diff --git a/test/invalid_thread_op_arg_program/condvar-two-mutexes.c b/test/invalid_thread_op_arg_program/condvar-two-mutexes.c new file mode 100644 index 00000000..cc36b148 --- /dev/null +++ b/test/invalid_thread_op_arg_program/condvar-two-mutexes.c @@ -0,0 +1,96 @@ +#include +#include +#include +#include +#include + +#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; +}