Handle pointer aliasing and identify object/threads according to trace

[maxwellpirtle]

Discussion

McMini cannot currently handle pointer aliasing. In the simple program shown below, e.g., McMini would improperly point out that the mutex mut has already been created. In more complicated examples where the identity of the object might matter more, this could pose a problem.

#include <pthread.h>
int 
main(int argc, const char **argv)
{
    pthread_mutex_t mut;
    pthread_mutex_init(&mut, NULL);
    pthread_mutex_init(&mut, NULL);
    return 0;
}

Furthermore, if the address of the visible object changes across executions (e.g. perhaps the program malloc()s some space for a sem_t), McMini will incorrectly track state across backtracking points (or more properly across fork() calls. This is bad for obvious reasons.

A tangentially related, and arguably more troublesome, problem is that of identifying threads. It's entirely possible, as far as I'm aware, that a pthread_t value is not unique across processes (even those created using fork()) or that a pthread_t value is reused when a thread exits. Here again, we'd have an issue of stability: McMini implicitly relies on identities remaining stable across process fork()s to function properly. This is too unstable for larger programs.

Possible Solution

The problem is one of identity. How can we identify an object, a thread, under different runtime environments? The solution is (briefly) outlined in the paper "Runtime Model Checking of Multithreaded C/C++ Programs" by Yang et al. (the Utah paper).
We effectively want to identify threads, objects, etc. based on the order in which McMini encountered the objects in the current transition sequence. See section 4.1 of the paper for details.

For pointer aliasing, we'd effectively want to map unique objects created by the program to their "stable" identity. An extra of level of indirection here seems to be incoming

Challenges

One of the major challenges here is reconciling the fact that objects are created when they're encountered, not when the initialization function (sem_init(), pthread_mutex_init(), etc) is executed by McMini. This clashes with assigning identity based on the transition sequence; in that case, we'd need to create the object when the transition was actually executed.

A possible strategy would be to create "embryo" objects, much in the same way we create an "embryo" thread at a pthread_create() call (although the semantics would differ a bit). Basically, we'd want to defer creating the object and assigning it a unique identifier until the initialization function was scheduled to execute by McMini. We'd need to think through this a bit more

[maxwellpirtle]

@gc00 I have a feeling you may have encountered similar problems while writing DMTCP?