From d5ea9a9312a9d4c0af5e1a89762625b4ba39003c Mon Sep 17 00:00:00 2001 From: Gene Cooperman Date: Tue, 23 Dec 2025 13:37:56 -0500 Subject: [PATCH 1/3] 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; +} From 87a4763935f29b65cc3362ca0be05699bb970c5c Mon Sep 17 00:00:00 2001 From: Gene Cooperman Date: Wed, 24 Dec 2025 17:17:39 -0500 Subject: [PATCH 2/3] simulateRunningTransition(): Add extra comments for clarity. --- src/MCStack.cpp | 33 +++++++++++++++++++++++++-------- 1 file changed, 25 insertions(+), 8 deletions(-) diff --git a/src/MCStack.cpp b/src/MCStack.cpp index 30245fc6..3064a6f8 100644 --- a/src/MCStack.cpp +++ b/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); From 8c92288dd67274398c2c0e76829a1363d56f2a79 Mon Sep 17 00:00:00 2001 From: Gene Cooperman Date: Wed, 24 Dec 2025 03:45:23 -0500 Subject: [PATCH 3/3] MCCondEnqueue: mc_report_...: bad next transitions * Before calling mc_report_undefined_behavior_on_fail(), we need to call MCStack::setNextTranstion(), or else the "PENDING TRANSTIONS" displayed to the user will be incorrect. * While this fixes MCCondEnqueue, we will need to apply the same logic to the other transitions. * For testing, try condvar-two-mutexes.c, which has a bug in which the associated mutex of a condition variable is different from the mutex argument of pthread_cond_wait(). --- NEWS | 4 ++ src/mcmini_private.cpp | 4 ++ src/transitions/cond/MCCondEnqueue.cpp | 83 +++++++++++++++++++------- 3 files changed, 70 insertions(+), 21 deletions(-) diff --git a/NEWS b/NEWS index 3697ba6c..fc1a0554 100644 --- a/NEWS +++ b/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) ========================================== diff --git a/src/mcmini_private.cpp b/src/mcmini_private.cpp index b52c9fdc..340d0dff 100644 --- a/src/mcmini_private.cpp +++ b/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); } diff --git a/src/transitions/cond/MCCondEnqueue.cpp b/src/transitions/cond/MCCondEnqueue.cpp index 47696fee..23e6a7bb 100644 --- a/src/transitions/cond/MCCondEnqueue.cpp +++ b/src/transitions/cond/MCCondEnqueue.cpp @@ -100,40 +100,81 @@ 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(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(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(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, @@ -141,10 +182,10 @@ MCReadCondEnqueue(const MCSharedTransition *shmTransition, // 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