9 #include <cdsannotate.h>
10 #include <specannotation.h>
11 #include <model_memory.h>
25 /* All other user-defined structs */
26 static IntegerList * set;
27 /* All other user-defined functions */
28 inline static call_id_t getID ( int64_t d1 , int64_t d2 ) {
32 inline static bool print ( int64_t p ) {
33 Data * d = ( Data * ) p ;
34 model_print ( "Elem-> d1 = %d, d2 = %d\n" , d -> data1 , d -> data2 ) ;
36 bool equal ( int64_t p1 , int64_t p2 ) {
37 if ( ! p1 || ! p2 ) return false ;
38 Data * d1 = ( Data * ) p1 ;
39 Data * d2 = ( Data * ) p2 ;
40 if ( d1 -> data1 == d2 -> data1 && d1 -> data2 == d2 -> data2 ) {
48 inline static void _write ( int64_t d1 , int64_t d2 ) {
49 Data * d = ( Data * ) MODEL_MALLOC ( sizeof ( Data ) ) ;
52 push_back ( set , ( int64_t ) d ) ;
55 inline static bool _read ( Data * res ) {
56 bool hasElem = has_elem_by_value ( set , ( int64_t ) res , & equal ) ;
60 /* Definition of interface info struct: Write */
61 typedef struct Write_info {
66 /* End of info struct definition: Write */
68 /* ID function of interface: Write */
69 inline static call_id_t Write_id(void *info, thread_id_t __TID__) {
70 Write_info* theInfo = (Write_info*)info;
71 Data * __RET__ = theInfo->__RET__;
75 call_id_t __ID__ = getID ( d1 , d2 ) ;;
78 /* End of ID function: Write */
80 /* Check action function of interface: Write */
81 inline static bool Write_check_action(void *info, call_id_t __ID__, thread_id_t __TID__) {
83 Write_info* theInfo = (Write_info*)info;
84 Data * __RET__ = theInfo->__RET__;
91 /* End of check action function: Write */
93 /* Definition of interface info struct: Read */
94 typedef struct Read_info {
97 /* End of info struct definition: Read */
99 /* ID function of interface: Read */
100 inline static call_id_t Read_id(void *info, thread_id_t __TID__) {
101 Read_info* theInfo = (Read_info*)info;
102 Data * __RET__ = theInfo->__RET__;
104 call_id_t __ID__ = getID ( __RET__ -> data1 , __RET__ -> data2 );
107 /* End of ID function: Read */
109 /* Check action function of interface: Read */
110 inline static bool Read_check_action(void *info, call_id_t __ID__, thread_id_t __TID__) {
112 Read_info* theInfo = (Read_info*)info;
113 Data * __RET__ = theInfo->__RET__;
115 check_passed = _read ( __RET__ ) ;;
120 /* End of check action function: Read */
122 #define INTERFACE_SIZE 2
123 static void** func_ptr_table;
124 static hb_rule** hb_rule_table;
125 static commutativity_rule** commutativity_rule_table;
126 inline static bool CommutativityCondition0(void *info1, void *info2) {
127 Write_info *_info1 = (Write_info*) info1;
128 Read_info *_info2 = (Read_info*) info2;
132 /* Initialization of sequential varialbes */
133 static void __SPEC_INIT__() {
134 set = createIntegerList ( ) ;
135 Data * d = ( Data * ) MODEL_MALLOC ( sizeof ( Data ) ) ;
138 push_back ( set , ( int64_t ) d ) ;
141 /* Cleanup routine of sequential variables */
142 static bool __SPEC_CLEANUP__() {
143 if ( set ) destroyIntegerList ( set ) ;
147 /* Define function for sequential code initialization */
148 inline static void __sequential_init() {
149 /* Init func_ptr_table */
150 func_ptr_table = (void**) malloc(sizeof(void*) * 2 * 2);
151 func_ptr_table[2 * 1] = (void*) &Write_id;
152 func_ptr_table[2 * 1 + 1] = (void*) &Write_check_action;
153 func_ptr_table[2 * 0] = (void*) &Read_id;
154 func_ptr_table[2 * 0 + 1] = (void*) &Read_check_action;
155 /* Write(true) -> Read(true) */
156 struct hb_rule *hbConditionInit0 = (struct hb_rule*) malloc(sizeof(struct hb_rule));
157 hbConditionInit0->interface_num_before = 1; // Write
158 hbConditionInit0->hb_condition_num_before = 0; //
159 hbConditionInit0->interface_num_after = 0; // Read
160 hbConditionInit0->hb_condition_num_after = 0; //
161 /* Write(true) -> Write(true) */
162 struct hb_rule *hbConditionInit1 = (struct hb_rule*) malloc(sizeof(struct hb_rule));
163 hbConditionInit1->interface_num_before = 1; // Write
164 hbConditionInit1->hb_condition_num_before = 0; //
165 hbConditionInit1->interface_num_after = 1; // Write
166 hbConditionInit1->hb_condition_num_after = 0; //
167 /* Init hb_rule_table */
168 hb_rule_table = (hb_rule**) malloc(sizeof(hb_rule*) * 2);
169 #define HB_RULE_TABLE_SIZE 2
170 hb_rule_table[0] = hbConditionInit0;
171 hb_rule_table[1] = hbConditionInit1;
172 /* Init commutativity_rule_table */
173 commutativity_rule_table = (commutativity_rule**) malloc(sizeof(commutativity_rule*) * 1);
174 commutativity_rule* rule;
175 rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
176 rule->interface_num_before = 1;
177 rule->interface_num_after = 0;
179 rule->condition = CommutativityCondition0;
180 commutativity_rule_table[0] = rule;
181 /* Pass init info, including function table info & HB rules & Commutativity Rules */
182 struct anno_init *anno_init = (struct anno_init*) malloc(sizeof(struct anno_init));
183 anno_init->init_func = (void_func_t) __SPEC_INIT__;
184 anno_init->cleanup_func = (cleanup_func_t) __SPEC_CLEANUP__;
185 anno_init->func_table = func_ptr_table;
186 anno_init->func_table_size = INTERFACE_SIZE;
187 anno_init->hb_rule_table = hb_rule_table;
188 anno_init->hb_rule_table_size = HB_RULE_TABLE_SIZE;
189 anno_init->commutativity_rule_table = commutativity_rule_table;
190 anno_init->commutativity_rule_table_size = 1;
191 struct spec_annotation *init = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
193 init->annotation = anno_init;
194 cdsannotate(SPEC_ANALYSIS, init);
198 /* End of Global construct generation in class */
201 Data * __wrapper__read();
204 /* Interface begins */
205 struct anno_interface_begin *interface_begin = (struct anno_interface_begin*) malloc(sizeof(struct anno_interface_begin));
206 interface_begin->interface_num = 0; // Read
207 interface_begin->interface_name = "Read";
208 struct spec_annotation *annotation_interface_begin = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
209 annotation_interface_begin->type = INTERFACE_BEGIN;
210 annotation_interface_begin->annotation = interface_begin;
211 cdsannotate(SPEC_ANALYSIS, annotation_interface_begin);
212 Data * __RET__ = __wrapper__read();
213 struct anno_hb_condition *hb_condition = (struct anno_hb_condition*) malloc(sizeof(struct anno_hb_condition));
214 hb_condition->interface_num = 0; // Read
215 hb_condition->hb_condition_num = 0;
216 struct spec_annotation *annotation_hb_condition = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
217 annotation_hb_condition->type = HB_CONDITION;
218 annotation_hb_condition->annotation = hb_condition;
219 cdsannotate(SPEC_ANALYSIS, annotation_hb_condition);
221 Read_info* info = (Read_info*) malloc(sizeof(Read_info));
222 info->__RET__ = __RET__;
223 struct anno_interface_end *interface_end = (struct anno_interface_end*) malloc(sizeof(struct anno_interface_end));
224 interface_end->interface_num = 0; // Read
225 interface_end->info = info;
226 struct spec_annotation *annoation_interface_end = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
227 annoation_interface_end->type = INTERFACE_END;
228 annoation_interface_end->annotation = interface_end;
229 cdsannotate(SPEC_ANALYSIS, annoation_interface_end);
233 Data * __wrapper__read() {
235 Data *res = data.load(memory_order_acquire);
236 /* Automatically generated code for commit point define check: Read_Success_Point */
239 struct anno_cp_define_check *cp_define_check = (struct anno_cp_define_check*) malloc(sizeof(struct anno_cp_define_check));
240 cp_define_check->label_num = 0;
241 cp_define_check->label_name = "Read_Success_Point";
242 cp_define_check->interface_num = 0;
243 struct spec_annotation *annotation_cp_define_check = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
244 annotation_cp_define_check->type = CP_DEFINE_CHECK;
245 annotation_cp_define_check->annotation = cp_define_check;
246 cdsannotate(SPEC_ANALYSIS, annotation_cp_define_check);
252 Data * __wrapper__write(int d1, int d2);
254 Data * write(int d1, int d2) {
255 /* Interface begins */
256 struct anno_interface_begin *interface_begin = (struct anno_interface_begin*) malloc(sizeof(struct anno_interface_begin));
257 interface_begin->interface_num = 1; // Write
258 interface_begin->interface_name = "Write";
259 struct spec_annotation *annotation_interface_begin = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
260 annotation_interface_begin->type = INTERFACE_BEGIN;
261 annotation_interface_begin->annotation = interface_begin;
262 cdsannotate(SPEC_ANALYSIS, annotation_interface_begin);
263 Data * __RET__ = __wrapper__write(d1, d2);
264 struct anno_hb_condition *hb_condition = (struct anno_hb_condition*) malloc(sizeof(struct anno_hb_condition));
265 hb_condition->interface_num = 1; // Write
266 hb_condition->hb_condition_num = 0;
267 struct spec_annotation *annotation_hb_condition = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
268 annotation_hb_condition->type = HB_CONDITION;
269 annotation_hb_condition->annotation = hb_condition;
270 cdsannotate(SPEC_ANALYSIS, annotation_hb_condition);
272 Write_info* info = (Write_info*) malloc(sizeof(Write_info));
273 info->__RET__ = __RET__;
276 struct anno_interface_end *interface_end = (struct anno_interface_end*) malloc(sizeof(struct anno_interface_end));
277 interface_end->interface_num = 1; // Write
278 interface_end->info = info;
279 struct spec_annotation *annoation_interface_end = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
280 annoation_interface_end->type = INTERFACE_END;
281 annoation_interface_end->annotation = interface_end;
282 cdsannotate(SPEC_ANALYSIS, annoation_interface_end);
286 Data * __wrapper__write(int d1, int d2) {
288 Data *tmp = (Data*) malloc(sizeof(Data));
291 Data *prev = data.load(memory_order_acquire);
295 succ = data.compare_exchange_strong(prev, tmp,
296 memory_order_release, memory_order_relaxed);
297 /* Automatically generated code for commit point define check: Write_Success_Point */
300 struct anno_cp_define_check *cp_define_check = (struct anno_cp_define_check*) malloc(sizeof(struct anno_cp_define_check));
301 cp_define_check->label_num = 1;
302 cp_define_check->label_name = "Write_Success_Point";
303 cp_define_check->interface_num = 1;
304 struct spec_annotation *annotation_cp_define_check = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
305 annotation_cp_define_check->type = CP_DEFINE_CHECK;
306 annotation_cp_define_check->annotation = cp_define_check;
307 cdsannotate(SPEC_ANALYSIS, annotation_cp_define_check);
315 void threadA(void *arg) {
319 void threadB(void *arg) {
323 void threadC(void *arg) {
327 void threadD(void *arg) {
329 printf("ThreadD: d1=%d, d2=%d\n", d->data1, d->data2);
332 int user_main(int argc, char **argv) {
336 thrd_t t1, t2, t3, t4;
337 Data *dataInit = (Data*) malloc(sizeof(Data));
340 atomic_init(&data, dataInit);
342 thrd_create(&t1, threadA, NULL);
343 thrd_create(&t2, threadB, NULL);
344 thrd_create(&t4, threadD, NULL);