Analysis of pthread_barrier for race detection

[michael-schwarz]

One of the features we could additionally have for checking for data races could be a support for pthread_barrier.

#include <stdio.h>
#include <pthread.h>

#define THREAD_NUMS 4
pthread_barrier_t barrier;

void *t0(void *param)
{
    lock(a); g = 3; unlock(a);
    pthread_barrier_wait(&barrier);
    printf("t0 ready\n");
}

void *t1(void *param)
{
    lock(a); g = 3; unlock(a);
    pthread_barrier_wait(&barrier);
    printf("t1 ready\n");
}

void *t2(void *param)
{
    lock(a); g = 3; unlock(a);
    pthread_barrier_wait(&barrier);
    printf("t2 ready\n");
}

int main(void)
{
    pthread_t t[3];

    pthread_barrier_init(&barrier, NULL, THREAD_NUMS);

    pthread_create(&t[0], NULL, t0, NULL);
    pthread_create(&t[1], NULL, t1, NULL);
    pthread_create(&t[2], NULL, t2, NULL);

    pthread_barrier_wait(&barrier);
    g = 5; //NORACE

    pthread_barrier_destroy(&barrier);

}

If one removes any of the pthread_barrier_wait calls, all successors to pthread_barrier_wait would be dead.

To this end, one would track locally: In each thread a must $$\underline M$$ and a may set $$\overline M$$ of x for which pthread_barrier_wait(x) has been called.

Globally, one would track at a global unknown [x]:

• The capacity passed to pthread_barrier_init
• A set of unique thread ids that call pthread_barrier_wait at most once. (If any of these is non-unique or one thread calls wait several times, we go to top)

Then:

• If the number of threads that may call pthread_barrier_wait is below the capacity (and all call it at most once and are unique), all successors of pthread_barrier_wait are dead.
• If at an access pthread_barrier_wait(x) is known to have returned $$x \in \underline M$$, the above condition is known to hold and the other access is by a thread that has to call pthread_barrier_wait(x) for it to return, but $$x$$ is not in $$\overline M$$ there, these two accesses cannot race.

It should be possible to cast this into a may-race-predicate enhanced digest Julian and I have discussed a little 😉