b66548039d9438a9ed4db3aeeb6675fa6c545304
[cdsspec-compiler.git] / benchmark / read-copy-update / rcu.cc
1 #include <atomic>
2 #include <threads.h>
3 #include <stdatomic.h>
4 #include <stdlib.h>
5 #include <stdio.h>
6
7 #include <spec_lib.h>
8 #include <stdlib.h>
9 #include <cdsannotate.h>
10 #include <specannotation.h>
11 #include <model_memory.h>
12 #include "common.h" 
13
14 #include "librace.h"
15
16 /**
17         This is an example about how to specify the correctness of the
18         read-copy-update synchronization mechanism.
19 */
20
21 typedef struct Data {
22         int data1;
23         int data2;
24         int data3;
25 } Data;
26
27 atomic<Data*> data;
28         
29 /**
30         @Begin
31         @Global_define:
32                 @DeclareVar:
33                         int data1;
34                         int data2;
35                         int data3;
36                 @InitVar:
37                         data1 = 0;
38                         data2 = 0;
39                         data3 = 0;
40         @Happens_before:
41                 Write -> Read
42                 Write -> Write
43         @End
44 */
45
46 /**
47         @Begin
48         @Interface: Read
49         @Commit_point_set: Read_Success_Point
50         //@ID: isOriginalRead(__RET__) ? 1 : DEFAULT_CALL_ID
51         @Post_check:
52                 data1 == __RET__->data1 &&
53                 data2 == __RET__->data2 &&
54                 data3 == __RET__->data3
55         @End
56 */
57 Data* read() {
58         Data *res = data.load(memory_order_acquire);
59         //load_32(&res->data1);
60         /**
61                 @Begin
62                 @Commit_point_define_check: true
63                 @Label: Read_Success_Point
64                 @End
65         */
66         //model_print("Read: %d, %d, %d\n", res->data1, res->data2, res->data3);
67         return res;
68 }
69
70 /**
71         @Begin
72         @Interface: Write
73         @Commit_point_set: Write_Success_Point
74         @Action:
75                 data1 += d1;
76                 data2 += d2;
77                 data3 += d3;
78         @End
79 */
80 Data* write(int d1, int d2, int d3) {
81         bool succ = false;
82         Data *tmp = (Data*) malloc(sizeof(Data));
83         Data *prev = data.load(memory_order_acquire);
84         do {
85         //store_32(&tmp->data1, prev->data1 + d1);
86         tmp->data1 = prev->data1 + d1;
87             tmp->data2 = prev->data2 + d2;
88             tmp->data3 = prev->data3 + d3;
89         succ = data.compare_exchange_strong(prev, tmp,
90             memory_order_acq_rel, memory_order_relaxed);
91                 /**
92                         @Begin
93                         @Commit_point_define_check: succ
94                         @Label: Write_Success_Point
95                         @End
96                 */
97         } while (!succ);
98         //model_print("Write: %d, %d, %d\n", tmp->data1, tmp->data2, tmp->data3);
99         return tmp;
100 }
101
102
103 void threadA(void *arg) {
104         write(1, 0, 0);
105 }
106
107 void threadB(void *arg) {
108         write(0, 1, 0);
109 }
110
111 void threadC(void *arg) {
112         write(0, 0, 1);
113 }
114
115 void threadD(void *arg) {
116         Data *dataC = read();
117 }
118
119 int user_main(int argc, char **argv) {
120         /**
121                 @Begin
122                 @Entry_point
123                 @End
124         */
125         
126         thrd_t t1, t2, t3, t4;
127         Data *dataInit = (Data*) malloc(sizeof(Data));
128         dataInit->data1 = 0;
129         dataInit->data2 = 0;
130         dataInit->data3 = 0;
131         atomic_init(&data, dataInit);
132         write(0, 0, 0);
133
134         thrd_create(&t1, threadA, NULL);
135         thrd_create(&t2, threadB, NULL);
136         thrd_create(&t3, threadC, NULL);
137         thrd_create(&t4, threadD, NULL);
138
139         thrd_join(t1);
140         thrd_join(t2);
141         thrd_join(t3);
142         thrd_join(t4);
143
144         return 0;
145 }