diff --git a/doc/glibc-sem-desync.txt b/doc/glibc-sem-desync.txt
new file mode 100644
index 00000000..1498c1a4
--- /dev/null
+++ b/doc/glibc-sem-desync.txt
@@ -0,0 +1,147 @@
+glibc sem_t "nwaiters" desync, and why child_side_sem is a raw futex instead
+=============================================================================
+
+What "glibc desync" means
+--------------------------
+glibc's NPTL sem_t packs two things into one 64-bit atomic word: the actual
+semaphore count, and `nwaiters` -- a count of how many threads are currently
+blocked inside sem_wait(). sem_post() uses `nwaiters` purely as an
+optimization: it increments the count, then checks `nwaiters`, and only
+makes the FUTEX_WAKE syscall if `nwaiters > 0`. If `nwaiters == 0`, it
+assumes nobody's waiting and skips the syscall entirely.
+
+"Desync" means `nwaiters` (glibc's userspace belief about who's waiting) no
+longer matches the kernel's actual futex wait queue for that address. When
+that happens, sem_post() can wrongly conclude "nobody is waiting" and
+silently skip the wake -- even though a real thread is genuinely parked in
+the kernel on that exact word. That is a lost wakeup, and the thread hangs
+forever.
+
+Does this happen only across checkpoint-restart, or anywhere?
+---------------------------------------------------------------
+Only in scenarios like McMini's, not in ordinary programs.
+
+In normal execution, `nwaiters` can never drift from reality, because the
+only code that ever touches it is sem_wait()/sem_post() themselves, via
+atomic read-modify-write on that same packed word -- it is a closed,
+self-consistent system. The only way to break it is for something *outside*
+the semaphore's own API to reset that memory (sem_destroy() + sem_init(), or
+an equivalent memset) while a thread is still validly blocked on it -- which
+POSIX explicitly documents as undefined behavior ("it is safe to destroy a
+semaphore only once no thread is blocked on it").
+
+Ordinary programs don't hit this because they only ever destroy a semaphore
+once they've confirmed nothing is using it. McMini's situation is different:
+DMTCP's checkpoint/restart transparently preserves a thread's real
+kernel-level "I'm blocked in this exact FUTEX_WAIT" state across the
+restart (that's just how checkpointing a blocked syscall works), while
+McMini's own code (mc_runner_mailbox_init()/mc_runner_mailbox_destroy())
+separately, explicitly reinitializes that same shared-memory semaphore for
+the new branch -- invisible to, and inconsistent with, a thread that (from
+the kernel's point of view) never actually left its old wait.
+
+CRIU's own documentation names this exact rule: everything sharing a
+futex/shared-memory region must be checkpointed and restored together as
+one atomic unit. McMini's architecture -- a permanent, never-checkpointed
+verifier sharing memory with a repeatedly-restarted target -- inherently
+breaks that rule.
+
+So: this is not a general glibc footgun waiting anywhere in a normal
+program; it is specific to externally reinitializing a semaphore's memory
+while a checkpoint/restart mechanism has silently kept a thread genuinely
+blocked on it underneath. Take away either half (no checkpoint/restart, or
+no external reinitialization) and it cannot occur.
+
+The fix
+--------
+Commit 1a4b3d9 ("Replace child_side_sem's glibc sem_t with a plain futex
+word") replaces `child_side_sem` -- the mailbox semaphore a DMTCP-restored
+target thread waits on, posted by the verifier -- with a bare futex word
+that has no separate userspace bookkeeping to desync in the first place.
+
+Files and functions:
+
+  include/mcmini/real_world/mailbox/runner_mailbox.h
+    - `child_side_sem` changed from `sem_t` to `uint32_t`.
+
+  src/common/runner_mailbox.c
+    - `mc_futex()`               -- thin wrapper around syscall(SYS_futex, ...).
+    - `mc_raw_sem_wait()`        -- replaces sem_wait() on child_side_sem: spins
+                                    on an atomic compare-and-swap against the
+                                    counter, blocking via FUTEX_WAIT only when
+                                    the counter is 0.
+    - `mc_raw_sem_post()`        -- replaces sem_post() on child_side_sem:
+                                    atomically increments the counter, then
+                                    calls FUTEX_WAKE *unconditionally* -- no
+                                    "is anyone really waiting" check, so there
+                                    is nothing to desync.
+    - `mc_wait_for_scheduler()`  -- now calls mc_raw_sem_wait().
+    - `mc_wake_thread()`         -- now calls mc_raw_sem_post().
+    - `mc_runner_mailbox_init()`/`mc_runner_mailbox_destroy()` -- initialize/
+      no-op-destroy the futex word directly instead of calling sem_init()/
+      sem_destroy() on it.
+
+`model_side_sem` (the verifier waits, the target posts) is untouched and
+remains a real sem_t: the verifier process is never checkpointed, so its
+side of the bookkeeping can never desync.
+
+Not yet fixed
+---------------
+Condition variables (pthread_cond_wait/pthread_cond_signal) have the same
+class of vulnerability via glibc's G1/G2 waiter-group bookkeeping, for the
+same reason (checkpoint/restart + externally-managed reinitialization). An
+analogous fix has not yet been applied there.
+
+Does this require pshared=1, or can it happen with pshared=0 too?
+---------------------------------------------------------------------
+`pshared` is the second parameter of sem_init() (`int sem_init(sem_t *sem,
+int pshared, unsigned int value)`): pshared=0 means the semaphore may only
+be used among threads of the single process that created it; pshared=1
+means it may be shared across process boundaries (typically by placing it
+in memory obtained via shm_open()/mmap(), as McMini does here).
+
+This bug requires pshared=1. It cannot happen with pshared=0, and the
+reason follows directly from the mechanism above: the desync needs an
+entity *outside the checkpointed unit* to reinitialize the semaphore's
+memory while a thread inside that unit is still genuinely blocked on it. In
+McMini's architecture that outside entity is the verifier (mcmini) -- a
+separate, permanent, never-checkpointed process -- while the target (with
+the blocked thread) gets checkpoint/restarted. DMTCP transparently
+preserves the target's kernel-level block across the restart, but the
+verifier's reinitialization of that shared memory has no way to know about,
+or wait for, that survival, because it is not part of the same checkpoint
+image at all.
+
+If pshared=0, the semaphore is only valid for use among threads of a
+single process. DMTCP checkpoints and restores that whole process --
+every thread, and all of the semaphore's own memory (nwaiters and value
+together) -- as one atomic, consistent snapshot. There is no outsider who
+could reinitialize the memory independently of the blocked thread's
+restore, because everything that touches it moves through the
+checkpoint/restart together.
+
+Two more reasons this is specifically a pshared=1 problem:
+
+  1. Using a pshared=0 semaphore across two processes is undefined
+     behavior under POSIX regardless of checkpointing -- Linux's NPTL
+     implementation uses FUTEX_PRIVATE_FLAG for private (pshared=0) futex
+     operations, keyed off the process's own memory descriptor, which
+     specifically assumes same-process access. "verifier process + target
+     process share a pshared=0 semaphore" is not a valid configuration to
+     begin with.
+  2. model_side_sem (still a real sem_t, pshared=1, in this same mailbox)
+     is the control case that proves the point: it is just as
+     cross-process-shared as child_side_sem was, but it is fine, because
+     the verifier's side of it is never checkpointed -- only the target
+     side (posting) is. The bug needs the *waiting* side to be the one
+     that gets checkpoint/restarted while the memory gets reinitialized
+     out from under it; that combination cannot arise for a purely
+     intra-process, pshared=0 semaphore.
+
+Separately: an ordinary program could still hit undefined behavior by
+calling sem_destroy() on any semaphore -- pshared=0 or 1 -- while a thread
+is genuinely blocked on it. That is always illegal per POSIX. But that is
+a plain application bug, not "the checkpoint/restart desync": the
+McMini-specific failure mode is that the reinitialization happens from a
+vantage point that literally cannot see the blocked thread at all, which
+is only possible across the process boundary that pshared=1 implies.
diff --git a/include/dmtcp.h b/include/dmtcp.h
index d0e774e4..e2e46f39 100644
--- a/include/dmtcp.h
+++ b/include/dmtcp.h
@@ -16,6 +16,8 @@
 #define DMTCP_H
 
 #include <netinet/ip.h>
+#include <assert.h>
+#include <pthread.h>
 #include <stddef.h>
 #include <stdio.h>
 #include <sys/socket.h>
@@ -43,8 +45,8 @@
 # define EXTERNC
 #endif // ifdef __cplusplus
 
-/* Define to the version of this package. */
-#define DMTCP_PLUGIN_API_VERSION "3"
+/* Bump when DmtcpPluginDescriptor_t changes ABI. */
+#define DMTCP_PLUGIN_API_VERSION "4"
 
 #ifdef __cplusplus
 namespace dmtcp {
@@ -145,6 +147,11 @@ typedef union _DmtcpEventData_t {
   struct {
     char *path;
   } realToVirtualPath, virtualToRealPath;
+
+  struct {
+    pthread_t pthread;
+    pid_t tid;
+  } pthreadInfo;
 } DmtcpEventData_t;
 
 typedef void (*HookFunctionPtr_t)(DmtcpEvent_t, DmtcpEventData_t *);
@@ -238,12 +245,78 @@ void dmtcp_initialize_plugin(void) __attribute((weak));
 typedef struct DmtcpUniqueProcessId {
   uint64_t _hostid;  // gethostid()
   uint64_t _time; // time()
-  pid_t _pid; // getpid()
+
+  union {
+    pid_t _pid; // getpid()
+    int32_t _;
+  };
+
   uint32_t _computation_generation; // computationGeneration()
 } DmtcpUniqueProcessId;
 
 int dmtcp_unique_pids_equal(DmtcpUniqueProcessId a, DmtcpUniqueProcessId b);
 
+typedef struct DmtcpInfo {
+  int argc;
+  const char **argv;
+} DmtcpInfo;
+
+enum ElfType {
+  Elf_32,
+  Elf_64
+};
+
+typedef struct {
+  uint64_t startAddr;
+  uint64_t endAddr;
+} MemRegion;
+
+typedef void (*PostRestartFnPtr_t)(double, int);
+#define DMTCP_CKPT_SIGNATURE "DMTCP_CHECKPOINT_IMAGE_v4.0\n"
+typedef struct {
+  char ckptSignature[32];
+
+  DmtcpUniqueProcessId upid;
+  DmtcpUniqueProcessId uppid;
+  DmtcpUniqueProcessId compGroup;
+
+  pid_t pid;
+  pid_t ppid;
+  pid_t sid;
+  pid_t gid;
+  pid_t fgid;
+  uint32_t isRootOfProcessTree;
+
+  uint32_t numPeers;
+  uint32_t elfType;
+
+  uint64_t clock_gettime_offset;
+  uint64_t getcpu_offset;
+  uint64_t gettimeofday_offset;
+  uint64_t time_offset;
+
+  // Reserve 3 * 30MB for restore buffer.
+#define RESTORE_BUF_TOTAL_SIZE (90 * 1024 * 1024)
+  MemRegion restoreBuf;
+
+  MemRegion vdso;
+  MemRegion vvar;
+  MemRegion vvarVClock;
+
+  uint64_t savedBrk;
+  uint64_t endOfStack;
+
+  uint64_t postRestartAddr;
+  //void (*post_restart)(double, int);
+
+  char procname[1024];
+  char procSelfExe[1024];
+
+  char padding[1792];
+} DmtcpCkptHeader;
+
+static_assert(sizeof(DmtcpCkptHeader) == 4096, "DmtcpCkptHeader must be 4096 bytes");
+
 // FIXME:
 // If a plugin is not compiled with defined(__PIC__) and we can verify
 // that we're using DMTCP (environment variables), and dmtcp_is_enabled
@@ -329,8 +402,6 @@ const char *dmtcp_get_ckpt_files_subdir(void);
 int dmtcp_should_ckpt_open_files(void);
 int dmtcp_allow_overwrite_with_ckpted_files(void);
 int dmtcp_skip_truncate_file_at_restart(const char* path);
-void dmtcp_set_restore_buf_addr(void *new_addr, uint64_t len);
-uint64_t dmtcp_restore_buf_len();
 
 int dmtcp_get_ckpt_signal(void);
 const char *dmtcp_get_uniquepid_str(void) __attribute__((weak));
@@ -428,13 +499,32 @@ int dmtcp_protected_environ_fd(void);
  *  discovers a pid without going through a system call (e.g., through
  *  the proc filesystem), use this to virtualize the pid.
  */
-pid_t dmtcp_real_to_virtual_pid(pid_t realPid) __attribute((weak));
-pid_t dmtcp_virtual_to_real_pid(pid_t virtualPid) __attribute((weak));
-
+pid_t dmtcp_pid_real_to_virtual(pid_t realPid) __attribute((weak));
+pid_t dmtcp_pid_virtual_to_real(pid_t virtualPid) __attribute((weak));
+
+// Returns 1 if virtual_tid names TSAN's own background thread, else 0.
+int dmtcp_is_tsan_background_thread(int virtual_tid) __attribute((weak));
+#define dmtcp_is_tsan_background_thread(virtual_tid) \
+  (dmtcp_is_tsan_background_thread ? \
+   dmtcp_is_tsan_background_thread(virtual_tid) : 0)
+
+// Tells DMTCP that this restart is one-shot: the checkpoint thread should
+// not resume its usual sleep-checkpoint-resume loop (i.e., it should not
+// wait for a future checkpoint request), since no such request is ever
+// coming. Must be called on the checkpoint thread itself, from a
+// DMTCP_EVENT_RESTART hook (before that event's plugin dispatch returns).
+void dmtcp_skip_post_restart_checkpoint_loop(void) __attribute((weak));
+#define dmtcp_skip_post_restart_checkpoint_loop() \
+  (dmtcp_skip_post_restart_checkpoint_loop ? \
+   dmtcp_skip_post_restart_checkpoint_loop() : (void)0)
+
+// McMini helpers: translate pids only when running under DMTCP.
+// (DMTCP plugin API v4 renamed dmtcp_{real_to_virtual,virtual_to_real}_pid to
+// dmtcp_pid_{real_to_virtual,virtual_to_real}.)
 #define mcmini_virtual_pid(PID) \
-  (dmtcp_is_enabled() ? dmtcp_real_to_virtual_pid((PID)) : (PID))
+  (dmtcp_is_enabled() ? dmtcp_pid_real_to_virtual((PID)) : (PID))
 #define mcmini_real_pid(PID) \
-  (dmtcp_is_enabled() ? dmtcp_virtual_to_real_pid((PID)) : (PID))
+  (dmtcp_is_enabled() ? dmtcp_pid_virtual_to_real((PID)) : (PID))
 
 // bq_file -> "batch queue file"; used only by batch-queue plugin
 int dmtcp_is_bq_file(const char *path) __attribute((weak));
@@ -445,7 +535,7 @@ int dmtcp_bq_restore_file(const char *path,
                           int type) __attribute((weak));
 
 /*  These next two functions are defined in contrib/ckptfile/ckptfile.cpp
- *  But they are currently used only in src/plugin/ipc/file/fileconnection.cpp
+ *  But they are currently used only in src/plugin/file/fileconnection.cpp
  *    and in a trivial fashion.  These are intended for future extensions.
  */
 int dmtcp_must_ckpt_file(const char *path) __attribute((weak));
diff --git a/include/mcmini/model/objects/mutex.hpp b/include/mcmini/model/objects/mutex.hpp
index 66789238..91d2fbac 100644
--- a/include/mcmini/model/objects/mutex.hpp
+++ b/include/mcmini/model/objects/mutex.hpp
@@ -1,5 +1,6 @@
 #pragma once
 
+#include "mcmini/defines.h"
 #include "mcmini/misc/extensions/unique_ptr.hpp"
 #include "mcmini/model/visible_object_state.hpp"
 
@@ -20,9 +21,16 @@ struct mutex : public model::visible_object_state {
   mutex() = default;
   ~mutex() = default;
   mutex(const mutex &) = default;
-  mutex(state s) : current_state(s) {}
-  mutex(state s, pthread_mutex_t* loc) : current_state(s), location(loc) {}
-  mutex(state s, pthread_mutex_t* loc, runner_id_t tid): current_state(s), location(loc), owner(tid) {}
+  // `location` has no default member initializer (unlike, say,
+  // condition_variable's `policy`), so it must always be passed explicitly
+  // -- a mutex without its real address is meaningless, and every
+  // mutex_lock/unlock faithfully forwards whatever get_location() returns,
+  // so an uninitialized one corrupts every subsequent state derived from
+  // it (see doc history around commit 9bd9ecf). `tid` defaults to
+  // RID_INVALID: "unlocked, no owner" is exactly what callers that omit it
+  // (mutex_init, condition_variable_enqueue_thread) mean.
+  mutex(state s, pthread_mutex_t* loc, runner_id_t tid = RID_INVALID)
+      : current_state(s), location(loc), owner(tid) {}
   
   // ---- State Observation --- //
   bool operator==(const mutex &other) const {
diff --git a/include/mcmini/model/transitions/condition_variables/condition_variable_enqueue_thread.hpp b/include/mcmini/model/transitions/condition_variables/condition_variable_enqueue_thread.hpp
index 73f2b1b1..e0acf25d 100644
--- a/include/mcmini/model/transitions/condition_variables/condition_variable_enqueue_thread.hpp
+++ b/include/mcmini/model/transitions/condition_variables/condition_variable_enqueue_thread.hpp
@@ -40,9 +40,15 @@ struct condition_variable_enqueue_thread : public model::transition{
 
     cv->get_policy()->add_waiter_with_state(executor, CV_WAITING);
     const int new_waiting_count = cv->get_policy()->return_wait_queue().size();
-    
+
     s.add_state_for_obj(cond_id, new condition_variable(condition_variable::cv_waiting, executor, m->get_location(), new_waiting_count));
-    s.add_state_for_obj(mutex_id, new mutex(mutex::unlocked));
+    // Preserve the mutex's location: mutex(state) (1-arg) has no default
+    // member initializer for `location` (unlike condition_variable's
+    // policy), so it's left completely uninitialized -- every later
+    // mutex_lock/unlock just faithfully forwards whatever garbage this
+    // leaves behind via ms->get_location(), corrupting the mutex's identity
+    // for the rest of the run.
+    s.add_state_for_obj(mutex_id, new mutex(mutex::unlocked, m->get_location()));
     return status::exists;
   }
   state::objid_t get_id() const { return this->cond_id; }
diff --git a/include/mcmini/model/transitions/mutex/mutex_init.hpp b/include/mcmini/model/transitions/mutex/mutex_init.hpp
index c664b2af..25dd1386 100644
--- a/include/mcmini/model/transitions/mutex/mutex_init.hpp
+++ b/include/mcmini/model/transitions/mutex/mutex_init.hpp
@@ -17,7 +17,14 @@ struct mutex_init : public model::transition {
 
   status modify(model::mutable_state& s) const override {
     using namespace model::objects;
-    s.add_state_for_obj(mutex_id, new mutex(mutex::unlocked));
+    // Preserve the location set on the placeholder object created by
+    // mutex_init_callback (see mutex.cpp) -- the 1-arg mutex(state)
+    // constructor used below has no default member initializer for
+    // `location`, so it would otherwise be left uninitialized, corrupting
+    // every later mutex_lock/unlock that faithfully forwards whatever
+    // garbage ms->get_location() reads back afterward.
+    const mutex* ms = s.get_state_of_object<mutex>(mutex_id);
+    s.add_state_for_obj(mutex_id, new mutex(mutex::unlocked, ms->get_location()));
     return status::exists;
   }
   state::objid_t get_id() const { return this->mutex_id; }
diff --git a/include/mcmini/model/transitions/mutex/mutex_unlock.hpp b/include/mcmini/model/transitions/mutex/mutex_unlock.hpp
index b100089a..4b50aabd 100644
--- a/include/mcmini/model/transitions/mutex/mutex_unlock.hpp
+++ b/include/mcmini/model/transitions/mutex/mutex_unlock.hpp
@@ -25,7 +25,7 @@ struct mutex_unlock : public model::transition {
       return status::disabled;
     }
 
-    s.add_state_for_obj(mutex_id, new mutex(mutex::unlocked, ms->get_location(), 0));
+    s.add_state_for_obj(mutex_id, new mutex(mutex::unlocked, ms->get_location()));
     return status::exists;
   }
   state::objid_t get_id() const { return this->mutex_id; }
diff --git a/include/mcmini/model/transitions/process/exit.hpp b/include/mcmini/model/transitions/process/exit.hpp
index e822bc20..6e69804d 100644
--- a/include/mcmini/model/transitions/process/exit.hpp
+++ b/include/mcmini/model/transitions/process/exit.hpp
@@ -1,5 +1,6 @@
 #pragma once
 
+#include "mcmini/model/objects/thread.hpp"
 #include "mcmini/model/transition.hpp"
 
 namespace model {
@@ -14,8 +15,14 @@ struct process_exit : public model::transition {
   ~process_exit() = default;
 
   status modify(model::mutable_state& s) const override {
-    // We ensure that exiting is never enabled. This ensures that it will never
-    // be explored by any model checking algorithm
+    // Mark the executor exited, like thread_exit does (minus its
+    // RID_MAIN_THREAD restriction, since exit()/abort() can end the process
+    // from any thread). Without this, is_active() keeps reporting true, so
+    // classic_dpor re-selects this same "enabled" transition forever for any
+    // exit code its program_exit_code() > 0 check doesn't already catch
+    // (i.e. exit code 0).
+    using namespace model::objects;
+    s.add_state_for_runner(executor, new thread(thread::exited));
     return status::exists;
   }
 
diff --git a/include/mcmini/real_world/mailbox/runner_mailbox.h b/include/mcmini/real_world/mailbox/runner_mailbox.h
index 8f864b55..d3bd644b 100644
--- a/include/mcmini/real_world/mailbox/runner_mailbox.h
+++ b/include/mcmini/real_world/mailbox/runner_mailbox.h
@@ -8,8 +8,21 @@ extern "C" {
 #include <stdint.h>
 
 typedef struct {
+  // Waited on by the verifier (mcmini), posted by the target thread. The
+  // verifier is never checkpointed, so a plain glibc sem_t is safe here.
   sem_t model_side_sem;
-  sem_t child_side_sem;
+  // Waited on by the target thread, posted by the verifier. A DMTCP-restored
+  // target thread can be genuinely blocked (kernel-level) on this exact
+  // futex word while glibc's own userspace "is anyone really waiting"
+  // bookkeeping is desynced from that -- because this memory gets
+  // reinitialized (see mc_runner_mailbox_init()/_destroy()) before every new
+  // DMTCP-restarted branch, and glibc's NPTL sem_t packs that bookkeeping
+  // into the same memory sem_post() checks to decide whether to skip the
+  // underlying futex(FUTEX_WAKE) syscall. A plain futex word (see
+  // mc_wake_thread()/mc_wait_for_scheduler() in runner_mailbox.c, which
+  // always call FUTEX_WAKE unconditionally) has no such bookkeeping to
+  // desync.
+  uint32_t child_side_sem;
   uint32_t type;
   uint8_t cnts[64];  // TODO: How much space should each thread have to write
                      // payloads?
diff --git a/include/mcmini/real_world/process/dmtcp_process_source.hpp b/include/mcmini/real_world/process/dmtcp_process_source.hpp
index 7e334f75..c9806d9a 100644
--- a/include/mcmini/real_world/process/dmtcp_process_source.hpp
+++ b/include/mcmini/real_world/process/dmtcp_process_source.hpp
@@ -6,7 +6,7 @@
 
 #include "mcmini/defines.h"
 #include "mcmini/forwards.hpp"
-#include "mcmini/real_world/process/dmtcp_coordinator.hpp"
+#include "mcmini/real_world/dmtcp_target.hpp"
 #include "mcmini/real_world/process/local_linux_process.hpp"
 #include "mcmini/real_world/process_source.hpp"
 #include "mcmini/real_world/shm.hpp"
@@ -27,14 +27,12 @@ class dmtcp_process_source : public process_source {
  private:
   std::string ckpt_file;
   dmtcp_target dmtcp_restart_target;
-  dmtcp_coordinator coordinator_target;
 
  private:
   pid_t make_new_branch();
 
  public:
   dmtcp_process_source(const std::string &ckpt_file);
-  virtual ~dmtcp_process_source();
 
  public:
   std::unique_ptr<process> make_new_process() override;
diff --git a/include/mcmini/spy/intercept/interception.h b/include/mcmini/spy/intercept/interception.h
index 105f024f..0ab77d15 100644
--- a/include/mcmini/spy/intercept/interception.h
+++ b/include/mcmini/spy/intercept/interception.h
@@ -29,6 +29,11 @@ int libdmtcp_pthread_create(pthread_t *thread, const pthread_attr_t *attr,
 int pthread_join(pthread_t thread, void**);
 int libpthread_pthread_join(pthread_t thread, void**);
 int libdmtcp_pthread_join(pthread_t thread, void**);
+// TSan-safe (libtsan-bypassing) handle for pthread_timedjoin_np, used by
+// mc_pthread_join's RECORD loop. Calling pthread_timedjoin_np directly resolves
+// to libtsan's interceptor, which trips a thread-registry CHECK. See
+// TSAN-McMini-DMTCP.txt.
+int libpthread_timedjoin_np(pthread_t thread, void**, const struct timespec*);
 
 int libpthread_mutex_init(pthread_mutex_t *, const pthread_mutexattr_t *);
 int libpthread_mutex_lock(pthread_mutex_t *);
diff --git a/src/common/multithreaded_fork.c b/src/common/multithreaded_fork.c
index 7d60a103..1112c954 100644
--- a/src/common/multithreaded_fork.c
+++ b/src/common/multithreaded_fork.c
@@ -177,7 +177,7 @@ pid_t get_tid_from_pthread_descriptor(pthread_t pthread_descriptor) {
   int offset = pthreadDescriptorTidOffset();
   pid_t ctid = *(pid_t*)((char*)(pthread_descriptor) + offset);
 #ifdef DMTCP
-  pid_t virttid = dmtcp_real_to_virtual_pid(ctid);
+  pid_t virttid = dmtcp_pid_real_to_virtual(ctid);
   ctid = (virttid ? virttid : ctid);
 #endif
   return ctid;
@@ -209,7 +209,7 @@ int get_child_threads(int child_threads[]) {
       if (atoi(entry->d_name) != 0) {
         pid_t nexttid = atoi(entry->d_name);
 #ifdef DMTCP
-        pid_t virttid = dmtcp_real_to_virtual_pid(nexttid);
+        pid_t virttid = dmtcp_pid_real_to_virtual(nexttid);
         nexttid = (virttid ? virttid : nexttid);
 #endif
         child_threads[i++] = nexttid;
diff --git a/src/common/runner_mailbox.c b/src/common/runner_mailbox.c
index e11af991..25d9ec57 100644
--- a/src/common/runner_mailbox.c
+++ b/src/common/runner_mailbox.c
@@ -1,22 +1,55 @@
 #include "mcmini/real_world/mailbox/runner_mailbox.h"
 
-#include <stdio.h>
+#include <errno.h>
+#include <linux/futex.h>
+#include <sys/syscall.h>
 #include <unistd.h>
 
-#include "mcmini/lib/log.h"
 #include "mcmini/defines.h"
 #include "mcmini/spy/intercept/interception.h"
 #include "string.h"
 
+// child_side_sem's own raw-futex protocol (see runner_mailbox.h for why it
+// isn't a glibc sem_t): a plain futex word used as a counting semaphore,
+// always waking unconditionally on post, so there's no userspace "is anyone
+// really waiting" bookkeeping to desync.
+static long mc_futex(volatile uint32_t *uaddr, int futex_op, uint32_t val) {
+  return syscall(SYS_futex, uaddr, futex_op, val, NULL, NULL, 0);
+}
+
+static int mc_raw_sem_wait(volatile uint32_t *sem) {
+  while (1) {
+    uint32_t cur = __atomic_load_n(sem, __ATOMIC_SEQ_CST);
+    if (cur > 0) {
+      uint32_t expected = cur;
+      if (__atomic_compare_exchange_n(sem, &expected, cur - 1, 0,
+                                      __ATOMIC_SEQ_CST, __ATOMIC_SEQ_CST)) {
+        return 0;
+      }
+      continue;
+    }
+    errno = 0;
+    long rc = mc_futex(sem, FUTEX_WAIT, 0);
+    if (rc == -1 && errno != EAGAIN && errno != EINTR) {
+      return -1;
+    }
+  }
+}
+
+static int mc_raw_sem_post(volatile uint32_t *sem) {
+  __atomic_fetch_add(sem, 1, __ATOMIC_SEQ_CST);
+  mc_futex(sem, FUTEX_WAKE, 1);
+  return 0;
+}
+
 void mc_runner_mailbox_init(volatile runner_mailbox* r) {
   runner_mailbox_ref ref = (runner_mailbox_ref)(r);
 #ifdef MC_SHARED_LIBRARY
   libpthread_sem_init(&ref->model_side_sem, SEM_FLAG_SHARED, 0);
-  libpthread_sem_init(&ref->child_side_sem, SEM_FLAG_SHARED, 0);
 #else
   sem_init(&ref->model_side_sem, SEM_FLAG_SHARED, 0);
-  sem_init(&ref->child_side_sem, SEM_FLAG_SHARED, 0);
 #endif
+  __atomic_store_n(&ref->child_side_sem, 0, __ATOMIC_SEQ_CST);
   memset(ref->cnts, 0, sizeof(ref->cnts));
 }
 
@@ -24,11 +57,11 @@ void mc_runner_mailbox_destroy(volatile runner_mailbox* r) {
   runner_mailbox_ref ref = (runner_mailbox_ref)(r);
 #ifdef MC_SHARED_LIBRARY
   libpthread_sem_destroy(&ref->model_side_sem);
-  libpthread_sem_destroy(&ref->child_side_sem);
 #else
   sem_destroy(&ref->model_side_sem);
-  sem_destroy(&ref->child_side_sem);
 #endif
+  // child_side_sem is a plain futex word, not a glibc sem_t: nothing to
+  // destroy.
 }
 
 int mc_wait_for_thread(volatile runner_mailbox* r) {
@@ -42,20 +75,12 @@ int mc_wait_for_thread(volatile runner_mailbox* r) {
 
 int mc_wait_for_scheduler(volatile runner_mailbox* r) {
   runner_mailbox_ref ref = (runner_mailbox_ref)(r);
-#ifdef MC_SHARED_LIBRARY
-  return libpthread_sem_wait(&ref->child_side_sem);
-#else
-  return sem_wait(&ref->child_side_sem);
-#endif
+  return mc_raw_sem_wait(&ref->child_side_sem);
 }
 
 int mc_wake_thread(volatile runner_mailbox* r) {
   runner_mailbox_ref ref = (runner_mailbox_ref)(r);
-#ifdef MC_SHARED_LIBRARY
-  return libpthread_sem_post(&ref->child_side_sem);
-#else
-  return sem_post(&ref->child_side_sem);
-#endif
+  return mc_raw_sem_post(&ref->child_side_sem);
 }
 
 int mc_wake_scheduler(volatile runner_mailbox* r) {
diff --git a/src/examples/CMakeLists.txt b/src/examples/CMakeLists.txt
index 5c056b14..9d0c9e24 100644
--- a/src/examples/CMakeLists.txt
+++ b/src/examples/CMakeLists.txt
@@ -4,8 +4,25 @@ add_executable(cv-test cv-test.c)
 add_executable(deadly-embrace deadly-embrace.c)
 add_executable(fifo-example fifo.cpp)
 add_executable(producer-consumer producer-consumer.c)
+add_executable(producer-consumer-park producer-consumer-park.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(deadly-embrace PUBLIC -pthread)
 target_link_libraries(producer-consumer PUBLIC -pthread)
+target_link_libraries(producer-consumer-park PUBLIC -pthread)
+
+# producer-consumer-park.c never calls pthread_join() or pthread_exit() --
+# main returns while both workers are still alive, parked forever on an
+# unposted semaphore (see that file's own comment, modeled on
+# multithreaded-fork-tsan-2.0's test_park.c). No --wrap needed: neither
+# pthread_join nor pthread_cond_wait is ever called here.
+add_executable(producer-consumer-park-tsan producer-consumer-park.c)
+target_compile_options(producer-consumer-park-tsan PUBLIC -fsanitize=thread)
+target_link_options(producer-consumer-park-tsan PUBLIC -fsanitize=thread)
+target_link_libraries(producer-consumer-park-tsan PUBLIC -pthread libmcmini)
+
+add_custom_command(TARGET producer-consumer-park-tsan POST_BUILD
+  COMMAND ${CMAKE_COMMAND} -E copy
+          $<TARGET_FILE:producer-consumer-park-tsan>
+          ${CMAKE_BINARY_DIR}/producer-consumer-park-tsan)
diff --git a/src/examples/producer-consumer-park.c b/src/examples/producer-consumer-park.c
new file mode 100644
index 00000000..67e0c26d
--- /dev/null
+++ b/src/examples/producer-consumer-park.c
@@ -0,0 +1,147 @@
+#include <stdlib.h>
+#include <stdio.h>
+#include <string.h>
+#include <pthread.h>
+#include <semaphore.h>
+#include <time.h>
+#include <unistd.h>
+
+#define MaxItems 1
+#define BufferSize 2
+
+// Unlike sleep(), a busy-wait can't be cut short by DMTCP's own
+// pre-checkpoint signal (which interrupts blocking syscalls, returning
+// early with time remaining) -- needed below so main's own delay reliably
+// lasts the full duration instead of racing main's return/exit() against
+// an in-progress checkpoint write.
+static void busy_wait_seconds(int seconds) {
+    struct timespec start, now;
+    clock_gettime(CLOCK_MONOTONIC, &start);
+    do {
+        clock_gettime(CLOCK_MONOTONIC, &now);
+    } while (now.tv_sec - start.tv_sec < seconds);
+}
+
+// Same as producer-consumer-safe.c, except main never calls pthread_join():
+// each worker signals `done` once its real work finishes, then parks forever
+// on an unposted semaphore, and main returns as soon as both `done`s are
+// posted -- exercising a real, alive-but-parked (never joined/exited) thread
+// still present when the process ends, matching multithreaded-fork-tsan-2.0's
+// test_park.c ("thread resurrection ... without pthread_join/pthread_exit").
+//
+// NOTE: main() returning here (rather than e.g. pthread_exit()) triggers
+// POSIX exit() semantics -- the whole process tears down immediately,
+// including TSan's own exit-time Finalize()/ThreadCount() bookkeeping, which
+// reuses main()'s now-dead stack slots (confirmed live via a gdb hardware
+// watchpoint: the exact address that held prod_ids[0] gets overwritten by
+// TSan's internal "alive thread count" a moment later). This can show up as
+// an apparently-garbled producer/consumer id in RECORD-mode's printf output
+// on a rare timing -- harmless (pure RECORD-mode artifact, before any
+// checkpoint/restart), not a libmcmini/DMTCP bug, and not the subject of
+// this file's actual test (multithreaded_fork's recreated-but-unjoined
+// thread handling under --multithreaded-fork restart).
+sem_t empty;
+sem_t full;
+sem_t producer_done;
+sem_t consumer_done;
+sem_t park; // never posted
+int in = 0;
+int out = 0;
+int buffer[BufferSize];
+pthread_mutex_t mutex;
+int DEBUG;
+
+static void sem_wait_retry(sem_t *s) { while (sem_wait(s) != 0) /* EINTR */; }
+
+void *producer(void *pno)
+{
+    int item;
+    for(int i = 0; i < MaxItems; i++) {
+        sleep(3);
+        item = rand(); // Produce an random item
+        sem_wait(&empty);
+        pthread_mutex_lock(&mutex);
+        buffer[in] = item;
+        if (DEBUG) {
+          printf("Producer %d: Insert Item %d at %d\n",
+                 *((int *)pno),buffer[in],in);
+        }
+        in = (in+1)%BufferSize;
+        pthread_mutex_unlock(&mutex);
+        sem_post(&full);
+    }
+    sem_post(&producer_done);
+    sem_wait_retry(&park); // park forever; never exit/join
+    return NULL;
+}
+
+void *consumer(void *cno)
+{
+    for(int i = 0; i < MaxItems; i++) {
+        sleep(3);
+        sem_wait(&full);
+        pthread_mutex_lock(&mutex);
+        int item = buffer[out];
+        if (DEBUG) {
+          printf("Consumer %d: Remove Item %d from %d\n",
+                 *((int *)cno),item, out);
+        }
+        out = (out+1)%BufferSize;
+        pthread_mutex_unlock(&mutex);
+        sem_post(&empty);
+    }
+    sem_post(&consumer_done);
+    sem_wait_retry(&park); // park forever; never exit/join
+    return NULL;
+}
+
+int main(int argc, char* argv[])
+{
+    int NUM_PRODUCERS = 1;
+    int NUM_CONSUMERS = 1;
+    DEBUG = 1;
+
+    pthread_t pro[NUM_PRODUCERS],con[NUM_CONSUMERS];
+
+    pthread_mutex_init(&mutex, NULL);
+    sem_init(&empty,0,BufferSize);
+    sem_init(&full,0,0);
+    sem_init(&producer_done,0,0);
+    sem_init(&consumer_done,0,0);
+    sem_init(&park,0,0);
+
+    int prod_ids[NUM_PRODUCERS];
+    int cons_ids[NUM_CONSUMERS];
+
+    for(int i = 0; i < NUM_PRODUCERS; i++) {
+        prod_ids[i] = i+1;
+        pthread_create(&pro[i], NULL, producer, (void *)&prod_ids[i]);
+    }
+    for(int i = 0; i < NUM_CONSUMERS; i++) {
+        cons_ids[i] = i+1;
+        pthread_create(&con[i], NULL, consumer, (void *)&cons_ids[i]);
+    }
+
+    for(int i = 0; i < NUM_PRODUCERS; i++) {
+        sem_wait(&producer_done);
+    }
+    for(int i = 0; i < NUM_CONSUMERS; i++) {
+        sem_wait(&consumer_done);
+    }
+    // Widen the window where both workers are safely parked (on `park`)
+    // but main hasn't yet returned/exited -- gives a checkpoint interval
+    // (mcmini -i N) a reliable target to land on, instead of racing main's
+    // own exit() against the workers' last bit of real work (see this
+    // file's top-of-file comment on the TSan-Finalize()/stack-reuse
+    // artifact that showed up when that race was too tight).
+    busy_wait_seconds(10);
+    // Deliberately no pthread_join(): producer/consumer are still alive,
+    // parked on `park`, when the process ends.
+
+    // Plain return, deliberately NOT an explicit exit(0) call: this is now
+    // a live regression test for interception.c's __libc_start_main hook,
+    // which runs mc_transparent_exit() after main() returns however it
+    // returns, catching exactly this case -- see that file for why a plain
+    // return used to bypass every exit()/_exit() interposition technique.
+    return 0;
+}
diff --git a/src/lib/dmtcp-callback.c b/src/lib/dmtcp-callback.c
index 7438c57a..cc67884c 100644
--- a/src/lib/dmtcp-callback.c
+++ b/src/lib/dmtcp-callback.c
@@ -1,6 +1,5 @@
 #define _GNU_SOURCE
 #include <assert.h>
-#include <dirent.h>
 #include <errno.h>
 #include <fcntl.h>  // man 2 open
 #include <pthread.h>
@@ -42,8 +41,6 @@ struct threadinfo {
   // tlsAddr only used in __aarch64__ and __riscv
   // In fact, __riscv has the address in a normal register, restored w/ context.
   unsigned long int tlsAddr;
-  // The kernel has a process-wide sigmask, and also a per-thread sigmask.
-  sigset_t thread_sigmask;
   // glibc:pthread_create and pthread_self use this, but not the clone call:
   pthread_t pthread_descriptor;
 } threadInfos[1000];
@@ -125,23 +122,19 @@ static void saveThreadStateBeforeFork(struct threadinfo* threadInfo) {
   threadInfo->pthread_descriptor = pthread_self();
   getTLSPointer(threadInfo);
 
-  // FIXME:  Add func fo get/set signals in child thread of child process.
-  //         and restore thread sigmask sfter setcontext.
-  pthread_sigmask(SIG_BLOCK, NULL, &threadInfo->thread_sigmask);
-  sigset_t sigtest;
-  pthread_sigmask(SIG_BLOCK, NULL, &sigtest);
-  sigdelset(&sigtest, SIG_MULTITHREADED_FORK);
-  if (! sigisemptyset(&sigtest)) {
-    fprintf(stderr, "PID %d: multithreaded_fork() not yet implemented"
-                    " for non-empty thread signaks\n", getpid());
-    libc_abort();
-  }
+  // No manual signal-mask save/restore needed: getcontext()/setcontext()
+  // already save/restore the blocked-signal set via ucontext_t's uc_sigmask,
+  // even when setcontext() resumes on a brand-new clone()'d OS thread (see
+  // child_setcontext_fast() below).
 }
 
 static int child_setcontext_fast(void *arg) {
   struct threadinfo* threadInfo = arg;
   setTLSPointer(threadInfo);
   patchThreadDescriptor(threadInfo->pthread_descriptor);
+  // Does not return: jumps to the getcontext() call site in
+  // thread_handle_after_dmtcp_restart(), restoring uc_sigmask (see
+  // saveThreadStateBeforeFork() above) along with the rest of the context.
   setcontext(&(threadInfo->context));
   return 0; // not reached
 }
@@ -191,39 +184,8 @@ pid_t fast_multithreaded_fork(void) {
    *  ret = INLINE_SYSCALL_CALL (clone, flags, 0, NULL, ctid, 0);
    *}
    *********************************************************************/
-#if 1
   pid_t _Fork();
   int childpid = _Fork();
-#else
-  // NOT YET FULLY DEVELOPED:
-  int flags = CLONE_CHILD_SETTID | CLONE_CHILD_CLEARTID | SIGCHLD;
-  int childpid;
-// syscall(SYS_clone, ...);
-// stack must be NULL
-// https://stackoverflow.com/questions/2898579/clone-equivalent-of-fork
-//   But that says to use only SIGCHLD for flags, and glibc uses the above.
-//   But it's okay, since we're setting ctid and tls to NULL.
-// FIXME:  If we're going to set the last 3 args to NULL, who cares in what order they're found!
-# ifdef __x86_64__
-           long clone(unsigned long flags, void *stack,
-                      int *parent_tid, int *child_tid,
-                      unsigned long tls);
-# elif defined(__aarch64__)
-           long clone(unsigned long flags, void *stack,
-                     int *parent_tid, unsigned long tls,
-                     int *child_tid);
-# elif defined(__riscv)
-#  error Unimplemented CPU architecture
-https://github.com/bminor/glibc/blob/master/sysdeps/unix/sysv/linux/riscv/clone.S
-int clone(int (*fn)(void *arg), void *child_stack, int flags, void *arg,
-	     void *parent_tidptr, void *tls, void *child_tidptr) */
-	/* The syscall expects the args to be in different slots.  */
-	mv		a0,a2
-	mv		a2,a4
-	mv		a3,a5
-	mv		a4,a6
-# endif
-#endif
   if (childpid == 0) { // child process
     restart_child_threads_fast();
   }
@@ -321,23 +283,27 @@ static void *template_thread(void *unused) {
   // to ensure a stable recorded state is pointless: we're not going to read it
   // anyway! This is an only a potential optimization for later though.
 
+  // Counting via a live /proc/self/task scan is a TOCTOU race: DMTCP
+  // recreates checkpointed threads asynchronously via clone(), so a scan
+  // that runs before it has finished recreating all of them undercounts,
+  // and this barrier then releases before every thread has actually
+  // restarted (confirmed empirically: one thread's own restart-completion
+  // signal can arrive after this barrier already declared a "consistent
+  // state").
+  //
+  // head_record_mode instead gives an exact, race-free count: it only ever
+  // gets THREAD entries for genuine target threads (the template thread and
+  // the checkpoint thread never go through libmcmini's wrapped
+  // pthread_create(), so neither is ever recorded here), and -- since a
+  // DMTCP checkpoint is a full memory snapshot -- this list is preserved
+  // exactly as it was at record time across every restart, with no
+  // dependence on restart-time scheduling.
   int thread_count = 0;
-  struct dirent *entry;
-  DIR *dp = opendir("/proc/self/task");
-  if (dp == NULL) {
-    perror("opendir");
-    mc_exit(EXIT_FAILURE);
-  }
-
-  while ((entry = readdir(dp)))
-    if (strcmp(entry->d_name, ".") != 0 && strcmp(entry->d_name, "..") != 0)
+  for (rec_list *entry = head_record_mode; entry != NULL; entry = entry->next) {
+    if (entry->vo.type == THREAD && entry->vo.thrd_state.status == ALIVE) {
       thread_count++;
-
-  // We don't want to count the template thread nor
-  // the checkpoint thread, but these will appear in
-  // `/proc/self/tasks`
-  thread_count -= 2;
-  closedir(dp);
+    }
+  }
   log_debug(
       "There are %d threads... waiting for them to get into a consistent "
       "state...\n",
@@ -579,6 +545,14 @@ static void presuspend_eventHook(DmtcpEvent_t event, DmtcpEventData_t *data) {
       } else {
         set_current_mode(DMTCP_RESTART_INTO_BRANCH);
         log_debug("`MCMINI_TEMPLATE_LOOP` was not set at restart-time\n");
+
+        // A DMTCP_RESTART_INTO_BRANCH process explores exactly one trace,
+        // then this process is discarded -- it will never legitimately be
+        // asked to checkpoint again. Left alone, the checkpoint thread would
+        // resume its normal sleep-checkpoint-resume loop and block forever
+        // waiting for a checkpoint request from this restart's (one-shot,
+        // otherwise idle) coordinator.
+        dmtcp_skip_post_restart_checkpoint_loop();
       }
 
       // During record mode, the shared memory
diff --git a/src/lib/interception.c b/src/lib/interception.c
index 6d0b66f6..0d29e955 100644
--- a/src/lib/interception.c
+++ b/src/lib/interception.c
@@ -16,6 +16,7 @@ typeof(&pthread_create) libpthread_pthread_create_ptr;
 typeof(&pthread_create) libdmtcp_pthread_create_ptr;
 typeof(&pthread_join) libpthread_pthread_join_ptr;
 typeof(&pthread_join) libdmtcp_pthread_join_ptr;
+typeof(&pthread_timedjoin_np) libpthread_timedjoin_np_ptr;
 typeof(&pthread_mutex_init) pthread_mutex_init_ptr;
 typeof(&pthread_mutex_lock) pthread_mutex_lock_ptr;
 typeof(&pthread_mutex_trylock) pthread_mutex_trylock_ptr;
@@ -69,6 +70,7 @@ void mc_load_intercepted_pthread_functions(void) {
 
   libpthread_pthread_create_ptr = dlsym(libpthread_handle, "pthread_create");
   libpthread_pthread_join_ptr = dlsym(libpthread_handle, "pthread_join");
+  libpthread_timedjoin_np_ptr = dlsym(libpthread_handle, "pthread_timedjoin_np");
   pthread_mutex_init_ptr = dlsym(libpthread_handle, "pthread_mutex_init");
   pthread_mutex_lock_ptr = dlsym(libpthread_handle, "pthread_mutex_lock");
   pthread_mutex_trylock_ptr = dlsym(libpthread_handle, "pthread_mutex_trylock");
@@ -228,6 +230,11 @@ int libpthread_pthread_join(pthread_t thread, void **rv) {
   libmcmini_init();
   return (*libpthread_pthread_join_ptr)(thread, rv);
 }
+int libpthread_timedjoin_np(pthread_t thread, void **rv,
+                            const struct timespec *abstime) {
+  libmcmini_init();
+  return (*libpthread_timedjoin_np_ptr)(thread, rv, abstime);
+}
 int libdmtcp_pthread_join(pthread_t thread, void **rv) {
   libmcmini_init();
   return (*libdmtcp_pthread_join_ptr)(thread, rv);
@@ -301,3 +308,44 @@ int libpthread_sem_wait_loop(sem_t *sem) {
     rc = libpthread_sem_wait(sem);
   return rc;
 }
+
+// __libc_start_main() is called from _start (crt1.o), not glibc-internal
+// code, so unlike exit()/_exit() -- whose implicit post-main() call chain
+// resolves through glibc-internal hidden aliases that bypass any public-
+// symbol interposition (see test/tsan_support/test_implicit_exit_interposition.c)
+// -- this call site goes through ordinary dynamic symbol resolution and can
+// be intercepted like any other public symbol. Used to guarantee
+// mc_transparent_exit()'s exit-transition/restart-quiescence handling runs
+// after the target's main() returns, even when it returns plainly
+// (`return N;`) rather than calling exit()/pthread_exit() explicitly --
+// verified in test/tsan_support/test_libc_start_main_hook.c.
+typedef int (*main_fn)(int, char **, char **);
+typedef int (*libc_start_main_fn)(main_fn, int, char **, void (*)(void),
+                                  void (*)(void), void (*)(void), void *);
+
+static main_fn real_main;
+
+static int wrapped_main(int argc, char **argv, char **envp) {
+  int rc = real_main(argc, argv, envp);
+  // libmcmini_init() itself is safe to call any time after main() has run
+  // (pthreads are certainly initialized by now), unlike at the top of
+  // __libc_start_main() below, which runs before glibc's own internal
+  // pthread-subsystem setup and must stay free of any pthread_once/mutex
+  // use until the real __libc_start_main() has had a chance to run.
+  libmcmini_init();
+  // Route a plain return from main() through the exact same model-checking
+  // exit protocol as an explicit exit(rc) call: mc_transparent_exit()
+  // itself performs the real, final process termination in every mode
+  // (see wrappers.c), so this call never returns.
+  mc_transparent_exit(rc);
+}
+
+int __libc_start_main(main_fn main, int argc, char **argv, void (*init)(void),
+                      void (*fini)(void), void (*rtld_fini)(void),
+                      void *stack_end) {
+  real_main = main;
+  libc_start_main_fn real_start_main =
+      (libc_start_main_fn)dlsym(RTLD_NEXT, "__libc_start_main");
+  return real_start_main(wrapped_main, argc, argv, init, fini, rtld_fini,
+                         stack_end);
+}
diff --git a/src/lib/wrappers.c b/src/lib/wrappers.c
index a385c012..a6a1373d 100644
--- a/src/lib/wrappers.c
+++ b/src/lib/wrappers.c
@@ -18,6 +18,11 @@
 typedef struct pthread_map {
     pthread_t thread;
     runner_id_t value;
+    // Posted by whichever thread eventually calls pthread_join() on this
+    // one (mc_pthread_join()'s TARGET_BRANCH case), waited on by this
+    // thread itself before it may really terminate (mc_exit_thread_in_child()).
+    // See the two functions for the full rationale.
+    sem_t exit_permission_sem;
     struct pthread_map *next;
 } pthread_map_t;
 
@@ -29,6 +34,7 @@ void insert_pthread_map(pthread_t t, runner_id_t v) {
     pthread_map_t *n = malloc(sizeof *n);
     n->thread = t;
     n->value = v;
+    libpthread_sem_init(&n->exit_permission_sem, 0, 0);
     n->next = head;
     head = n;
     pthread_rwlock_unlock(&pthread_map_lock);
@@ -39,12 +45,27 @@ runner_id_t search_pthread_map(pthread_t t) {
     pthread_map_t *cur = head;
     while (cur) {
         if (pthread_equal(cur->thread, t)) {
-            return cur->value;
+            break;
         }
         cur = cur->next;
     }
     pthread_rwlock_unlock(&pthread_map_lock);
-    return RID_INVALID;
+    return cur == NULL ? RID_INVALID : cur->value;
+}
+
+// Returns the given thread's own exit_permission_sem (see pthread_map_t),
+// or NULL if the thread is not (yet) registered.
+sem_t *find_exit_permission_sem(pthread_t t) {
+  pthread_rwlock_rdlock(&pthread_map_lock);
+  pthread_map_t *cur = head;
+  while (cur) {
+    if (pthread_equal(cur->thread, t)) {
+      break;
+    }
+    cur = cur->next;
+  }
+  pthread_rwlock_unlock(&pthread_map_lock);
+  return cur == NULL ? NULL : &cur->exit_permission_sem;
 }
 
 
@@ -335,7 +356,16 @@ void mc_exit_thread_in_child(void) {
   thread_get_mailbox()->type = THREAD_EXIT_TYPE;
   thread_wake_scheduler_and_wait();
   thread_awake_scheduler_for_thread_finish_transition();
-  thread_block_indefinitely();
+
+  // Wait for whichever thread eventually calls pthread_join() on this one
+  // (see mc_pthread_join()'s TARGET_BRANCH case) to grant permission before
+  // this thread is allowed to really terminate. This keeps this thread's
+  // pthread_t/tid valid for exactly as long as a real, unjoined POSIX
+  // thread's would be -- no longer -- rather than parking it forever
+  // regardless of whether anyone ever joins it.
+  sem_t *exit_permission = find_exit_permission_sem(pthread_self());
+  assert(exit_permission != NULL);
+  libpthread_sem_wait(exit_permission);
 }
 
 void mc_exit_main_thread_in_child(void) {
@@ -389,7 +419,14 @@ MCMINI_NO_RETURN void mc_transparent_exit(int status) {
       volatile runner_mailbox *mb = thread_get_mailbox();
       mb->type = PROCESS_EXIT_TYPE;
       memcpy_v(mb->cnts, &status, sizeof(status));
-      thread_await_scheduler();
+      // Unlike every other wrapper's TARGET_BRANCH* case, this used to call
+      // the wait-only thread_await_scheduler(), which never posts
+      // model_side_sem. That's harmless for a thread that fell through from
+      // DMTCP_RESTART_INTO_BRANCH/TEMPLATE above (thread_handle_after_dmtcp_restart()
+      // already posted it), but a thread already in TARGET_BRANCH_AFTER_RESTART
+      // (e.g. main(), calling exit() for the first time since restart) jumps
+      // straight here and hangs the coordinator's execute_runner() forever.
+      thread_wake_scheduler_and_wait();
 
       // After "exiting", don't actually exit yet:
       // the model checker will prevent the process
@@ -397,7 +434,7 @@ MCMINI_NO_RETURN void mc_transparent_exit(int status) {
       // branch as "useless" since at this point
       mb->type = PROCESS_EXIT_TYPE;
       memcpy_v(mb->cnts, &status, sizeof(status));
-      thread_await_scheduler();
+      thread_wake_scheduler_and_wait();
     }
     default: {
       libc_exit(status);
@@ -726,7 +763,10 @@ int mc_pthread_join(pthread_t t, void **rv) {
 
       struct timespec time = {.tv_sec = 2, .tv_nsec = 0};
       while (1) {
-        int rc = pthread_timedjoin_np(t, rv, &time);
+        // Use the libtsan-bypassing handle: a direct pthread_timedjoin_np would
+        // hit libtsan's interceptor and trip its thread-registry CHECK under
+        // DMTCP. See TSAN-McMini-DMTCP.txt.
+        int rc = libpthread_timedjoin_np(t, rv, &time);
         if (rc == 0) {  // Join succeeded
           libpthread_mutex_lock(&rec_list_lock);
           thread_record->vo.thrd_state.status = EXITED;
@@ -769,7 +809,16 @@ int mc_pthread_join(pthread_t t, void **rv) {
       memcpy_v(thread_get_mailbox()->cnts, &rid, sizeof(runner_id_t));
       thread_get_mailbox()->type = THREAD_JOIN_TYPE;
       thread_wake_scheduler_and_wait();
-      return 0;
+
+      // Grant the target thread permission to really terminate now that
+      // it's been joined (see mc_exit_thread_in_child()), then perform a
+      // genuine join, so its OS thread actually dies -- and *rv is
+      // genuinely populated -- before we return, instead of only
+      // simulating success at the model level.
+      sem_t *exit_permission = find_exit_permission_sem(t);
+      assert(exit_permission != NULL);
+      libpthread_sem_post(exit_permission);
+      return libpthread_pthread_join(t, rv);
     }
     default: {
       libc_abort();
@@ -963,7 +1012,18 @@ int mc_pthread_cond_wait(pthread_cond_t *cond, pthread_mutex_t *mutex) {
       mb->type = COND_WAIT_TYPE;
       memcpy_v(mb->cnts, &cond, sizeof(cond));
       memcpy_v(mb->cnts + sizeof(cond), &mutex, sizeof(mutex));
-      thread_handle_after_dmtcp_restart();
+      // thread_handle_after_dmtcp_restart() (used for the COND_ENQUEUE_TYPE
+      // round above) is a one-time-per-thread restart check-in: it captures
+      // a getcontext() snapshot and posts the quiescence barrier that the
+      // background template thread waits on exactly once per real thread. By
+      // the time this second round runs, that barrier has already released
+      // and set mode to TARGET_BRANCH_AFTER_RESTART, so a second call falls
+      // into thread_handle_after_dmtcp_restart()'s `default: libc_abort()`
+      // (its mode_on_entry no longer matches DMTCP_RESTART_INTO_BRANCH/
+      // TEMPLATE) -- confirmed live via dmesg showing a SIGABRT here. Use the
+      // ordinary wake+wait call instead, matching every other wrapper's
+      // second-and-later round with the coordinator.
+      thread_wake_scheduler_and_wait();
       libpthread_mutex_lock(mutex);
       return 0;
     }
diff --git a/src/mcmini/mcmini.cpp b/src/mcmini/mcmini.cpp
index 025c28e3..05b41a8b 100644
--- a/src/mcmini/mcmini.cpp
+++ b/src/mcmini/mcmini.cpp
@@ -142,14 +142,64 @@ void found_abnormal_termination(
   for (const auto& t : program_model.get_trace()) {
     ss << "thread " << t->get_executor() << ": " << t->to_string() << "\n";
   }
+  // `ub.culprit` may not have a pending transition in the model's current
+  // view: this callback can also fire for a termination_error raised while
+  // `coordinator::return_to_depth()` is replaying already-recorded history
+  // against a freshly restarted process, and by the replay's target depth
+  // the culprit thread may already have exited in the model.
   const transition* terminator =
       program_model.get_pending_transition_for(ub.culprit);
-  ss << "thread " << terminator->get_executor() << ": "
-     << terminator->to_string() << "\n";
+  if (terminator != nullptr) {
+    ss << "thread " << terminator->get_executor() << ": "
+       << terminator->to_string() << "\n";
+  } else {
+    ss << "thread " << ub.culprit << ": (no longer pending)\n";
+  }
+
+  ss << "\nNEXT THREAD OPERATIONS\n";
+  for (const auto& tpair : program_model.get_pending_transitions()) {
+    if (terminator != nullptr && tpair.first == terminator->get_executor()) {
+      ss << "thread " << tpair.first << ": executing"
+         << "\n";
+    } else {
+      ss << "thread " << tpair.first << ": " << tpair.second->to_string()
+         << "\n";
+    }
+  }
+  ss << stats.total_transitions + 1 << " total transitions executed"
+     << "\n";
+  std::cout << ss.str();
+  std::cout.flush();
+}
+
+void found_nonzero_exit_code(
+    const coordinator& c, const stats& stats,
+    const real_world::process::nonzero_exit_code_error& nzec) {
+  std::cerr << "NONZERO EXIT CODE (" << nzec.exit_code << "):\n"
+            << nzec.what() << std::endl;
+
+  std::stringstream ss;
+  const auto& program_model = c.get_current_program_model();
+  ss << "TRACE " << stats.trace_id << "\n";
+  for (const auto& t : program_model.get_trace()) {
+    ss << "thread " << t->get_executor() << ": " << t->to_string() << "\n";
+  }
+  // See found_abnormal_termination()'s identical comment: `nzec.culprit` may
+  // no longer have a pending transition in the model's current view if this
+  // fired while `coordinator::return_to_depth()` was replaying history.
+  const transition* culprit_transition =
+      program_model.get_pending_transition_for(nzec.culprit);
+  if (culprit_transition != nullptr) {
+    ss << "thread " << culprit_transition->get_executor() << ": "
+       << culprit_transition->to_string() << "\n";
+  } else {
+    ss << "thread " << nzec.culprit << ": (no longer pending)\n";
+  }
 
   ss << "\nNEXT THREAD OPERATIONS\n";
   for (const auto& tpair : program_model.get_pending_transitions()) {
-    if (tpair.first == terminator->get_executor()) {
+    if (culprit_transition != nullptr &&
+        tpair.first == culprit_transition->get_executor()) {
       ss << "thread " << tpair.first << ": executing"
          << "\n";
     } else {
@@ -195,6 +245,7 @@ void do_model_checking(const config& config) {
   c.deadlock = &found_deadlock;
   c.undefined_behavior = &found_undefined_behavior;
   c.abnormal_termination = &found_abnormal_termination;
+  c.nonzero_exit_code = &found_nonzero_exit_code;
   classic_dpor_checker.verify_using(coordinator, c);
   std::cout << "Model checking completed!" << std::endl;
 }
@@ -319,6 +370,7 @@ void do_model_checking_from_dmtcp_ckpt_file(const config& config) {
   c.undefined_behavior = &found_undefined_behavior;
   c.deadlock = &found_deadlock;
   c.abnormal_termination = &found_abnormal_termination;
+  c.nonzero_exit_code = &found_nonzero_exit_code;
   classic_dpor_checker.verify_using(coordinator, c);
   std::cerr << "Deep debugging completed!" << std::endl;
 }
diff --git a/src/mcmini/model/transitions/mutex.cpp b/src/mcmini/model/transitions/mutex.cpp
index 1757a7e7..72cd074d 100644
--- a/src/mcmini/model/transitions/mutex.cpp
+++ b/src/mcmini/model/transitions/mutex.cpp
@@ -14,7 +14,8 @@ model::transition* mutex_init_callback(runner_id_t p,
 
   // Locate the corresponding model of this object
   if (!m.contains(remote_mut))
-    m.observe_object(remote_mut, new mutex(mutex::state::uninitialized));
+    m.observe_object(remote_mut,
+                     new mutex(mutex::state::uninitialized, remote_mut));
 
   state::objid_t const mut = m.get_model_of_object(remote_mut);
   return new transitions::mutex_init(p, mut);
diff --git a/src/mcmini/model_checking/algorithms/classic_dpor.cpp b/src/mcmini/model_checking/algorithms/classic_dpor.cpp
index 2504f213..d9dbde56 100644
--- a/src/mcmini/model_checking/algorithms/classic_dpor.cpp
+++ b/src/mcmini/model_checking/algorithms/classic_dpor.cpp
@@ -197,7 +197,22 @@ void classic_dpor::verify_using(coordinator &coordinator,
       // backtracking.
       log_debug(dpor_logger)
           << "Backtracking to depth `" << (dpor_stack.size() - 1) << "`";
-      coordinator.return_to_depth(dpor_stack.size() - 1);
+      try {
+        coordinator.return_to_depth(dpor_stack.size() - 1);
+      } catch (const real_world::process::termination_error &te) {
+        // The process spawned to replay history up to this depth (see
+        // `coordinator::return_to_depth()`) died before the replay
+        // finished. Report it the same way a termination during forward
+        // exploration is reported, rather than letting it escape
+        // unhandled all the way out of `verify_using()`.
+        if (callbacks.abnormal_termination)
+          callbacks.abnormal_termination(coordinator, model_checking_stats, te);
+        return;
+      } catch (const real_world::process::nonzero_exit_code_error &nzec) {
+        if (callbacks.nonzero_exit_code)
+          callbacks.nonzero_exit_code(coordinator, model_checking_stats, nzec);
+        return;
+      }
       log_debug(dpor_logger) << "Finished backtracking to depth `"
                              << (dpor_stack.size() - 1) << "`";
       model_checking_stats.trace_id++;
diff --git a/src/mcmini/real_world/dmtcp_process_source.cpp b/src/mcmini/real_world/dmtcp_process_source.cpp
index 89b79dff..268d2dbe 100644
--- a/src/mcmini/real_world/dmtcp_process_source.cpp
+++ b/src/mcmini/real_world/dmtcp_process_source.cpp
@@ -66,11 +66,3 @@ std::unique_ptr<process> dmtcp_process_source::make_new_process() {
   // assert(tstruct->cpid == target_branch_pid);
   return extensions::make_unique<local_linux_process>(target_branch_pid);
 }
-
-dmtcp_process_source::~dmtcp_process_source() {
-  target dmtcp_cleanup(
-      "dmtcp_command",
-      {"-q", "--port", std::to_string(this->coordinator_target.get_port())});
-  dmtcp_cleanup.set_quiet(true);
-  dmtcp_cleanup.launch_and_wait();
-}
diff --git a/src/mcmini/real_world/local_linux_process.cpp b/src/mcmini/real_world/local_linux_process.cpp
index 75c46036..c784a7f8 100644
--- a/src/mcmini/real_world/local_linux_process.cpp
+++ b/src/mcmini/real_world/local_linux_process.cpp
@@ -2,6 +2,7 @@
 
 #include <errno.h>
 #include <signal.h>
+#include <sys/wait.h>
 
 #include <atomic>
 #include <cstring>
@@ -52,6 +53,29 @@ local_linux_process::~local_linux_process() {
       } else {
         log_error(process_logger) << "Error: " << strerror(errno);
       }
+    } else {
+      // This death is expected and already fully handled (we just reaped
+      // it above): consume the SIGCHLD it generated, so it doesn't linger in
+      // signal_tracker's counter. Otherwise the next process this class
+      // creates (see coordinator::return_to_depth()/assign_new_process_handle(),
+      // which destroys the old handle immediately before creating a new
+      // one) would see that leftover count on its own first execute_runner()
+      // call and wrongly conclude *it* had just died, even though it's
+      // still alive and simply hasn't responded yet.
+      signal_tracker::instance().try_consume_signal(SIGCHLD);
+
+      // The process we just killed may itself have left behind other
+      // now-orphaned descendants (e.g. its own private DMTCP coordinator,
+      // spawned by `dmtcp_restart --new-coordinator`) that die/reparent to
+      // us -- as the PR_SET_CHILD_SUBREAPER subreaper -- around the same
+      // time, generating their own SIGCHLDs. signal_tracker's counter isn't
+      // tied to a specific pid, so drain every zombie that's already
+      // reapable right now (non-blocking: this must never wait on a
+      // descendant that hasn't died yet) and consume one signal per reap,
+      // so none of them linger to be misattributed later either.
+      while (waitpid(-1, &status, WNOHANG) > 0) {
+        signal_tracker::instance().try_consume_signal(SIGCHLD);
+      }
     }
   }
 }
@@ -83,40 +107,60 @@ volatile runner_mailbox *local_linux_process::execute_runner(runner_id_t id) {
   // TODO: The template process will also send a SIGCHLD if it dies
   // unexpectedly. Because we don't expect the template process to die, this is
   // OK for now, but should be handled in the future.
-  errno = 0;
-  signal_tracker::sig_semwait((sem_t *)&rmb->model_side_sem);
-  if (signal_tracker::instance().try_consume_signal(SIGCHLD)) {
-    // TODO: Get the true failure status from the template process via
-    // e.g. shared memory.
-    throw process::termination_error(SIGTERM, id,
-                                     "Process terminated abnormally.");
-    // // TODO: Double check that this
-    // // is the correct process that sent
-    // // the SIGCHILD using WNOHANG.
-
-    // // `PR_SET_CHILD_SUBREAPER` enables us to wait on
-    // // this grandchild.
-    // int status;
-    // int rc = waitpid(this->pid, &status, 0);
-    // if (rc == -1) {
-    //   throw process::execution_error(
-    //       "Error attempting to determine the failure causing the child
-    //       process " "to abnormally exit (or possibly an internal error of
-    //       McMini)." + std::string(strerror(errno)));
-    // } else {
-    //   if (WIFEXITED(status)) {
-    //     int exit_code = WEXITSTATUS(status);
-    //     throw process::nonzero_exit_code_error(
-    //         exit_code, "Process terminated with a non-zero exit code.");
-    //   } else if (WIFSIGNALED(status)) {
-    //     int signo = WTERMSIG(status);
-    //     throw process::termination_error(signo,
-    //                                      "Process terminated abnormally.");
-    //   } else {
-    //     throw process::execution_error(
-    //         "SIGSTOP/SIGCONT in branch processes is not yet supported.");
-    //   }
-    // }
+  while (true) {
+    errno = 0;
+    signal_tracker::sig_semwait((sem_t *)&rmb->model_side_sem);
+    if (!signal_tracker::instance().try_consume_signal(SIGCHLD)) {
+      break;
+    }
+    // signal_tracker's SIGCHLD count is process-wide, not tied to a pid, so
+    // a pending count doesn't necessarily mean *this->pid* is the one that
+    // died -- some other descendant (e.g. a previous branch's own private
+    // DMTCP coordinator) may have generated it instead. Confirm with a
+    // non-blocking waitpid() specifically on this->pid (PR_SET_CHILD_SUBREAPER,
+    // set in target::prepare_mcmini_targets(), lets us wait on it even though
+    // it isn't a direct child): if it hasn't actually changed state, this
+    // SIGCHLD wasn't ours, so just resume waiting instead of misreporting a
+    // termination that didn't happen.
+    int status;
+    int rc = waitpid(this->pid, &status, WNOHANG);
+    if (rc == 0) {
+      continue;
+    }
+    if (rc == -1) {
+      throw process::execution_error(
+          "Error attempting to determine the failure causing the child "
+          "process to abnormally exit (or possibly an internal error of "
+          "McMini): " + std::string(strerror(errno)));
+    } else if (WIFEXITED(status)) {
+      const int exit_code = WEXITSTATUS(status);
+      if (exit_code != 0) {
+        throw process::nonzero_exit_code_error(
+            exit_code, id, "The program exited with code " + std::to_string(exit_code));
+      }
+      // A clean (code 0) exit reaching this SIGCHLD-based detection path is
+      // not the same situation nonzero_exit_code_error reports: that
+      // exception means the *target program* exited abnormally, a bug for
+      // the user to fix. Here, the whole process fully terminated on its
+      // own while this runner still had a transition pending on it -- i.e.
+      // it bypassed the model-driven exit protocol (mc_transparent_exit(),
+      // fixed in commit 6bed56a, deliberately keeps the process alive
+      // across both of its mailbox rounds before ever calling the real
+      // exit(2)) rather than checking in normally. That is a McMini-side
+      // protocol violation to investigate, not a target-program bug.
+      throw process::execution_error(
+          "Runner " + std::to_string(id) +
+          "'s process exited normally (code 0) while a transition was "
+          "still pending on it, bypassing the model-driven exit protocol.");
+    } else if (WIFSIGNALED(status)) {
+      throw process::termination_error(
+          WTERMSIG(status), id,
+          "Process terminated abnormally by signal " +
+              std::to_string(WTERMSIG(status)));
+    } else {
+      throw process::execution_error(
+          "SIGSTOP/SIGCONT in branch processes is not yet supported.");
+    }
   }
   return rmb;
 }