Route pthread_create via RTLD_NEXT so TSan targets don't crash#5
Open
gc00 wants to merge 3 commits into
Open
Conversation
A mutex declared with PTHREAD_MUTEX_INITIALIZER never flows through the pthread_mutex_init wrapper, so the model never observes it being initialized. Previously mutex_lock_callback threw "uninitialized mutex" in that case (the `// TODO: add code from Gene's PR here` placeholder). Port the original McMini behavior: on a lock of a mutex the model has not seen, read the target's memory via process_vm_readv and compare against PTHREAD_MUTEX_INITIALIZER. On a match, lazily register the mutex as initialized+unlocked; otherwise report undefined behavior. Unlock is left reporting undefined behavior for an unknown mutex (faithful to the original, which does not lazily register on unlock). - model_to_system_map: expose get_target_pid() so callbacks can read the live target's memory. - coordinator: implement get_target_pid() from the current process handle. - mutex.cpp: add the process_vm_readv validation helper and port the lock callback; fix the mis-copied unlock message. A FIXME documents that, as in the original McMini, this only detects an uninitialized mutex for stack/garbage mutexes; a never-initialized data/heap mutex is zero-filled (== PTHREAD_MUTEX_INITIALIZER on glibc) and still slips through. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Exercises the reject path of the PTHREAD_MUTEX_INITIALIZER support: a stack-allocated pthread_mutex_t filled with non-zero garbage (so it cannot be mistaken for the all-zero PTHREAD_MUTEX_INITIALIZER) is locked without initialization. McMini reports: UNDEFINED BEHAVIOR: Attempting to lock an uninitialized mutex Note the data/heap case is intentionally not detected (zero-filled == PTHREAD_MUTEX_INITIALIZER); see the FIXME in src/mcmini/model/transitions/mutex.cpp. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
When model checking a target compiled with -fsanitize=thread, the worker
threads that libmcmini spawns in TARGET_BRANCH mode segfaulted on their
first instrumented memory access: they were created through libc's raw
pthread_create (resolved from an explicit dlopen("libpthread.so")
handle), which bypasses libtsan's pthread_create interceptor, so
ThreadSanitizer never initialized the per-thread ThreadState. The first
__tsan_* call then dereferenced a null ThreadState (SEGV on a small fixed
offset such as 0x828, inside libtsan).
In classic model checking, resolve pthread_create via dlsym(RTLD_NEXT)
instead. Because libmcmini.so is LD_PRELOAD'd ahead of the target's
DT_NEEDED libraries, RTLD_NEXT lands on the sanitizer's interceptor when
the target is instrumented (which sets up the thread's state), and falls
through to libc/libpthread otherwise.
The change is gated on !dmtcp_is_enabled(): under DMTCP, libdmtcp is also
in the link map and RTLD_NEXT could resolve to its interceptor, and the
DMTCP thread-creation paths are handled separately via
libdmtcp_pthread_create. The explicit-handle behavior is preserved there
byte-for-byte, so deep debugging is unaffected. (Only pthread_create is
routed this way; the model-checking join path never calls the real
pthread_join. Sanitizer support under deep debugging is future work.)
Verified: mcmini now model checks ~/dmtcp.git/test/tsan_target (a
-fsanitize=thread program) without the SEGV; spawned worker threads run
their instrumented lock/increment/unlock loops under scheduler control.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
[ This PR is stacked on top of PR #3 so that it can handle PTHREAD_MUTEX_INITIALIZER in the target. ]
Model checking a
-fsanitize=threadtarget crashed: worker threads spawnedby libmcmini were created through libc's raw pthread_create, bypassing
libtsan's interceptor, so ThreadSanitizer never set up their ThreadState
and the first instrumented access hit a null deref (SEGV inside libtsan).
Fix: in classic mode, resolve pthread_create via
dlsym(RTLD_NEXT). Sincelibmcmini.so is LD_PRELOAD'd ahead of the target's libraries, this routes
through the sanitizer's interceptor when present and falls back to libc
otherwise. Gated on !dmtcp_is_enabled(), leaving the DMTCP path unchanged.
Verified: mcmini now model checks tsan_target with no SEGV.
Caveats: crash fix only (mutex/cond/sem still bypass libtsan, so their ops
are untracked but no longer crash); classic mode only, DMTCP+TSan is
future work. Stacks on pthread-mutex-initializer-support.