These tests had become less useful, since the model-checker would ignore
release sequence fixup in the absence of pending data races. So add some
normal loads and stores to our tests, inducing some data races and some
proper synchronization.
#include "stdatomic.h"
atomic_int x;
+int var = 0;
static void a(void *obj)
{
+ store_32(&var, 1);
atomic_store_explicit(&x, *((int *)obj), memory_order_release);
atomic_store_explicit(&x, *((int *)obj) + 1, memory_order_relaxed);
}
{
int r = atomic_load_explicit(&x, memory_order_acquire);
printf("r = %u\n", r);
+ store_32(&var, 3);
}
static void b1(void *obj)
int i = 7;
int r = atomic_load_explicit(&x, memory_order_acquire);
printf("r = %u\n", r);
+ store_32(&var, 2);
thrd_create(&t3, (thrd_start_t)&a, &i);
thrd_create(&t4, (thrd_start_t)&b2, NULL);
thrd_join(t3);
#include "stdatomic.h"
atomic_int x;
+int var = 0;
static void a(void *obj)
{
+ store_32(&var, 1);
atomic_store_explicit(&x, 1, memory_order_release);
atomic_store_explicit(&x, 42, memory_order_relaxed);
}
{
int r = atomic_load_explicit(&x, memory_order_acquire);
printf("r = %u\n", r);
+ printf("load %d\n", load_32(&var));
}
static void c(void *obj)