diff --git a/include/mcmini/coordinator/model_to_system_map.hpp b/include/mcmini/coordinator/model_to_system_map.hpp index 91674ec..40f096f 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 5c056b1..64c3255 100644 --- a/src/examples/CMakeLists.txt +++ b/src/examples/CMakeLists.txt @@ -1,11 +1,15 @@ 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(cv-uninitialized cv-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(cv-uninitialized PUBLIC -pthread) target_link_libraries(deadly-embrace PUBLIC -pthread) target_link_libraries(producer-consumer PUBLIC -pthread) diff --git a/src/examples/cv-uninitialized.c b/src/examples/cv-uninitialized.c new file mode 100644 index 0000000..84a979d --- /dev/null +++ b/src/examples/cv-uninitialized.c @@ -0,0 +1,24 @@ +// Negative test for PTHREAD_COND_INITIALIZER support. +// +// A stack-allocated condition variable that was never initialized -- neither +// via pthread_cond_init() nor PTHREAD_COND_INITIALIZER -- is operated on. McMini +// must report undefined behavior rather than silently accepting it. +// +// The cond var is filled with non-zero garbage so it cannot be mistaken for +// PTHREAD_COND_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 cv would (intentionally) slip through -- see the FIXME +// in src/mcmini/model/transitions/condition_variables.cpp. +// +// Expected McMini result: +// UNDEFINED BEHAVIOR: +// Attempting to signal an uninitialized condition variable +#include +#include + +int main(void) { + pthread_cond_t cond; + memset(&cond, 0xff, sizeof(cond)); // simulate an uninitialized stack cv + pthread_cond_signal(&cond); + return 0; +} diff --git a/src/examples/mutex-uninitialized.c b/src/examples/mutex-uninitialized.c new file mode 100644 index 0000000..99fe155 --- /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 2b8146d..c3e9e03 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/condition_variables.cpp b/src/mcmini/model/transitions/condition_variables.cpp index c5af6d7..dead85e 100644 --- a/src/mcmini/model/transitions/condition_variables.cpp +++ b/src/mcmini/model/transitions/condition_variables.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/condition_variables/callbacks.hpp" @@ -6,6 +14,61 @@ using namespace model; using namespace objects; +namespace { + +/** + * @brief Reads the bytes of the condition variable at `remote_cond` out of the + * target process `target_pid` and reports whether they match the bit pattern + * of a statically-initialized condition variable (`PTHREAD_COND_INITIALIZER`). + * + * @return true if the remote bytes equal `PTHREAD_COND_INITIALIZER`; false if + * they differ or the remote memory could not be read. + */ +bool remote_cond_is_static_initializer(pid_t target_pid, + pthread_cond_t *remote_cond) { + if (target_pid <= 0) return false; + pthread_cond_t initializer = PTHREAD_COND_INITIALIZER; + pthread_cond_t local; + struct iovec local_iov = {&local, sizeof(local)}; + struct iovec remote_iov = {(void *)remote_cond, 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; +} + +/** + * @brief Ensures `remote_cond` is present in the model, supporting condition + * variables declared with `PTHREAD_COND_INITIALIZER`. + * + * Such a condition variable never flows through the `pthread_cond_init` + * wrapper, so the model never observes it being initialized. If the model has + * not seen it, read the target's memory: if it matches + * `PTHREAD_COND_INITIALIZER`, lazily register it as initialized (mirroring + * `cond_init_callback`); otherwise report `ub_message` as undefined behavior. + * + * FIXME: As in the original McMini, this detects an uninitialized condition + * variable only for stack-allocated (or otherwise garbage-filled) cvs. A + * never-initialized cv in the data or heap segment is zero-filled, which on + * glibc is identical to `PTHREAD_COND_INITIALIZER`, so it passes this check and + * slips through undetected. + */ +void ensure_cond_initialized(model_to_system_map &m, + pthread_cond_t *remote_cond, + const char *ub_message) { + if (m.contains(remote_cond)) return; + if (!remote_cond_is_static_initializer(m.get_target_pid(), remote_cond)) + throw undefined_behavior_exception(ub_message); + // FIXME: Allow dynamic selection of wakeup policies (mirrors + // cond_init_callback). + ConditionVariablePolicy *policy = new ConditionVariableArbitraryPolicy(); + m.observe_object(remote_cond, new condition_variable( + condition_variable::state::cv_initialized, + policy)); +} + +} // namespace + model::transition* cond_init_callback(runner_id_t p, const volatile runner_mailbox& rmb, model_to_system_map& m) { @@ -36,14 +99,14 @@ model::transition* cond_waiting_thread_enqueue_callback(runner_id_t p, memcpy_v(&remote_cond, (volatile void*)rmb.cnts, sizeof(pthread_cond_t*)); memcpy_v(&remote_mut, (volatile void*)(rmb.cnts + sizeof(pthread_cond_t*)), sizeof(pthread_mutex_t*)); - if (!m.contains(remote_cond)) - throw undefined_behavior_exception( - "Attempting to wait on an uninitialized condition variable"); + ensure_cond_initialized( + m, remote_cond, + "Attempting to wait on an uninitialized condition variable"); if (!m.contains(remote_mut)) throw undefined_behavior_exception( "Attempting to wait on a condition variable with an uninitialized mutex"); - + state::objid_t const cond = m.get_model_of_object(remote_cond); state::objid_t const mut = m.get_model_of_object(remote_mut); return new transitions::condition_variable_enqueue_thread(p, cond, mut); @@ -79,9 +142,9 @@ model::transition* cond_signal_callback(runner_id_t p, memcpy_v(&remote_cond, (volatile void*)rmb.cnts, sizeof(pthread_cond_t*)); // Locate the corresponding model of this object - if (!m.contains(remote_cond)) - throw undefined_behavior_exception( - "Attempting to signal an uninitialized condition variable"); + ensure_cond_initialized( + m, remote_cond, + "Attempting to signal an uninitialized condition variable"); state::objid_t const cond = m.get_model_of_object(remote_cond); return new transitions::condition_variable_signal(p, cond); @@ -94,9 +157,9 @@ model::transition* cond_broadcast_callback(runner_id_t p, memcpy_v(&remote_cond, (volatile void*)rmb.cnts, sizeof(pthread_cond_t*)); // Locate the corresponding model of this object - if (!m.contains(remote_cond)) - throw undefined_behavior_exception( - "Attempting to broadcast on an uninitialized condition variable"); + ensure_cond_initialized( + m, remote_cond, + "Attempting to broadcast on an uninitialized condition variable"); state::objid_t const cond = m.get_model_of_object(remote_cond); return new transitions::condition_variable_broadcast(p, cond); diff --git a/src/mcmini/model/transitions/mutex.cpp b/src/mcmini/model/transitions/mutex.cpp index 1757a7e..20eee4e 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);