Incorrect atomic ordering for arrays on TSO and PSO

[ldr709]

CBMC (with either TSO or PSO as memory model) incorrectly reports "VERIFICATION SUCCESSFUL" when given the following test case. This seems to imply that the atomic c[0] = 1 is ordered with read_x = x. Interestingly, this test fails if c is just an unsigned long and not an array.

#include <assert.h>
#include <pthread.h>
#include <stdlib.h>

unsigned long x;
unsigned long read_x;

unsigned long c[1];
unsigned long read_c;

void *thread0(void *arg)
{
    __CPROVER_atomic_begin();
    c[0] = 1;
    __CPROVER_atomic_end();

    read_x = x;

    return NULL;
}

void *thread1(void *arg)
{
    x = 1;
    __CPROVER_fence("WRfence");
    read_c = c[0];

    return NULL;
}

int main(int argc, char *argv[])
{
    pthread_t t0;
    pthread_t t1;

    if (pthread_create(&t0, NULL, thread0, NULL))
        abort();
    if (pthread_create(&t1, NULL, thread1, NULL))
        abort();
    if (pthread_join(t0, NULL))
        abort();
    if (pthread_join(t1, NULL))
        abort();

    assert(read_x == 1 || read_c == 1);

    return 0;
}

[peterschrammel]

see also #123