PTHREAD_MUTEX_INITIALIZER support

[gc00]

Porting support for PTHREAD_MUTEX_INITIALIZER to deep-debug

[maxwellpirtle]

We saw this fix worked in McMini before, but after considering it further, I think a better solution would be to perform the check for whether we think the mutex was statically initialized within libmcmini.so itself and not on the model size. We then inform the model of the result of the check instead.

Specifically, when we encounter pthread_mutex_lock and friends in libmcmini.so, we should check if the mutex appears to be PTHREAD_MUTEX_INITIALIZER using a simple memcmp. If the mutex appears to be statically initialized, we would record this information inside

volatile runner_mailbox& rmb

The model could then check this extra data inside to yield something like

if (rmb.cnts[0] == 1) {
 // Indicates that `memcmp(remote_mut, PTHREAD_MUTEX_INITIALIZER) == 0` so initialize the mutex in the model
} else {
// memcmp(remote_mut, PTHREAD_MUTEX_INITIALIZER) != 0: UB
throw undefined_behavior_exception(
          "Attempting to lock an uninitialized mutex");
}

This keeps the model-side code cleaner. Reasoning about multiple processes is challenging. Deep debug attempts to reduce the burden of needing to reason about multiple processes in any given function as much as possible. In general, any additional information that libmcmini.so needs to communicate with the model should be passed through the specific payloads in the mailboxes.

[maxwellpirtle]

Specifically, look at wrappers.c

volatile runner_mailbox *thread_get_mailbox() {
  assert(!is_checkpoint_thread());
  assert(tid_self != RID_INVALID);
  assert(tid_self != RID_CHECKPOINT_THREAD);
  return &((volatile struct mcmini_shm_file *)(global_shm_start))
              ->mailboxes[tid_self];
}

You'll see examples such as this in mc_pthread_mutex_unlock

//...
    case TARGET_BRANCH:
    case TARGET_BRANCH_AFTER_RESTART: {
      volatile runner_mailbox *mb = thread_get_mailbox();
      mb->type = MUTEX_UNLOCK_TYPE;
      memcpy_v(mb->cnts, &mutex, sizeof(mutex));
      thread_wake_scheduler_and_wait();
      return libpthread_mutex_unlock(mutex);
    }

we could add

memcpy_v(mb->cnts, &mutex, sizeof(mutex));
static int static_mutex = PTHREAD_MUTEX_INITIALIZER;
int is_static_mutex = memcmp(&mutex, & static_mutex, sizeof(mutex)) == 0;
memcpy_v(mb->cnts[sizeof(mutex)], &is_static_mutex, sizeof(mutex)); // NEW CODE

and then the model code becomes

if (rmb.cnts[sizeof(pthread_mutex_t) == 1) {
  // Statically initialized mutex that we didn't see, initialize it now
  m.observe_object(remote_mut, new mutex(mutex::state::unlocked, remote_mut));
else {
  throw undefined_behavior_exception(
          "Attempting to lock an uninitialized mutex");
}

Corresponding changes would be needed in other locations in libmcmini.so

[gc00]

Hi @maxwellpirtle , Thanks for reviewing this. I agree that if we can move this to the model side, this would be an improvement. And presumably, this would be easier to do in deep-debug, rather than classic McMini.

Since you are more familiar with the deep-debug code, is there any chance that you could do this? It would probably take me more time than it would you. Hopefully, with tools like Claude, it would be fairly fast for you to do this. (In my case, I simply asked Claude to port the classic McMini code to deep-debug.)