7 #include <cdsannotate.h>
8 #include <specannotation.h>
9 #include <model_memory.h>
14 #define RW_LOCK_BIAS 0x00100000
15 #define WRITE_LOCK_CMP RW_LOCK_BIAS
27 /* All other user-defined structs */
28 static bool writer_lock_acquired;
29 static int reader_lock_cnt;
30 /* All other user-defined functions */
31 /* Definition of interface info struct: Write_Trylock */
32 typedef struct Write_Trylock_info {
36 /* End of info struct definition: Write_Trylock */
38 /* ID function of interface: Write_Trylock */
39 inline static call_id_t Write_Trylock_id(void *info, thread_id_t __TID__) {
40 Write_Trylock_info* theInfo = (Write_Trylock_info*)info;
41 int __RET__ = theInfo->__RET__;
42 rwlock_t * rw = theInfo->rw;
47 /* End of ID function: Write_Trylock */
49 /* Check action function of interface: Write_Trylock */
50 inline static bool Write_Trylock_check_action(void *info, call_id_t __ID__, thread_id_t __TID__) {
52 Write_Trylock_info* theInfo = (Write_Trylock_info*)info;
53 int __RET__ = theInfo->__RET__;
54 rwlock_t * rw = theInfo->rw;
56 if ( __RET__ == 1 ) writer_lock_acquired = true ;
59 /* End of check action function: Write_Trylock */
61 /* Definition of interface info struct: Read_Trylock */
62 typedef struct Read_Trylock_info {
66 /* End of info struct definition: Read_Trylock */
68 /* ID function of interface: Read_Trylock */
69 inline static call_id_t Read_Trylock_id(void *info, thread_id_t __TID__) {
70 Read_Trylock_info* theInfo = (Read_Trylock_info*)info;
71 int __RET__ = theInfo->__RET__;
72 rwlock_t * rw = theInfo->rw;
77 /* End of ID function: Read_Trylock */
79 /* Check action function of interface: Read_Trylock */
80 inline static bool Read_Trylock_check_action(void *info, call_id_t __ID__, thread_id_t __TID__) {
82 Read_Trylock_info* theInfo = (Read_Trylock_info*)info;
83 int __RET__ = theInfo->__RET__;
84 rwlock_t * rw = theInfo->rw;
86 if ( __RET__ ) reader_lock_cnt ++ ;
87 check_passed = __RET__ == ! writer_lock_acquired || ! __RET__;
92 /* End of check action function: Read_Trylock */
94 /* Definition of interface info struct: Write_Lock */
95 typedef struct Write_Lock_info {
98 /* End of info struct definition: Write_Lock */
100 /* ID function of interface: Write_Lock */
101 inline static call_id_t Write_Lock_id(void *info, thread_id_t __TID__) {
102 Write_Lock_info* theInfo = (Write_Lock_info*)info;
103 rwlock_t * rw = theInfo->rw;
105 call_id_t __ID__ = 0;
108 /* End of ID function: Write_Lock */
110 /* Check action function of interface: Write_Lock */
111 inline static bool Write_Lock_check_action(void *info, call_id_t __ID__, thread_id_t __TID__) {
113 Write_Lock_info* theInfo = (Write_Lock_info*)info;
114 rwlock_t * rw = theInfo->rw;
116 check_passed = ! writer_lock_acquired && reader_lock_cnt == 0;
119 writer_lock_acquired = true ;
122 /* End of check action function: Write_Lock */
124 /* Definition of interface info struct: Write_Unlock */
125 typedef struct Write_Unlock_info {
128 /* End of info struct definition: Write_Unlock */
130 /* ID function of interface: Write_Unlock */
131 inline static call_id_t Write_Unlock_id(void *info, thread_id_t __TID__) {
132 Write_Unlock_info* theInfo = (Write_Unlock_info*)info;
133 rwlock_t * rw = theInfo->rw;
135 call_id_t __ID__ = 0;
138 /* End of ID function: Write_Unlock */
140 /* Check action function of interface: Write_Unlock */
141 inline static bool Write_Unlock_check_action(void *info, call_id_t __ID__, thread_id_t __TID__) {
143 Write_Unlock_info* theInfo = (Write_Unlock_info*)info;
144 rwlock_t * rw = theInfo->rw;
146 check_passed = reader_lock_cnt == 0 && writer_lock_acquired;
149 writer_lock_acquired = false ;
152 /* End of check action function: Write_Unlock */
154 /* Definition of interface info struct: Read_Unlock */
155 typedef struct Read_Unlock_info {
158 /* End of info struct definition: Read_Unlock */
160 /* ID function of interface: Read_Unlock */
161 inline static call_id_t Read_Unlock_id(void *info, thread_id_t __TID__) {
162 Read_Unlock_info* theInfo = (Read_Unlock_info*)info;
163 rwlock_t * rw = theInfo->rw;
165 call_id_t __ID__ = 0;
168 /* End of ID function: Read_Unlock */
170 /* Check action function of interface: Read_Unlock */
171 inline static bool Read_Unlock_check_action(void *info, call_id_t __ID__, thread_id_t __TID__) {
173 Read_Unlock_info* theInfo = (Read_Unlock_info*)info;
174 rwlock_t * rw = theInfo->rw;
176 check_passed = reader_lock_cnt > 0 && ! writer_lock_acquired;
182 /* End of check action function: Read_Unlock */
184 /* Definition of interface info struct: Read_Lock */
185 typedef struct Read_Lock_info {
188 /* End of info struct definition: Read_Lock */
190 /* ID function of interface: Read_Lock */
191 inline static call_id_t Read_Lock_id(void *info, thread_id_t __TID__) {
192 Read_Lock_info* theInfo = (Read_Lock_info*)info;
193 rwlock_t * rw = theInfo->rw;
195 call_id_t __ID__ = 0;
198 /* End of ID function: Read_Lock */
200 /* Check action function of interface: Read_Lock */
201 inline static bool Read_Lock_check_action(void *info, call_id_t __ID__, thread_id_t __TID__) {
203 Read_Lock_info* theInfo = (Read_Lock_info*)info;
204 rwlock_t * rw = theInfo->rw;
206 check_passed = ! writer_lock_acquired;
212 /* End of check action function: Read_Lock */
214 #define INTERFACE_SIZE 6
215 static void** func_ptr_table;
216 static hb_rule** hb_rule_table;
217 static commutativity_rule** commutativity_rule_table;
218 inline static bool CommutativityCondition0(void *info1, void *info2) {
219 Read_Lock_info *_info1 = (Read_Lock_info*) info1;
220 Read_Lock_info *_info2 = (Read_Lock_info*) info2;
223 inline static bool CommutativityCondition1(void *info1, void *info2) {
224 Read_Lock_info *_info1 = (Read_Lock_info*) info1;
225 Read_Unlock_info *_info2 = (Read_Unlock_info*) info2;
228 inline static bool CommutativityCondition2(void *info1, void *info2) {
229 Read_Lock_info *_info1 = (Read_Lock_info*) info1;
230 Read_Trylock_info *_info2 = (Read_Trylock_info*) info2;
233 inline static bool CommutativityCondition3(void *info1, void *info2) {
234 Read_Lock_info *_info1 = (Read_Lock_info*) info1;
235 Write_Trylock_info *_info2 = (Write_Trylock_info*) info2;
236 return ! _info2-> __RET__;
238 inline static bool CommutativityCondition4(void *info1, void *info2) {
239 Read_Unlock_info *_info1 = (Read_Unlock_info*) info1;
240 Read_Unlock_info *_info2 = (Read_Unlock_info*) info2;
243 inline static bool CommutativityCondition5(void *info1, void *info2) {
244 Read_Unlock_info *_info1 = (Read_Unlock_info*) info1;
245 Read_Trylock_info *_info2 = (Read_Trylock_info*) info2;
248 inline static bool CommutativityCondition6(void *info1, void *info2) {
249 Read_Unlock_info *_info1 = (Read_Unlock_info*) info1;
250 Write_Trylock_info *_info2 = (Write_Trylock_info*) info2;
251 return ! _info2-> __RET__;
253 inline static bool CommutativityCondition7(void *info1, void *info2) {
254 Read_Trylock_info *_info1 = (Read_Trylock_info*) info1;
255 Read_Trylock_info *_info2 = (Read_Trylock_info*) info2;
258 inline static bool CommutativityCondition8(void *info1, void *info2) {
259 Read_Trylock_info *_info1 = (Read_Trylock_info*) info1;
260 Write_Trylock_info *_info2 = (Write_Trylock_info*) info2;
261 return ! _info1-> __RET__ || ! _info2-> __RET__;
263 inline static bool CommutativityCondition9(void *info1, void *info2) {
264 Read_Trylock_info *_info1 = (Read_Trylock_info*) info1;
265 Write_Lock_info *_info2 = (Write_Lock_info*) info2;
266 return ! _info1-> __RET__;
268 inline static bool CommutativityCondition10(void *info1, void *info2) {
269 Read_Trylock_info *_info1 = (Read_Trylock_info*) info1;
270 Write_Unlock_info *_info2 = (Write_Unlock_info*) info2;
271 return ! _info1-> __RET__;
273 inline static bool CommutativityCondition11(void *info1, void *info2) {
274 Write_Trylock_info *_info1 = (Write_Trylock_info*) info1;
275 Write_Trylock_info *_info2 = (Write_Trylock_info*) info2;
276 return ! _info1-> __RET__ || ! _info2-> __RET__;
278 inline static bool CommutativityCondition12(void *info1, void *info2) {
279 Write_Trylock_info *_info1 = (Write_Trylock_info*) info1;
280 Write_Unlock_info *_info2 = (Write_Unlock_info*) info2;
281 return ! _info1-> __RET__;
283 inline static bool CommutativityCondition13(void *info1, void *info2) {
284 Write_Trylock_info *_info1 = (Write_Trylock_info*) info1;
285 Write_Lock_info *_info2 = (Write_Lock_info*) info2;
286 return ! _info1-> __RET__;
289 /* Initialization of sequential varialbes */
290 static void __SPEC_INIT__() {
291 writer_lock_acquired = false ;
292 reader_lock_cnt = 0 ;
295 /* Cleanup routine of sequential variables */
296 static bool __SPEC_CLEANUP__() {
300 /* Define function for sequential code initialization */
301 inline static void __sequential_init() {
302 /* Init func_ptr_table */
303 func_ptr_table = (void**) malloc(sizeof(void*) * 6 * 2);
304 func_ptr_table[2 * 3] = (void*) &Write_Trylock_id;
305 func_ptr_table[2 * 3 + 1] = (void*) &Write_Trylock_check_action;
306 func_ptr_table[2 * 2] = (void*) &Read_Trylock_id;
307 func_ptr_table[2 * 2 + 1] = (void*) &Read_Trylock_check_action;
308 func_ptr_table[2 * 1] = (void*) &Write_Lock_id;
309 func_ptr_table[2 * 1 + 1] = (void*) &Write_Lock_check_action;
310 func_ptr_table[2 * 5] = (void*) &Write_Unlock_id;
311 func_ptr_table[2 * 5 + 1] = (void*) &Write_Unlock_check_action;
312 func_ptr_table[2 * 4] = (void*) &Read_Unlock_id;
313 func_ptr_table[2 * 4 + 1] = (void*) &Read_Unlock_check_action;
314 func_ptr_table[2 * 0] = (void*) &Read_Lock_id;
315 func_ptr_table[2 * 0 + 1] = (void*) &Read_Lock_check_action;
316 /* Read_Unlock(true) -> Write_Lock(true) */
317 struct hb_rule *hbConditionInit0 = (struct hb_rule*) malloc(sizeof(struct hb_rule));
318 hbConditionInit0->interface_num_before = 4; // Read_Unlock
319 hbConditionInit0->hb_condition_num_before = 0; //
320 hbConditionInit0->interface_num_after = 1; // Write_Lock
321 hbConditionInit0->hb_condition_num_after = 0; //
322 /* Read_Unlock(true) -> Write_Trylock(HB_Write_Trylock_Succ) */
323 struct hb_rule *hbConditionInit1 = (struct hb_rule*) malloc(sizeof(struct hb_rule));
324 hbConditionInit1->interface_num_before = 4; // Read_Unlock
325 hbConditionInit1->hb_condition_num_before = 0; //
326 hbConditionInit1->interface_num_after = 3; // Write_Trylock
327 hbConditionInit1->hb_condition_num_after = 1; // HB_Write_Trylock_Succ
328 /* Write_Unlock(true) -> Write_Lock(true) */
329 struct hb_rule *hbConditionInit2 = (struct hb_rule*) malloc(sizeof(struct hb_rule));
330 hbConditionInit2->interface_num_before = 5; // Write_Unlock
331 hbConditionInit2->hb_condition_num_before = 0; //
332 hbConditionInit2->interface_num_after = 1; // Write_Lock
333 hbConditionInit2->hb_condition_num_after = 0; //
334 /* Write_Unlock(true) -> Write_Trylock(HB_Write_Trylock_Succ) */
335 struct hb_rule *hbConditionInit3 = (struct hb_rule*) malloc(sizeof(struct hb_rule));
336 hbConditionInit3->interface_num_before = 5; // Write_Unlock
337 hbConditionInit3->hb_condition_num_before = 0; //
338 hbConditionInit3->interface_num_after = 3; // Write_Trylock
339 hbConditionInit3->hb_condition_num_after = 1; // HB_Write_Trylock_Succ
340 /* Write_Unlock(true) -> Read_Lock(true) */
341 struct hb_rule *hbConditionInit4 = (struct hb_rule*) malloc(sizeof(struct hb_rule));
342 hbConditionInit4->interface_num_before = 5; // Write_Unlock
343 hbConditionInit4->hb_condition_num_before = 0; //
344 hbConditionInit4->interface_num_after = 0; // Read_Lock
345 hbConditionInit4->hb_condition_num_after = 0; //
346 /* Write_Unlock(true) -> Read_Trylock(HB_Read_Trylock_Succ) */
347 struct hb_rule *hbConditionInit5 = (struct hb_rule*) malloc(sizeof(struct hb_rule));
348 hbConditionInit5->interface_num_before = 5; // Write_Unlock
349 hbConditionInit5->hb_condition_num_before = 0; //
350 hbConditionInit5->interface_num_after = 2; // Read_Trylock
351 hbConditionInit5->hb_condition_num_after = 2; // HB_Read_Trylock_Succ
352 /* Init hb_rule_table */
353 hb_rule_table = (hb_rule**) malloc(sizeof(hb_rule*) * 6);
354 #define HB_RULE_TABLE_SIZE 6
355 hb_rule_table[0] = hbConditionInit0;
356 hb_rule_table[1] = hbConditionInit1;
357 hb_rule_table[2] = hbConditionInit2;
358 hb_rule_table[3] = hbConditionInit3;
359 hb_rule_table[4] = hbConditionInit4;
360 hb_rule_table[5] = hbConditionInit5;
361 /* Init commutativity_rule_table */
362 commutativity_rule_table = (commutativity_rule**) malloc(sizeof(commutativity_rule*) * 14);
363 commutativity_rule* rule;
364 rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
365 rule->interface_num_before = 0;
366 rule->interface_num_after = 0;
368 rule->condition = CommutativityCondition0;
369 commutativity_rule_table[0] = rule;
370 rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
371 rule->interface_num_before = 0;
372 rule->interface_num_after = 4;
374 rule->condition = CommutativityCondition1;
375 commutativity_rule_table[1] = rule;
376 rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
377 rule->interface_num_before = 0;
378 rule->interface_num_after = 2;
380 rule->condition = CommutativityCondition2;
381 commutativity_rule_table[2] = rule;
382 rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
383 rule->interface_num_before = 0;
384 rule->interface_num_after = 3;
385 rule->rule = "! _Method2 . __RET__";
386 rule->condition = CommutativityCondition3;
387 commutativity_rule_table[3] = rule;
388 rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
389 rule->interface_num_before = 4;
390 rule->interface_num_after = 4;
392 rule->condition = CommutativityCondition4;
393 commutativity_rule_table[4] = rule;
394 rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
395 rule->interface_num_before = 4;
396 rule->interface_num_after = 2;
398 rule->condition = CommutativityCondition5;
399 commutativity_rule_table[5] = rule;
400 rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
401 rule->interface_num_before = 4;
402 rule->interface_num_after = 3;
403 rule->rule = "! _Method2 . __RET__";
404 rule->condition = CommutativityCondition6;
405 commutativity_rule_table[6] = rule;
406 rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
407 rule->interface_num_before = 2;
408 rule->interface_num_after = 2;
410 rule->condition = CommutativityCondition7;
411 commutativity_rule_table[7] = rule;
412 rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
413 rule->interface_num_before = 2;
414 rule->interface_num_after = 3;
415 rule->rule = "! _Method1 . __RET__ || ! _Method2 . __RET__";
416 rule->condition = CommutativityCondition8;
417 commutativity_rule_table[8] = rule;
418 rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
419 rule->interface_num_before = 2;
420 rule->interface_num_after = 1;
421 rule->rule = "! _Method1 . __RET__";
422 rule->condition = CommutativityCondition9;
423 commutativity_rule_table[9] = rule;
424 rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
425 rule->interface_num_before = 2;
426 rule->interface_num_after = 5;
427 rule->rule = "! _Method1 . __RET__";
428 rule->condition = CommutativityCondition10;
429 commutativity_rule_table[10] = rule;
430 rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
431 rule->interface_num_before = 3;
432 rule->interface_num_after = 3;
433 rule->rule = "! _Method1 . __RET__ || ! _Method2 . __RET__";
434 rule->condition = CommutativityCondition11;
435 commutativity_rule_table[11] = rule;
436 rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
437 rule->interface_num_before = 3;
438 rule->interface_num_after = 5;
439 rule->rule = "! _Method1 . __RET__";
440 rule->condition = CommutativityCondition12;
441 commutativity_rule_table[12] = rule;
442 rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
443 rule->interface_num_before = 3;
444 rule->interface_num_after = 1;
445 rule->rule = "! _Method1 . __RET__";
446 rule->condition = CommutativityCondition13;
447 commutativity_rule_table[13] = rule;
448 /* Pass init info, including function table info & HB rules & Commutativity Rules */
449 struct anno_init *anno_init = (struct anno_init*) malloc(sizeof(struct anno_init));
450 anno_init->init_func = (void_func_t) __SPEC_INIT__;
451 anno_init->cleanup_func = (cleanup_func_t) __SPEC_CLEANUP__;
452 anno_init->func_table = func_ptr_table;
453 anno_init->func_table_size = INTERFACE_SIZE;
454 anno_init->hb_rule_table = hb_rule_table;
455 anno_init->hb_rule_table_size = HB_RULE_TABLE_SIZE;
456 anno_init->commutativity_rule_table = commutativity_rule_table;
457 anno_init->commutativity_rule_table_size = 14;
458 struct spec_annotation *init = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
460 init->annotation = anno_init;
461 cdsannotate(SPEC_ANALYSIS, init);
465 /* End of Global construct generation in class */
468 static inline int read_can_lock(rwlock_t *lock)
470 return atomic_load_explicit(&lock->lock, memory_order_relaxed) > 0;
473 static inline int write_can_lock(rwlock_t *lock)
475 return atomic_load_explicit(&lock->lock, memory_order_relaxed) == RW_LOCK_BIAS;
479 void __wrapper__read_lock(rwlock_t * rw);
481 void read_lock(rwlock_t * rw) {
482 /* Interface begins */
483 struct anno_interface_begin *interface_begin = (struct anno_interface_begin*) malloc(sizeof(struct anno_interface_begin));
484 interface_begin->interface_num = 0; // Read_Lock
485 interface_begin->interface_name = "Read_Lock";
486 struct spec_annotation *annotation_interface_begin = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
487 annotation_interface_begin->type = INTERFACE_BEGIN;
488 annotation_interface_begin->annotation = interface_begin;
489 cdsannotate(SPEC_ANALYSIS, annotation_interface_begin);
490 __wrapper__read_lock(rw);
491 struct anno_hb_condition *hb_condition = (struct anno_hb_condition*) malloc(sizeof(struct anno_hb_condition));
492 hb_condition->interface_num = 0; // Read_Lock
493 hb_condition->hb_condition_num = 0;
494 struct spec_annotation *annotation_hb_condition = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
495 annotation_hb_condition->type = HB_CONDITION;
496 annotation_hb_condition->annotation = hb_condition;
497 cdsannotate(SPEC_ANALYSIS, annotation_hb_condition);
499 Read_Lock_info* info = (Read_Lock_info*) malloc(sizeof(Read_Lock_info));
501 struct anno_interface_end *interface_end = (struct anno_interface_end*) malloc(sizeof(struct anno_interface_end));
502 interface_end->interface_num = 0; // Read_Lock
503 interface_end->info = info;
504 struct spec_annotation *annoation_interface_end = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
505 annoation_interface_end->type = INTERFACE_END;
506 annoation_interface_end->annotation = interface_end;
507 cdsannotate(SPEC_ANALYSIS, annoation_interface_end);
510 void __wrapper__read_lock(rwlock_t * rw)
514 int priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
515 /* Automatically generated code for commit point define check: Read_Lock_Success_1 */
517 if (priorvalue > 0) {
518 struct anno_cp_define_check *cp_define_check = (struct anno_cp_define_check*) malloc(sizeof(struct anno_cp_define_check));
519 cp_define_check->label_num = 0;
520 cp_define_check->label_name = "Read_Lock_Success_1";
521 cp_define_check->interface_num = 0;
522 struct spec_annotation *annotation_cp_define_check = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
523 annotation_cp_define_check->type = CP_DEFINE_CHECK;
524 annotation_cp_define_check->annotation = cp_define_check;
525 cdsannotate(SPEC_ANALYSIS, annotation_cp_define_check);
528 while (priorvalue <= 0) {
529 atomic_fetch_add_explicit(&rw->lock, 1, memory_order_relaxed);
530 while (atomic_load_explicit(&rw->lock, memory_order_relaxed) <= 0) {
534 priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
535 /* Automatically generated code for commit point define check: Read_Lock_Success_2 */
537 if (priorvalue > 0) {
538 struct anno_cp_define_check *cp_define_check = (struct anno_cp_define_check*) malloc(sizeof(struct anno_cp_define_check));
539 cp_define_check->label_num = 1;
540 cp_define_check->label_name = "Read_Lock_Success_2";
541 cp_define_check->interface_num = 0;
542 struct spec_annotation *annotation_cp_define_check = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
543 annotation_cp_define_check->type = CP_DEFINE_CHECK;
544 annotation_cp_define_check->annotation = cp_define_check;
545 cdsannotate(SPEC_ANALYSIS, annotation_cp_define_check);
552 void __wrapper__write_lock(rwlock_t * rw);
554 void write_lock(rwlock_t * rw) {
555 /* Interface begins */
556 struct anno_interface_begin *interface_begin = (struct anno_interface_begin*) malloc(sizeof(struct anno_interface_begin));
557 interface_begin->interface_num = 1; // Write_Lock
558 interface_begin->interface_name = "Write_Lock";
559 struct spec_annotation *annotation_interface_begin = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
560 annotation_interface_begin->type = INTERFACE_BEGIN;
561 annotation_interface_begin->annotation = interface_begin;
562 cdsannotate(SPEC_ANALYSIS, annotation_interface_begin);
563 __wrapper__write_lock(rw);
564 struct anno_hb_condition *hb_condition = (struct anno_hb_condition*) malloc(sizeof(struct anno_hb_condition));
565 hb_condition->interface_num = 1; // Write_Lock
566 hb_condition->hb_condition_num = 0;
567 struct spec_annotation *annotation_hb_condition = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
568 annotation_hb_condition->type = HB_CONDITION;
569 annotation_hb_condition->annotation = hb_condition;
570 cdsannotate(SPEC_ANALYSIS, annotation_hb_condition);
572 Write_Lock_info* info = (Write_Lock_info*) malloc(sizeof(Write_Lock_info));
574 struct anno_interface_end *interface_end = (struct anno_interface_end*) malloc(sizeof(struct anno_interface_end));
575 interface_end->interface_num = 1; // Write_Lock
576 interface_end->info = info;
577 struct spec_annotation *annoation_interface_end = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
578 annoation_interface_end->type = INTERFACE_END;
579 annoation_interface_end->annotation = interface_end;
580 cdsannotate(SPEC_ANALYSIS, annoation_interface_end);
583 void __wrapper__write_lock(rwlock_t * rw)
586 int priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
587 /* Automatically generated code for commit point define check: Write_Lock_Success_1 */
589 if (priorvalue == RW_LOCK_BIAS) {
590 struct anno_cp_define_check *cp_define_check = (struct anno_cp_define_check*) malloc(sizeof(struct anno_cp_define_check));
591 cp_define_check->label_num = 2;
592 cp_define_check->label_name = "Write_Lock_Success_1";
593 cp_define_check->interface_num = 1;
594 struct spec_annotation *annotation_cp_define_check = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
595 annotation_cp_define_check->type = CP_DEFINE_CHECK;
596 annotation_cp_define_check->annotation = cp_define_check;
597 cdsannotate(SPEC_ANALYSIS, annotation_cp_define_check);
600 while (priorvalue != RW_LOCK_BIAS) {
601 atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_relaxed);
602 while (atomic_load_explicit(&rw->lock, memory_order_relaxed) != RW_LOCK_BIAS) {
606 priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
607 /* Automatically generated code for commit point define check: Write_Lock_Success_2 */
609 if (priorvalue == RW_LOCK_BIAS) {
610 struct anno_cp_define_check *cp_define_check = (struct anno_cp_define_check*) malloc(sizeof(struct anno_cp_define_check));
611 cp_define_check->label_num = 3;
612 cp_define_check->label_name = "Write_Lock_Success_2";
613 cp_define_check->interface_num = 1;
614 struct spec_annotation *annotation_cp_define_check = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
615 annotation_cp_define_check->type = CP_DEFINE_CHECK;
616 annotation_cp_define_check->annotation = cp_define_check;
617 cdsannotate(SPEC_ANALYSIS, annotation_cp_define_check);
623 int __wrapper__read_trylock(rwlock_t * rw);
625 int read_trylock(rwlock_t * rw) {
626 /* Interface begins */
627 struct anno_interface_begin *interface_begin = (struct anno_interface_begin*) malloc(sizeof(struct anno_interface_begin));
628 interface_begin->interface_num = 2; // Read_Trylock
629 interface_begin->interface_name = "Read_Trylock";
630 struct spec_annotation *annotation_interface_begin = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
631 annotation_interface_begin->type = INTERFACE_BEGIN;
632 annotation_interface_begin->annotation = interface_begin;
633 cdsannotate(SPEC_ANALYSIS, annotation_interface_begin);
634 int __RET__ = __wrapper__read_trylock(rw);
636 struct anno_hb_condition *hb_condition = (struct anno_hb_condition*) malloc(sizeof(struct anno_hb_condition));
637 hb_condition->interface_num = 2; // Read_Trylock
638 hb_condition->hb_condition_num = 2;
639 struct spec_annotation *annotation_hb_condition = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
640 annotation_hb_condition->type = HB_CONDITION;
641 annotation_hb_condition->annotation = hb_condition;
642 cdsannotate(SPEC_ANALYSIS, annotation_hb_condition);
645 Read_Trylock_info* info = (Read_Trylock_info*) malloc(sizeof(Read_Trylock_info));
646 info->__RET__ = __RET__;
648 struct anno_interface_end *interface_end = (struct anno_interface_end*) malloc(sizeof(struct anno_interface_end));
649 interface_end->interface_num = 2; // Read_Trylock
650 interface_end->info = info;
651 struct spec_annotation *annoation_interface_end = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
652 annoation_interface_end->type = INTERFACE_END;
653 annoation_interface_end->annotation = interface_end;
654 cdsannotate(SPEC_ANALYSIS, annoation_interface_end);
658 int __wrapper__read_trylock(rwlock_t * rw)
661 int priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
662 /* Automatically generated code for potential commit point: Potential_Read_Trylock_Point */
665 struct anno_potential_cp_define *potential_cp_define = (struct anno_potential_cp_define*) malloc(sizeof(struct anno_potential_cp_define));
666 potential_cp_define->label_num = 4;
667 potential_cp_define->label_name = "Potential_Read_Trylock_Point";
668 struct spec_annotation *annotation_potential_cp_define = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
669 annotation_potential_cp_define->type = POTENTIAL_CP_DEFINE;
670 annotation_potential_cp_define->annotation = potential_cp_define;
671 cdsannotate(SPEC_ANALYSIS, annotation_potential_cp_define);
674 if (priorvalue > 0) {
675 /* Automatically generated code for commit point define: Read_Trylock_Succ_Point */
678 struct anno_cp_define *cp_define = (struct anno_cp_define*) malloc(sizeof(struct anno_cp_define));
679 cp_define->label_num = 5;
680 cp_define->label_name = "Read_Trylock_Succ_Point";
681 cp_define->potential_cp_label_num = 4;
682 cp_define->potential_label_name = "Potential_Read_Trylock_Point";
683 cp_define->interface_num = 2;
684 struct spec_annotation *annotation_cp_define = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
685 annotation_cp_define->type = CP_DEFINE;
686 annotation_cp_define->annotation = cp_define;
687 cdsannotate(SPEC_ANALYSIS, annotation_cp_define);
692 /* Automatically generated code for commit point define: Read_Trylock_Fail_Point */
695 struct anno_cp_define *cp_define = (struct anno_cp_define*) malloc(sizeof(struct anno_cp_define));
696 cp_define->label_num = 6;
697 cp_define->label_name = "Read_Trylock_Fail_Point";
698 cp_define->potential_cp_label_num = 4;
699 cp_define->potential_label_name = "Potential_Read_Trylock_Point";
700 cp_define->interface_num = 2;
701 struct spec_annotation *annotation_cp_define = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
702 annotation_cp_define->type = CP_DEFINE;
703 annotation_cp_define->annotation = cp_define;
704 cdsannotate(SPEC_ANALYSIS, annotation_cp_define);
707 atomic_fetch_add_explicit(&rw->lock, 1, memory_order_relaxed);
711 int __wrapper__write_trylock(rwlock_t * rw);
713 int write_trylock(rwlock_t * rw) {
714 /* Interface begins */
715 struct anno_interface_begin *interface_begin = (struct anno_interface_begin*) malloc(sizeof(struct anno_interface_begin));
716 interface_begin->interface_num = 3; // Write_Trylock
717 interface_begin->interface_name = "Write_Trylock";
718 struct spec_annotation *annotation_interface_begin = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
719 annotation_interface_begin->type = INTERFACE_BEGIN;
720 annotation_interface_begin->annotation = interface_begin;
721 cdsannotate(SPEC_ANALYSIS, annotation_interface_begin);
722 int __RET__ = __wrapper__write_trylock(rw);
724 struct anno_hb_condition *hb_condition = (struct anno_hb_condition*) malloc(sizeof(struct anno_hb_condition));
725 hb_condition->interface_num = 3; // Write_Trylock
726 hb_condition->hb_condition_num = 1;
727 struct spec_annotation *annotation_hb_condition = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
728 annotation_hb_condition->type = HB_CONDITION;
729 annotation_hb_condition->annotation = hb_condition;
730 cdsannotate(SPEC_ANALYSIS, annotation_hb_condition);
733 Write_Trylock_info* info = (Write_Trylock_info*) malloc(sizeof(Write_Trylock_info));
734 info->__RET__ = __RET__;
736 struct anno_interface_end *interface_end = (struct anno_interface_end*) malloc(sizeof(struct anno_interface_end));
737 interface_end->interface_num = 3; // Write_Trylock
738 interface_end->info = info;
739 struct spec_annotation *annoation_interface_end = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
740 annoation_interface_end->type = INTERFACE_END;
741 annoation_interface_end->annotation = interface_end;
742 cdsannotate(SPEC_ANALYSIS, annoation_interface_end);
746 int __wrapper__write_trylock(rwlock_t * rw)
749 int priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
750 /* Automatically generated code for potential commit point: Potential_Write_Trylock_Point */
753 struct anno_potential_cp_define *potential_cp_define = (struct anno_potential_cp_define*) malloc(sizeof(struct anno_potential_cp_define));
754 potential_cp_define->label_num = 7;
755 potential_cp_define->label_name = "Potential_Write_Trylock_Point";
756 struct spec_annotation *annotation_potential_cp_define = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
757 annotation_potential_cp_define->type = POTENTIAL_CP_DEFINE;
758 annotation_potential_cp_define->annotation = potential_cp_define;
759 cdsannotate(SPEC_ANALYSIS, annotation_potential_cp_define);
762 if (priorvalue == RW_LOCK_BIAS) {
763 /* Automatically generated code for commit point define: Write_Trylock_Succ_Point */
766 struct anno_cp_define *cp_define = (struct anno_cp_define*) malloc(sizeof(struct anno_cp_define));
767 cp_define->label_num = 8;
768 cp_define->label_name = "Write_Trylock_Succ_Point";
769 cp_define->potential_cp_label_num = 7;
770 cp_define->potential_label_name = "Potential_Write_Trylock_Point";
771 cp_define->interface_num = 3;
772 struct spec_annotation *annotation_cp_define = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
773 annotation_cp_define->type = CP_DEFINE;
774 annotation_cp_define->annotation = cp_define;
775 cdsannotate(SPEC_ANALYSIS, annotation_cp_define);
780 /* Automatically generated code for commit point define: Write_Trylock_Fail_Point */
783 struct anno_cp_define *cp_define = (struct anno_cp_define*) malloc(sizeof(struct anno_cp_define));
784 cp_define->label_num = 9;
785 cp_define->label_name = "Write_Trylock_Fail_Point";
786 cp_define->potential_cp_label_num = 7;
787 cp_define->potential_label_name = "Potential_Write_Trylock_Point";
788 cp_define->interface_num = 3;
789 struct spec_annotation *annotation_cp_define = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
790 annotation_cp_define->type = CP_DEFINE;
791 annotation_cp_define->annotation = cp_define;
792 cdsannotate(SPEC_ANALYSIS, annotation_cp_define);
795 atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_relaxed);
799 void __wrapper__read_unlock(rwlock_t * rw);
801 void read_unlock(rwlock_t * rw) {
802 /* Interface begins */
803 struct anno_interface_begin *interface_begin = (struct anno_interface_begin*) malloc(sizeof(struct anno_interface_begin));
804 interface_begin->interface_num = 4; // Read_Unlock
805 interface_begin->interface_name = "Read_Unlock";
806 struct spec_annotation *annotation_interface_begin = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
807 annotation_interface_begin->type = INTERFACE_BEGIN;
808 annotation_interface_begin->annotation = interface_begin;
809 cdsannotate(SPEC_ANALYSIS, annotation_interface_begin);
810 __wrapper__read_unlock(rw);
811 struct anno_hb_condition *hb_condition = (struct anno_hb_condition*) malloc(sizeof(struct anno_hb_condition));
812 hb_condition->interface_num = 4; // Read_Unlock
813 hb_condition->hb_condition_num = 0;
814 struct spec_annotation *annotation_hb_condition = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
815 annotation_hb_condition->type = HB_CONDITION;
816 annotation_hb_condition->annotation = hb_condition;
817 cdsannotate(SPEC_ANALYSIS, annotation_hb_condition);
819 Read_Unlock_info* info = (Read_Unlock_info*) malloc(sizeof(Read_Unlock_info));
821 struct anno_interface_end *interface_end = (struct anno_interface_end*) malloc(sizeof(struct anno_interface_end));
822 interface_end->interface_num = 4; // Read_Unlock
823 interface_end->info = info;
824 struct spec_annotation *annoation_interface_end = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
825 annoation_interface_end->type = INTERFACE_END;
826 annoation_interface_end->annotation = interface_end;
827 cdsannotate(SPEC_ANALYSIS, annoation_interface_end);
830 void __wrapper__read_unlock(rwlock_t * rw)
833 atomic_fetch_add_explicit(&rw->lock, 1, memory_order_release);
834 /* Automatically generated code for commit point define check: Read_Unlock_Point */
837 struct anno_cp_define_check *cp_define_check = (struct anno_cp_define_check*) malloc(sizeof(struct anno_cp_define_check));
838 cp_define_check->label_num = 10;
839 cp_define_check->label_name = "Read_Unlock_Point";
840 cp_define_check->interface_num = 4;
841 struct spec_annotation *annotation_cp_define_check = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
842 annotation_cp_define_check->type = CP_DEFINE_CHECK;
843 annotation_cp_define_check->annotation = cp_define_check;
844 cdsannotate(SPEC_ANALYSIS, annotation_cp_define_check);
849 void __wrapper__write_unlock(rwlock_t * rw);
851 void write_unlock(rwlock_t * rw) {
852 /* Interface begins */
853 struct anno_interface_begin *interface_begin = (struct anno_interface_begin*) malloc(sizeof(struct anno_interface_begin));
854 interface_begin->interface_num = 5; // Write_Unlock
855 interface_begin->interface_name = "Write_Unlock";
856 struct spec_annotation *annotation_interface_begin = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
857 annotation_interface_begin->type = INTERFACE_BEGIN;
858 annotation_interface_begin->annotation = interface_begin;
859 cdsannotate(SPEC_ANALYSIS, annotation_interface_begin);
860 __wrapper__write_unlock(rw);
861 struct anno_hb_condition *hb_condition = (struct anno_hb_condition*) malloc(sizeof(struct anno_hb_condition));
862 hb_condition->interface_num = 5; // Write_Unlock
863 hb_condition->hb_condition_num = 0;
864 struct spec_annotation *annotation_hb_condition = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
865 annotation_hb_condition->type = HB_CONDITION;
866 annotation_hb_condition->annotation = hb_condition;
867 cdsannotate(SPEC_ANALYSIS, annotation_hb_condition);
869 Write_Unlock_info* info = (Write_Unlock_info*) malloc(sizeof(Write_Unlock_info));
871 struct anno_interface_end *interface_end = (struct anno_interface_end*) malloc(sizeof(struct anno_interface_end));
872 interface_end->interface_num = 5; // Write_Unlock
873 interface_end->info = info;
874 struct spec_annotation *annoation_interface_end = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
875 annoation_interface_end->type = INTERFACE_END;
876 annoation_interface_end->annotation = interface_end;
877 cdsannotate(SPEC_ANALYSIS, annoation_interface_end);
880 void __wrapper__write_unlock(rwlock_t * rw)
883 atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_release);
884 /* Automatically generated code for commit point define check: Write_Unlock_Point */
887 struct anno_cp_define_check *cp_define_check = (struct anno_cp_define_check*) malloc(sizeof(struct anno_cp_define_check));
888 cp_define_check->label_num = 11;
889 cp_define_check->label_name = "Write_Unlock_Point";
890 cp_define_check->interface_num = 5;
891 struct spec_annotation *annotation_cp_define_check = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
892 annotation_cp_define_check->type = CP_DEFINE_CHECK;
893 annotation_cp_define_check->annotation = cp_define_check;
894 cdsannotate(SPEC_ANALYSIS, annotation_cp_define_check);
904 static void a(void *obj)
907 read_unlock(&mylock);
911 write_unlock(&mylock);
914 static void b(void *obj)
916 if (read_trylock(&mylock) == 1) {
917 read_unlock(&mylock);
920 if (write_trylock(&mylock) == 1) {
921 write_unlock(&mylock);
925 int user_main(int argc, char **argv)
930 atomic_init(&mylock.lock, RW_LOCK_BIAS);
932 thrd_create(&t1, (thrd_start_t)&a, NULL);
933 thrd_create(&t2, (thrd_start_t)&b, NULL);