more edits
[cdsspec-compiler.git] / notes / generated_code_examples.txt
1 ******    Example1:    ******
2 Global Variable Declaration
3
4 /* Include all the header files that contains the interface declaration */
5 #inlcude <atomic>
6 #include <memory>
7 #include <assert.h>
8
9 /* Other necessary header files */
10 #include <stdint.h>
11 #include <specannotation.h>
12 #include <spec_lib.h>
13
14 /* All other user-defined functions */
15 ALL_USER_DEFINED_FUNCTIONS  // Make them static 
16
17 /* Definition of interface info struct (per interface) */
18 typedef struct Put_info {
19         shared_ptr<TypeV> __RET__;
20         TypeK & key;
21         TypeV & value;
22 } Put_info;
23
24 typedef struct Get_info {
25         shared_ptr<TypeV> __RET__;
26         TypeK & key;
27 } Get_info;
28 /* End of info struct definition */
29
30 /* ID functions of interface */
31 static id_t Put_id() {
32         id_t id = PUT_ID;  // Default ID == 0;
33         return id;
34 }
35
36 static id_t Get_id() {
37         id_t id = GET_ID;
38         return id;
39 }
40 /* End of ID functions */
41
42
43
44 /* Check_action function of interfaces */
45 bool Put_check_action(void *info, id_t __ID__) {
46         bool check_passed;
47         Put_info *theInfo = (Put_info) info;
48         shared_ptr<TypeV> __RET__ = theInfo->__RET__;
49         TypeK & key = theInfo->key;
50         TypeV & value = theInfo->value;
51
52         // __COND_SAT__
53         bool __COND_SAT__ = PUT_CONDITION;
54
55         // Check
56         check_passed = PUT_CHECK_EXPRESSION;
57         if (!check_passed)
58                 return false;
59
60         // Action
61         PUT_ACTION
62
63         // Post_check
64         check_passed = PUT_POST_CHECK_EXPRESSION;
65         if (!check_passed)
66                 return false;
67
68         // Post_action
69         PUT_POST_ACTION
70 }
71
72
73 bool Get_check_action(void *info, id_t __ID__) {
74         //...
75 }
76 /* End of check_action function definitions */ 
77
78 /* Initialization of interface<->function_ptr table */
79 #define INTERFACE_SIZE 2
80 void** func_ptr_table;
81
82 /* Beginning of other user-defined variables */
83 bool lock_acquired;
84 int reader_lock_cnt;
85 /* End of other user-defined variables */
86
87
88 /* Define function for sequential code initialization */
89 void __sequential_init() {
90         /* Init func_ptr_table */
91         func_ptr_table = (void**) malloc(sizeof(void*) * 2);
92         func_ptr_table[0] = (void*) &Put_id;
93         func_ptr_table[1] = (void*) &Put_check_action;
94         func_ptr_table[2] = (void*) &Get_id;
95         func_ptr_table[3] = (void*) &Get_check_action;
96
97         /* Init user-defined variables */
98         lock_acquired = false;
99         reader_lock_cnt = 0;
100
101         /* Pass function table info */
102         anno_func_table_init func_table;
103         func_table.size = INTERFACE_SIZE;
104         func_table.table = func_ptr_table;
105         spec_annotation func_init;
106         func_init.type = FUNC_TABLE_INIT;
107         func_init.annotation = &anno_func_table_init;
108         cdsannotate(SPEC_ANALYSIS, &func_init);
109
110         /* Pass the happens-before initialization here */
111         /* PutIfAbsent (putIfAbsent_Succ) -> Get (true) */
112         anno_hb_init hbConditionInit0;
113         hbConditionInit0.interface_num_before = 1;
114         hbConditionInit0.hb_condition_num_before = 1;
115         hbConditionInit0.interface_num_after = 2;
116         hbConditionInit0.hb_condition_num_after = 0;
117         spec_annotation hb_init0;
118         hb_init0.type = HB_INIT;
119         hb_init0.annotation = &hbConditionInit0;
120         cdsannotate(SPEC_ANALYSIS, &hb_init0);
121 }
122 /* End of Global construct generation in class */
123
124 /* The following static field declaration is necessary for class */
125 template <typename T>
126 bool CLASS<T>::lock_acquired;
127
128 template <typename T>
129 int CLASS<T>::reader_lock_cnt;
130 /* End of static field definition */
131
132
133 ******    Example2:    ******
134 Interface Wrapper
135
136 /* Include the header files first */
137 #include <threads.h>
138 #include <cdsannotate.h>
139 #include <specannotation.h>
140 #include <spec_lib.h>
141
142 TypeReturn interfaceName(ARGType1 arg1, ARGType2 arg2)
143 {
144         // Interface begins
145         anno_interface_begin interface_begin;
146         interface_begin.interface_num = 0; // Interface number
147         spec_annotation annotation_interface_begin;
148         annotation_interface_begin.type = INTERFACE_BEGIN;
149         annotation_interface_begin.annotation = &interface_begin;
150         cdsannotate(SPEC_ANALYSIS, &annoation_interface_begin);
151
152         TypeReturn __RET__ = __wrapper_interfaceName(arg1, arg2);
153
154         // HB conditions (if any)
155         if (HB_CONDITION1) {
156                 anno_hb_condition hb_condition1;
157                 hb_condition1.interface_num = 0; // Interface number
158                 hb_condition1.hb_condition_num = 1; // HB condition number
159                 spec_annotation annotation_hb_condition;
160                 annotation_hb_condition.type = HB_CONDITION;
161                 annotation_hb_condition.annotation = &hb_condition;
162                 cdsannotate(SPEC_ANALYSIS, &annotation_hb_condition);
163         }
164         // And more (if any)
165
166         // Interface ends
167         INTERFACE_LABEL_info info = (INTERFACE_LABEL_info*) malloc(sizeof(INTERFACE_LABEL_info));
168         info->__RET__ = __RET__;
169         info->arg1 = arg1;
170         info->arg2 = arg2;
171         anno_interface_end interface_end;
172         interface_end.interface_num = 0; // Interface number
173         interface_end.info = info; // Info
174         spec_annotation annotation_interface_end;
175         annotation_interface_end.type = INTERFACE_END;
176         annotation_interface_end.annotation = &interface_end;
177         cdsannotate(SPEC_ANALYSIS, &annoation_interface_end);
178 }
179
180
181 ******    Example3:    ******
182 Potential Commit Point
183
184
185 #include <stdint.h>
186 #include <cdsannotate.h>
187
188 /* Should add the __ATOMIC_RET__ if necessary */
189 uint64_t __ATOMIC_RET = somevar.compare_exchange_explicit(...);
190
191 if (POTENTIAL_CP_DEFINE_CONDITION) {
192         anno_potential_cp_define potential_cp_define;
193         potential_cp_define.label_num = 1; // Commit point label number
194         spec_annotation annotation_potential_cp_define;
195         annotation_potential_cp_define.type = POTENTIAL_CP_DEFINE;
196         annotation_potential_cp_define.annotation = &potential_cp_define;
197         cdsannotate(SPEC_ANALYSIS, &annotation_potential_cp_define);
198 }
199
200 ******    Example4:    ******
201 Commit Point Define
202
203 #include <threads.h>
204 #include <cdsannotate.h>
205 #include <stdint.h>
206
207 /* Should add the __ATOMIC_RET__ if necessary */
208 uint64_t __ATOMIC_RET = somevar.compare_exchange_explicit(...);
209
210 /* For all the interface check at this commit point (if there is multiple
211  * checks here) */
212 // Commit point 3 <=> potentialCP 4
213 if (COMMIT_POINT3_CONDITION) {
214         anno_cp_define cp_define;
215         cp_define.label_num = 3;
216         cp_define.potential_cp_label_num = 1;
217         spec_annotation annotation_cp_define;
218         annotation_cp_define.type = CP_DEFINE;
219         annotation_cp_define.annotation = &cp_define;
220         cdsannotate(SPEC_ANALYSIS, &annotation_cp_define);
221 }
222 // More if there are any
223
224 }
225
226
227 *****    Example5:    ******
228 Commit Point Define Check
229
230
231 #include <threads.h>
232 #include <cdsannotate.h>
233 #include <stdint.h>
234
235 /* Should add the __ATOMIC_RET__ if necessary */
236 uint64_t __ATOMIC_RET = somevar.compare_exchange_explicit(...);
237
238
239 /* For all the interface check at this commit point (if there is multiple
240  * checks here) */
241 if (COMMIT_POINT3_CONDITION) {
242         anno_cp_define cp_define;
243         uint64_t call_sequence_num = get(&__sequential.interface_call_sequence, tid);
244         bool check_passed = false;
245         cp_define.check_passed = check_passed;
246         cp_define.interface_num = interface_num;
247         cp_define.label_num = 3;
248         cp_define.call_sequence_num = call_sequence_num;
249         spec_annotation annotation_cp_define;
250         annotation_cp_define.type = CP_DEFINE;
251         annotation_cp_define.annotation = &cp_define;
252         cdsannotate(SPEC_ANALYSIS, &annotation_cp_define);
253 }
254 // More if there are any
255
256 }