Sync for branched thread creation should also consistently publish to initial values like enter_multithreaded #327
Description
At #321 (comment) it turned out that sync Join for other privatizations (including in base) should also publish to initial values just like enter_multithreaded would.
For example, we're unsound in the following example:
// SKIP PARAM: --enable ana.int.interval
#include <pthread.h>
#include <assert.h>
int g = 1;
pthread_mutex_t A = PTHREAD_MUTEX_INITIALIZER;
void *t_fun(void *arg) {
return NULL;
}
int main(void) {
int x, r;
pthread_t id;
if (r) {
pthread_create(&id, NULL, t_fun, NULL);
pthread_mutex_lock(&A);
g = 5;
pthread_mutex_unlock(&A);
}
else {
g = 10;
}
pthread_mutex_lock(&A);
x = g; // may read 10!
pthread_mutex_unlock(&A);
return 0;
}Alternatively making threadflag path-sensitive should avoid all such cases and keep single- and multithreaded mode separate. Then no sync Join should be necessary.