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_WRAPPER__(atomic_int *loc) {
22 return loc->load(memory_order_acquire);
25 int Load(atomic_int *loc) {
26 // Instrument with the INTERFACE_BEGIN annotation
27 Method cur = _createInterfaceBeginAnnotation("LOAD");
28 // Call the actual function
29 int RET = Load_WRAPPER__(loc);
31 // Initialize the value struct
32 LOAD *value = new LOAD;
36 // Store the value info into the current MethodCall
39 // Return if there exists a return value
44 @SideEffect: STATE(val) = val;
47 void Store_WRAPPER__(atomic_int *loc, int val) {
48 loc->store(val, memory_order_release);
51 void Store(atomic_int *loc, int val) {
52 // Instrument with the INTERFACE_BEGIN annotation
53 Method cur = _createInterfaceBeginAnnotation("STORE");
54 // Call the actual function
55 Store_WRAPPER__(loc, val);
57 // Initialize the value struct
58 STORE *value = new STORE;
62 // Store the value info into the current MethodCall
66 static void a(void *obj)
72 static void b(void *obj)
77 static void c(void *obj)
83 int user_main(int argc, char **argv)
88 _createInitAnnotation();
90 thrd_create(&t1, (thrd_start_t)&a, NULL);
91 thrd_create(&t2, (thrd_start_t)&b, NULL);
92 thrd_create(&t3, (thrd_start_t)&c, NULL);