PTHREAD_COND_INITIALIZER support

include/mcmini/coordinator/model_to_system_map.hpp

@@ -1,5 +1,7 @@
 #pragma once
 
+#include <sys/types.h>
+
 #include <functional>
 
 #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<const model::transition *(model::state::runner_id_t)>;
 

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)

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 <pthread.h>
+#include <string.h>
+
+int main(void) {
+  pthread_cond_t cond;
+  memset(&cond, 0xff, sizeof(cond));  // simulate an uninitialized stack cv
+  pthread_cond_signal(&cond);
+  return 0;
+}

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 <pthread.h>
+#include <string.h>
+
+int main(void) {
+  pthread_mutex_t mutex;
+  memset(&mutex, 0xff, sizeof(mutex));  // simulate an uninitialized stack mutex
+  pthread_mutex_lock(&mutex);
+  return 0;
+}

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<void> handle) const {
   model::state::objid_t objid = get_model_of_object(handle);

src/mcmini/model/transitions/condition_variables.cpp

@@ -1,3 +1,11 @@
+#ifndef _GNU_SOURCE
+#define _GNU_SOURCE  // for process_vm_readv(2)
+#endif
+#include <pthread.h>
+#include <sys/uio.h>
+
+#include <cstring>
+
 #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);

src/mcmini/model/transitions/mutex.cpp

@@ -1,10 +1,47 @@
+#ifndef _GNU_SOURCE
+#define _GNU_SOURCE  // for process_vm_readv(2)
+#endif
+#include <pthread.h>
+#include <sys/uio.h>
+
+#include <cstring>
+
 #include "mcmini/mem.h"
 #include "mcmini/model/exception.hpp"
 #include "mcmini/model/transitions/mutex/callbacks.hpp"
 
 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);