c0fe7f661a06317df8b758156a88fa5eb5cd68df
[model-checker.git] / test / insanesync.cc
1 #include <stdlib.h>
2 #include <stdio.h>
3 #include <threads.h>
4 #include <atomic>
5
6 #include "librace.h"
7 #include "model-assert.h"
8
9 using namespace std;
10
11 atomic_int x, y;
12 atomic_intptr_t z, z2;
13
14 int r1, r2, r3; /* "local" variables */
15
16 /**
17                 This example illustrates a self-satisfying cycle involving
18                 synchronization.  A failed synchronization creates the store that
19                 causes the synchronization to fail.
20
21                 The C++11 memory model nominally allows r1=0, r2=1, r3=5.
22
23                 This example is insane, we don't support that behavior.
24 */
25
26
27 static void a(void *obj)
28 {
29         z.store((intptr_t)&y, memory_order_relaxed);
30         r1 = y.fetch_add(1, memory_order_release);
31         z.store((intptr_t)&x, memory_order_relaxed);
32         r2 = y.fetch_add(1, memory_order_release);
33 }
34
35
36 static void b(void *obj)
37 {
38         r3 = y.fetch_add(1, memory_order_acquire);
39         intptr_t ptr = z.load(memory_order_relaxed);
40         z2.store(ptr, memory_order_relaxed);
41 }
42
43 static void c(void *obj)
44 {
45         atomic_int *ptr2 = (atomic_int *)z2.load(memory_order_relaxed);
46         (*ptr2).store(5, memory_order_relaxed);
47 }
48
49 int user_main(int argc, char **argv)
50 {
51         thrd_t t1, t2, t3;
52
53         atomic_init(&x, 0);
54         atomic_init(&y, 0);
55         atomic_init(&z, (intptr_t) &x);
56         atomic_init(&z2, (intptr_t) &x);
57
58         thrd_create(&t1, (thrd_start_t)&a, NULL);
59         thrd_create(&t2, (thrd_start_t)&b, NULL);
60         thrd_create(&t3, (thrd_start_t)&c, NULL);
61
62         thrd_join(t1);
63         thrd_join(t2);
64         thrd_join(t3);
65
66         printf("r1=%d, r2=%d, r3=%d\n", r1, r2, r3);
67
68         return 0;
69 }