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