Uniqueness analysis for Juliet suite std_thread wrappers

[vesalvojdani]

Would be good to have this sooner rather than later. Goblint can't analyze Juliet suite race detection stuff because they use some wrappers that end up creating pointers to structs containing the mutex. One could obviously just take their lock operations as native, but these are much simpler programs than all the idioms we handle with symbolic locks. It does not seem unreasonable to think that we should be able to analyzer the following.

struct { pthread_mutex_t mutex; } *mylock;
int myglobal;

void *t_fun(void *arg) {
  pthread_mutex_lock(&mylock->mutex);
  myglobal=myglobal+1;
  pthread_mutex_unlock(&mylock->mutex);
  return NULL;
}

int main(void) {
  pthread_t id;
  mylock = malloc(sizeof(*mylock));
  pthread_mutex_init(&mylock->mutex, NULL);

  pthread_create(&id, NULL, t_fun, NULL);
  pthread_mutex_lock(&mylock->mutex);
  myglobal=myglobal+1;
  pthread_mutex_unlock(&mylock->mutex);
  pthread_join (id, NULL);
  return 0;
}

[michael-schwarz]

This amounts to checking that the malloc(...) is reached exactly once as far as I can see.

If it suffices to find this information for mallocs that happen in single-threaded mode with earlyglobs off, this should be fairly simple:

It would suffice to equip the blob with a boolean is_unique. Upon the call to malloc in single-thread mode:

• If there already is a blob associated with this allocation site in the local state: Set its is_unique to false
• If there is not, create it with is_unique true.

When in multi-threaded mode: Create it immediately with is_unique false. Upon going multithreaded, one should simply be able to publish it without any further complications.

You have an undergrad student on these Juliet things, right? Maybe they can also implement this?

[sim642]

It seems like a slight variation of thread analysis could work for the multithreaded case as well. And it would avoid having to hammer yet another feature into base analysis to manage the uniqueness flag in blobs.

[michael-schwarz]

A student of ours is implementing this as part of their practical course (special 1-participant instance of the course).

[michael-schwarz]

We should investigate how much of this is resolved by #722.

[vesalvojdani]

Hmm... I tried the Juliet suite examples again with enabled. The above examples work, but there seems to be some additional trickiness with the way Juliet suite wrappers create threads that combined with this uniqueness causes a spurious access without locks. Since we already have malloc uniqueness analysis PR merged, I will rename this issue to track Juliet suite thread wrapper crap.

[sim642]

As determined during GobCon, the problem is this check: https://github.com/goblint/analyzer/blob/33775dbcc680622acb836129e2b157372c57ebc7/src/analyses/mallocWrapperAnalysis.ml#L131-L133 When the second (non-unique) thread locks the mutex, it checks whether it is unique and only considers the case when the locking thread is unique. In this case, however, it would also suffice that the thread that created the malloc variable was unique.

[vesalvojdani]

What is the status of this thing now? You have a student working on the remaining issues for this?

[michael-schwarz]

No, there's no one currently working on it.