From 5f1f26da235fcaa78dcb88bd1d562f4db48be204 Mon Sep 17 00:00:00 2001 From: Gene Cooperman Date: Tue, 30 Jun 2026 13:20:55 -0400 Subject: [PATCH 1/2] Support PTHREAD_MUTEX_INITIALIZER (statically-initialized mutexes) A mutex declared with PTHREAD_MUTEX_INITIALIZER never flows through the pthread_mutex_init wrapper, so the model never observes it being initialized. Previously mutex_lock_callback threw "uninitialized mutex" in that case (the `// TODO: add code from Gene's PR here` placeholder). Port the original McMini behavior: on a lock of a mutex the model has not seen, read the target's memory via process_vm_readv and compare against PTHREAD_MUTEX_INITIALIZER. On a match, lazily register the mutex as initialized+unlocked; otherwise report undefined behavior. Unlock is left reporting undefined behavior for an unknown mutex (faithful to the original, which does not lazily register on unlock). - model_to_system_map: expose get_target_pid() so callbacks can read the live target's memory. - coordinator: implement get_target_pid() from the current process handle. - mutex.cpp: add the process_vm_readv validation helper and port the lock callback; fix the mis-copied unlock message. A FIXME documents that, as in the original McMini, this only detects an uninitialized mutex for stack/garbage mutexes; a never-initialized data/heap mutex is zero-filled (== PTHREAD_MUTEX_INITIALIZER on glibc) and still slips through. Co-Authored-By: Claude Opus 4.8 (1M context) --- .../coordinator/model_to_system_map.hpp | 12 ++++ src/mcmini/coordinator/coordinator.cpp | 6 ++ src/mcmini/model/transitions/mutex.cpp | 68 +++++++++++++++++-- 3 files changed, 80 insertions(+), 6 deletions(-) diff --git a/include/mcmini/coordinator/model_to_system_map.hpp b/include/mcmini/coordinator/model_to_system_map.hpp index 91674ec5..40f096ff 100644 --- a/include/mcmini/coordinator/model_to_system_map.hpp +++ b/include/mcmini/coordinator/model_to_system_map.hpp @@ -1,5 +1,7 @@ #pragma once +#include + #include #include "mcmini/coordinator/coordinator.hpp" @@ -52,6 +54,16 @@ class model_to_system_map final { return get_model_of_runner(addr) != model::invalid_rid; } + /** + * @brief The PID of the live target process the coordinator is currently + * managing, or -1 if no process is currently alive. + * + * Used by transition callbacks that need to inspect the target's memory + * directly (e.g. reading a primitive to check whether it was statically + * initialized). + */ + pid_t get_target_pid() const; + using runner_generation_function = std::function; diff --git a/src/mcmini/coordinator/coordinator.cpp b/src/mcmini/coordinator/coordinator.cpp index 2b8146d3..c3e9e03f 100644 --- a/src/mcmini/coordinator/coordinator.cpp +++ b/src/mcmini/coordinator/coordinator.cpp @@ -102,6 +102,12 @@ void coordinator::return_to_depth(uint32_t n) { << "\n\n**************** AFTER RESTORATION *********************"; } +pid_t model_to_system_map::get_target_pid() const { + return _coordinator.current_process_handle + ? _coordinator.current_process_handle->get_pid() + : -1; +} + model::state::runner_id_t model_to_system_map::get_model_of_runner( remote_address handle) const { model::state::objid_t objid = get_model_of_object(handle); diff --git a/src/mcmini/model/transitions/mutex.cpp b/src/mcmini/model/transitions/mutex.cpp index 1757a7e7..20eee4ed 100644 --- a/src/mcmini/model/transitions/mutex.cpp +++ b/src/mcmini/model/transitions/mutex.cpp @@ -1,3 +1,11 @@ +#ifndef _GNU_SOURCE +#define _GNU_SOURCE // for process_vm_readv(2) +#endif +#include +#include + +#include + #include "mcmini/mem.h" #include "mcmini/model/exception.hpp" #include "mcmini/model/transitions/mutex/callbacks.hpp" @@ -5,6 +13,35 @@ using namespace model; using namespace objects; +namespace { + +/** + * @brief Reads the bytes of the mutex at `remote_mutex` out of the target + * process `target_pid` and reports whether they match the bit pattern of a + * statically-initialized mutex (`PTHREAD_MUTEX_INITIALIZER`). + * + * This is how a mutex declared with `PTHREAD_MUTEX_INITIALIZER` (which never + * flows through the `pthread_mutex_init` wrapper, and so is never observed by + * the model) is distinguished from a genuinely uninitialized one. + * + * @return true if the remote bytes equal `PTHREAD_MUTEX_INITIALIZER`; false if + * they differ or the remote memory could not be read. + */ +bool remote_mutex_is_static_initializer(pid_t target_pid, + pthread_mutex_t *remote_mutex) { + if (target_pid <= 0) return false; + pthread_mutex_t initializer = PTHREAD_MUTEX_INITIALIZER; + pthread_mutex_t local; + struct iovec local_iov = {&local, sizeof(local)}; + struct iovec remote_iov = {(void *)remote_mutex, sizeof(local)}; + ssize_t nread = + process_vm_readv(target_pid, &local_iov, 1, &remote_iov, 1, 0); + if (nread != (ssize_t)sizeof(local)) return false; + return memcmp(&local, &initializer, sizeof(local)) == 0; +} + +} // namespace + model::transition* mutex_init_callback(runner_id_t p, const volatile runner_mailbox& rmb, model_to_system_map& m) { @@ -26,10 +63,26 @@ model::transition* mutex_lock_callback(runner_id_t p, pthread_mutex_t* remote_mut; memcpy_v(&remote_mut, (volatile void*)rmb.cnts, sizeof(pthread_mutex_t*)); - // TODO: add code from Gene's PR here - if (!m.contains(remote_mut)) - throw undefined_behavior_exception( - "Attempting to lock an uninitialized mutex"); + if (!m.contains(remote_mut)) { + // The model has never seen this mutex initialized. Either it was declared + // with `PTHREAD_MUTEX_INITIALIZER` (which never flows through the + // `pthread_mutex_init` wrapper) or it is genuinely uninitialized. Read the + // target's memory to tell the two apart. + // + // FIXME: This detects an uninitialized-mutex bug only for stack-allocated + // (or otherwise garbage-filled) mutexes. A mutex in the data or heap + // segment is zero-initialized by the OS, and on glibc that bit pattern is + // identical to `PTHREAD_MUTEX_INITIALIZER`, so a never-initialized + // data/heap mutex passes this check and slips through undetected (same + // limitation as the original McMini). + if (!remote_mutex_is_static_initializer(m.get_target_pid(), remote_mut)) + throw undefined_behavior_exception( + "Attempting to lock an uninitialized mutex"); + + // Statically initialized via `PTHREAD_MUTEX_INITIALIZER`: lazily register + // it as an initialized, unlocked mutex. + m.observe_object(remote_mut, new mutex(mutex::state::unlocked, remote_mut)); + } state::objid_t const mut = m.get_model_of_object(remote_mut); return new transitions::mutex_lock(p, mut); @@ -41,10 +94,13 @@ model::transition* mutex_unlock_callback(runner_id_t p, pthread_mutex_t* remote_mut; memcpy_v(&remote_mut, (volatile void*)rmb.cnts, sizeof(pthread_mutex_t*)); - // TODO: add code from Gene's PR here + // Unlike lock, unlocking a mutex the model has never seen is genuine + // undefined behavior (a `PTHREAD_MUTEX_INITIALIZER` mutex starts unlocked, so + // a first-ever operation of "unlock" cannot be valid). This matches the + // original McMini, which does not lazily register a mutex on unlock. if (!m.contains(remote_mut)) throw undefined_behavior_exception( - "Attempting to lock an uninitialized mutex"); + "Attempting to unlock an uninitialized mutex"); state::objid_t const mut = m.get_model_of_object(remote_mut); return new transitions::mutex_unlock(p, mut); From f58122933840c491dcb1cf80f7037d482027dcb3 Mon Sep 17 00:00:00 2001 From: Gene Cooperman Date: Wed, 1 Jul 2026 13:07:09 -0400 Subject: [PATCH 2/2] Add negative test for uninitialized stack-allocated mutex Exercises the reject path of the PTHREAD_MUTEX_INITIALIZER support: a stack-allocated pthread_mutex_t filled with non-zero garbage (so it cannot be mistaken for the all-zero PTHREAD_MUTEX_INITIALIZER) is locked without initialization. McMini reports: UNDEFINED BEHAVIOR: Attempting to lock an uninitialized mutex Note the data/heap case is intentionally not detected (zero-filled == PTHREAD_MUTEX_INITIALIZER); see the FIXME in src/mcmini/model/transitions/mutex.cpp. Co-Authored-By: Claude Opus 4.8 (1M context) --- src/examples/CMakeLists.txt | 2 ++ src/examples/mutex-uninitialized.c | 24 ++++++++++++++++++++++++ 2 files changed, 26 insertions(+) create mode 100644 src/examples/mutex-uninitialized.c diff --git a/src/examples/CMakeLists.txt b/src/examples/CMakeLists.txt index 5c056b14..a208fea8 100644 --- a/src/examples/CMakeLists.txt +++ b/src/examples/CMakeLists.txt @@ -1,11 +1,13 @@ add_executable(hello-world hello-world.c) add_executable(cv-hello-world cv-hello-world.c) add_executable(cv-test cv-test.c) +add_executable(mutex-uninitialized mutex-uninitialized.c) add_executable(deadly-embrace deadly-embrace.c) add_executable(fifo-example fifo.cpp) add_executable(producer-consumer producer-consumer.c) target_link_libraries(hello-world PUBLIC -pthread) target_link_libraries(cv-hello-world PUBLIC -pthread) target_link_libraries(cv-test PUBLIC -pthread) +target_link_libraries(mutex-uninitialized PUBLIC -pthread) target_link_libraries(deadly-embrace PUBLIC -pthread) target_link_libraries(producer-consumer PUBLIC -pthread) diff --git a/src/examples/mutex-uninitialized.c b/src/examples/mutex-uninitialized.c new file mode 100644 index 00000000..99fe1552 --- /dev/null +++ b/src/examples/mutex-uninitialized.c @@ -0,0 +1,24 @@ +// Negative test for PTHREAD_MUTEX_INITIALIZER support. +// +// A stack-allocated mutex that was never initialized -- neither via +// pthread_mutex_init() nor PTHREAD_MUTEX_INITIALIZER -- is locked. McMini must +// report undefined behavior rather than silently accepting it. +// +// The mutex is filled with non-zero garbage so it cannot be mistaken for +// PTHREAD_MUTEX_INITIALIZER (which is all zeros on glibc). This is exactly the +// stack/garbage case the process_vm_readv check is designed to catch; a +// zero-filled data/heap mutex would (intentionally) slip through -- see the +// FIXME in src/mcmini/model/transitions/mutex.cpp. +// +// Expected McMini result: +// UNDEFINED BEHAVIOR: +// Attempting to lock an uninitialized mutex +#include +#include + +int main(void) { + pthread_mutex_t mutex; + memset(&mutex, 0xff, sizeof(mutex)); // simulate an uninitialized stack mutex + pthread_mutex_lock(&mutex); + return 0; +}