3 * @brief Independent read and independent write test
11 #include "model-assert.h"
16 int r1, r2, r3, r4; /* "local" variables */
18 static void *a(void *obj)
20 x.store(1, wildcard(1));
24 static void *b(void *obj)
26 y.store(1, wildcard(2));
30 static void *c(void *obj)
32 r1 = x.load(wildcard(3));
33 r2 = y.load(wildcard(4));
37 static void *d(void *obj)
39 r3 = y.load(wildcard(5));
40 r4 = x.load(wildcard(6));
45 int user_main(int argc, char **argv)
47 pthread_t t1, t2, t3, t4;
52 printf("Main thread: creating 4 threads\n");
53 pthread_create(&t1,NULL, &a, NULL);
54 pthread_create(&t2,NULL, &b, NULL);
55 pthread_create(&t3,NULL, &c, NULL);
56 pthread_create(&t4,NULL, &d, NULL);
58 pthread_join(t1,NULL);
59 pthread_join(t2,NULL);
60 pthread_join(t3,NULL);
61 pthread_join(t4,NULL);
62 printf("Main thread is finished\n");
65 * This condition should not be hit if the execution is SC */
66 bool sc = (r1 == 1 && r2 == 0 && r3 == 1 && r4 == 0);