8 /** @DeclareState: int val;
10 @Commutativity: LOAD <-> LOAD (true)
11 @Commutativity: STORE <-> LOAD (true)
12 @Commutativity: STORE <-> STORE (true)
17 return HasItem(PREV, STATE(val) == RET);
18 @SideEffect: STATE(val) = RET;
21 int Load(atomic_int *loc) {
22 return loc->load(memory_order_acquire);
26 @SideEffect: STATE(val) = val;
29 void Store(atomic_int *loc, int val) {
30 loc->store(val, memory_order_release);
33 static void a(void *obj)
39 static void b(void *obj)
44 static void c(void *obj)
50 int user_main(int argc, char **argv)
56 thrd_create(&t1, (thrd_start_t)&a, NULL);
57 thrd_create(&t2, (thrd_start_t)&b, NULL);
58 thrd_create(&t3, (thrd_start_t)&c, NULL);