PTHREAD_COND_INITIALIZER support#4
Open
gc00 wants to merge 4 commits into
Open
Conversation
maxwellpirtle
requested changes
Jun 30, 2026
Contributor
Author
|
Yes, in this case, it's only the last commit that is important. Now that you've accepted PR #2, I no longer have a problem of multiple PRs needed for further code development. I'll push this again with just the last (cond initializer) commit. And as before, since you're more familiar with the deep-debug code, could you change this code to do everything on the model side? You could do it faster than me -- especially with the help of AI. |
gc00
force-pushed
the
pthread-cond-initializer-support
branch
from
2d935d7 to
ed8e78f
Compare
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>
A condition variable declared with PTHREAD_COND_INITIALIZER never flows through the pthread_cond_init wrapper, so the model never observes it being initialized. Previously the enqueue/wait, signal, and broadcast callbacks threw "uninitialized condition variable" in that case. Port the original McMini behavior (mirrors the PTHREAD_MUTEX_INITIALIZER support): on the first operation against a condition variable the model has not seen, read the target's memory via process_vm_readv and compare against PTHREAD_COND_INITIALIZER. On a match, lazily register it as initialized with the arbitrary wakeup policy (as cond_init_callback does); otherwise report undefined behavior. The shared logic lives in ensure_cond_initialized(), used by the enqueue, signal, and broadcast callbacks (the operations that can first touch a statically-initialized cv). The actual wait callback is unchanged: it always follows enqueue, which has already registered the cv. Destroy is also unchanged (destroying a never-initialized cv stays undefined behavior, faithful to the original). A FIXME documents that, as in the original McMini, this only detects an uninitialized cv for stack/garbage cvs; a never-initialized data/heap cv is zero-filled (== PTHREAD_COND_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_COND_INITIALIZER support: a stack-allocated pthread_cond_t filled with non-zero garbage (so it cannot be mistaken for the all-zero PTHREAD_COND_INITIALIZER) is signaled without initialization. McMini reports: UNDEFINED BEHAVIOR: Attempting to signal an uninitialized condition variable This complements src/examples/cv-test.c (a global PTHREAD_COND_INITIALIZER cv, which is accepted). Note the data/heap case is intentionally not detected (zero-filled == PTHREAD_COND_INITIALIZER); see the FIXME in src/mcmini/model/transitions/condition_variables.cpp. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
gc00
force-pushed
the
pthread-cond-initializer-support
branch
from
bcc35a5 to
7dd612d
Compare
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
2 participants
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.
Port from classic McMing