output/linuxrwlocks/linuxrwlocks.c

   1 #include <stdio.h>
   2 #include <threads.h>
   3 #include <stdatomic.h>
   4
   5 #include <spec_lib.h>
   6 #include <stdlib.h>
   7 #include <cdsannotate.h>
   8 #include <specannotation.h>
   9 #include <model_memory.h>
  10 #include "common.h"
  11
  12 #include "librace.h"
  13
  14 #define RW_LOCK_BIAS            0x00100000
  15 #define WRITE_LOCK_CMP          RW_LOCK_BIAS
  16
  17 typedef union {
  18         atomic_int lock;
  19 } rwlock_t;
  20
  21
  22
  23
  24
  25
  26
  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 {
  33 int __RET__;
  34 rwlock_t * rw;
  35 } Write_Trylock_info;
  36 /* End of info struct definition: Write_Trylock */
  37
  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;
  43
  44         call_id_t __ID__ = 0;
  45         return __ID__;
  46 }
  47 /* End of ID function: Write_Trylock */
  48
  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__) {
  51         bool check_passed;
  52         Write_Trylock_info* theInfo = (Write_Trylock_info*)info;
  53         int __RET__ = theInfo->__RET__;
  54         rwlock_t * rw = theInfo->rw;
  55
  56         if ( __RET__ == 1 ) writer_lock_acquired = true ;
  57         return true;
  58 }
  59 /* End of check action function: Write_Trylock */
  60
  61 /* Definition of interface info struct: Read_Trylock */
  62 typedef struct Read_Trylock_info {
  63 int __RET__;
  64 rwlock_t * rw;
  65 } Read_Trylock_info;
  66 /* End of info struct definition: Read_Trylock */
  67
  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;
  73
  74         call_id_t __ID__ = 0;
  75         return __ID__;
  76 }
  77 /* End of ID function: Read_Trylock */
  78
  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__) {
  81         bool check_passed;
  82         Read_Trylock_info* theInfo = (Read_Trylock_info*)info;
  83         int __RET__ = theInfo->__RET__;
  84         rwlock_t * rw = theInfo->rw;
  85
  86         if ( __RET__ ) reader_lock_cnt ++ ;
  87         check_passed = __RET__ == ! writer_lock_acquired || ! __RET__;
  88         if (!check_passed)
  89                 return false;
  90         return true;
  91 }
  92 /* End of check action function: Read_Trylock */
  93
  94 /* Definition of interface info struct: Write_Lock */
  95 typedef struct Write_Lock_info {
  96 rwlock_t * rw;
  97 } Write_Lock_info;
  98 /* End of info struct definition: Write_Lock */
  99
 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;
 104
 105         call_id_t __ID__ = 0;
 106         return __ID__;
 107 }
 108 /* End of ID function: Write_Lock */
 109
 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__) {
 112         bool check_passed;
 113         Write_Lock_info* theInfo = (Write_Lock_info*)info;
 114         rwlock_t * rw = theInfo->rw;
 115
 116         check_passed = ! writer_lock_acquired && reader_lock_cnt == 0;
 117         if (!check_passed)
 118                 return false;
 119         writer_lock_acquired = true ;
 120         return true;
 121 }
 122 /* End of check action function: Write_Lock */
 123
 124 /* Definition of interface info struct: Write_Unlock */
 125 typedef struct Write_Unlock_info {
 126 rwlock_t * rw;
 127 } Write_Unlock_info;
 128 /* End of info struct definition: Write_Unlock */
 129
 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;
 134
 135         call_id_t __ID__ = 0;
 136         return __ID__;
 137 }
 138 /* End of ID function: Write_Unlock */
 139
 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__) {
 142         bool check_passed;
 143         Write_Unlock_info* theInfo = (Write_Unlock_info*)info;
 144         rwlock_t * rw = theInfo->rw;
 145
 146         check_passed = reader_lock_cnt == 0 && writer_lock_acquired;
 147         if (!check_passed)
 148                 return false;
 149         writer_lock_acquired = false ;
 150         return true;
 151 }
 152 /* End of check action function: Write_Unlock */
 153
 154 /* Definition of interface info struct: Read_Unlock */
 155 typedef struct Read_Unlock_info {
 156 rwlock_t * rw;
 157 } Read_Unlock_info;
 158 /* End of info struct definition: Read_Unlock */
 159
 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;
 164
 165         call_id_t __ID__ = 0;
 166         return __ID__;
 167 }
 168 /* End of ID function: Read_Unlock */
 169
 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__) {
 172         bool check_passed;
 173         Read_Unlock_info* theInfo = (Read_Unlock_info*)info;
 174         rwlock_t * rw = theInfo->rw;
 175
 176         check_passed = reader_lock_cnt > 0 && ! writer_lock_acquired;
 177         if (!check_passed)
 178                 return false;
 179         reader_lock_cnt -- ;
 180         return true;
 181 }
 182 /* End of check action function: Read_Unlock */
 183
 184 /* Definition of interface info struct: Read_Lock */
 185 typedef struct Read_Lock_info {
 186 rwlock_t * rw;
 187 } Read_Lock_info;
 188 /* End of info struct definition: Read_Lock */
 189
 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;
 194
 195         call_id_t __ID__ = 0;
 196         return __ID__;
 197 }
 198 /* End of ID function: Read_Lock */
 199
 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__) {
 202         bool check_passed;
 203         Read_Lock_info* theInfo = (Read_Lock_info*)info;
 204         rwlock_t * rw = theInfo->rw;
 205
 206         check_passed = ! writer_lock_acquired;
 207         if (!check_passed)
 208                 return false;
 209         reader_lock_cnt ++ ;
 210         return true;
 211 }
 212 /* End of check action function: Read_Lock */
 213
 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;
 221         return true;
 222 }
 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;
 226         return true;
 227 }
 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;
 231         return true;
 232 }
 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__;
 237 }
 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;
 241         return true;
 242 }
 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;
 246         return true;
 247 }
 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__;
 252 }
 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;
 256         return true;
 257 }
 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__;
 262 }
 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__;
 267 }
 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__;
 272 }
 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__;
 277 }
 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__;
 282 }
 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__;
 287 }
 288
 289 /* Initialization of sequential varialbes */
 290 static void __SPEC_INIT__() {
 291         writer_lock_acquired = false ;
 292         reader_lock_cnt = 0 ;
 293 }
 294
 295 /* Cleanup routine of sequential variables */
 296 static bool __SPEC_CLEANUP__() {
 297         return true;
 298 }
 299
 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;
 367         rule->rule = "true";
 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;
 373         rule->rule = "true";
 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;
 379         rule->rule = "true";
 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;
 391         rule->rule = "true";
 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;
 397         rule->rule = "true";
 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;
 409         rule->rule = "true";
 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));
 459         init->type = INIT;
 460         init->annotation = anno_init;
 461         cdsannotate(SPEC_ANALYSIS, init);
 462
 463 }
 464
 465 /* End of Global construct generation in class */
 466
 467
 468 static inline int read_can_lock(rwlock_t *lock)
 469 {
 470         return atomic_load_explicit(&lock->lock, memory_order_relaxed) > 0;
 471 }
 472
 473 static inline int write_can_lock(rwlock_t *lock)
 474 {
 475         return atomic_load_explicit(&lock->lock, memory_order_relaxed) == RW_LOCK_BIAS;
 476 }
 477
 478
 479 void __wrapper__read_lock(rwlock_t * rw);
 480
 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);
 498
 499         Read_Lock_info* info = (Read_Lock_info*) malloc(sizeof(Read_Lock_info));
 500         info->rw = rw;
 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);
 508 }
 509
 510 void __wrapper__read_lock(rwlock_t * rw)
 511 {
 512
 513
 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 */
 516
 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);
 526         }
 527
 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) {
 531                         thrd_yield();
 532                 }
 533
 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 */
 536
 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);
 546         }
 547
 548         }
 549 }
 550
 551
 552 void __wrapper__write_lock(rwlock_t * rw);
 553
 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);
 571
 572         Write_Lock_info* info = (Write_Lock_info*) malloc(sizeof(Write_Lock_info));
 573         info->rw = rw;
 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);
 581 }
 582
 583 void __wrapper__write_lock(rwlock_t * rw)
 584 {
 585
 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 */
 588
 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);
 598         }
 599
 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) {
 603                         thrd_yield();
 604                 }
 605
 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 */
 608
 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);
 618         }
 619
 620         }
 621 }
 622
 623 int __wrapper__read_trylock(rwlock_t * rw);
 624
 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);
 635         if (__RET__ == 1) {
 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);
 643         }
 644
 645         Read_Trylock_info* info = (Read_Trylock_info*) malloc(sizeof(Read_Trylock_info));
 646         info->__RET__ = __RET__;
 647         info->rw = rw;
 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);
 655         return __RET__;
 656 }
 657
 658 int __wrapper__read_trylock(rwlock_t * rw)
 659 {
 660
 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 */
 663
 664         if (true) {
 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);
 672         }
 673
 674         if (priorvalue > 0) {
 675         /* Automatically generated code for commit point define: Read_Trylock_Succ_Point */
 676
 677         if (true) {
 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);
 688         }
 689
 690                 return 1;
 691         }
 692         /* Automatically generated code for commit point define: Read_Trylock_Fail_Point */
 693
 694         if (true) {
 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);
 705         }
 706
 707         atomic_fetch_add_explicit(&rw->lock, 1, memory_order_relaxed);
 708         return 0;
 709 }
 710
 711 int __wrapper__write_trylock(rwlock_t * rw);
 712
 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);
 723         if (__RET__ == 1) {
 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);
 731         }
 732
 733         Write_Trylock_info* info = (Write_Trylock_info*) malloc(sizeof(Write_Trylock_info));
 734         info->__RET__ = __RET__;
 735         info->rw = rw;
 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);
 743         return __RET__;
 744 }
 745
 746 int __wrapper__write_trylock(rwlock_t * rw)
 747 {
 748
 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 */
 751
 752         if (true) {
 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);
 760         }
 761
 762         if (priorvalue == RW_LOCK_BIAS) {
 763         /* Automatically generated code for commit point define: Write_Trylock_Succ_Point */
 764
 765         if (true) {
 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);
 776         }
 777
 778                 return 1;
 779         }
 780         /* Automatically generated code for commit point define: Write_Trylock_Fail_Point */
 781
 782         if (true) {
 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);
 793         }
 794
 795         atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_relaxed);
 796         return 0;
 797 }
 798
 799 void __wrapper__read_unlock(rwlock_t * rw);
 800
 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);
 818
 819         Read_Unlock_info* info = (Read_Unlock_info*) malloc(sizeof(Read_Unlock_info));
 820         info->rw = rw;
 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);
 828 }
 829
 830 void __wrapper__read_unlock(rwlock_t * rw)
 831 {
 832
 833         atomic_fetch_add_explicit(&rw->lock, 1, memory_order_release);
 834         /* Automatically generated code for commit point define check: Read_Unlock_Point */
 835
 836         if (true) {
 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);
 845         }
 846
 847 }
 848
 849 void __wrapper__write_unlock(rwlock_t * rw);
 850
 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);
 868
 869         Write_Unlock_info* info = (Write_Unlock_info*) malloc(sizeof(Write_Unlock_info));
 870         info->rw = rw;
 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);
 878 }
 879
 880 void __wrapper__write_unlock(rwlock_t * rw)
 881 {
 882
 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 */
 885
 886         if (true) {
 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);
 895         }
 896
 897
 898
 899 }
 900
 901 rwlock_t mylock;
 902 int shareddata;
 903
 904 static void a(void *obj)
 905 {
 906         read_lock(&mylock);
 907                         read_unlock(&mylock);
 908
 909         write_lock(&mylock);
 910                 shareddata = 47;
 911         write_unlock(&mylock);
 912 }
 913
 914 static void b(void *obj)
 915 {
 916         if (read_trylock(&mylock) == 1) {
 917                                 read_unlock(&mylock);
 918         }
 919
 920         if (write_trylock(&mylock) == 1) {
 921                                 write_unlock(&mylock);
 922         }
 923 }
 924
 925 int user_main(int argc, char **argv)
 926 {
 927         __sequential_init();
 928
 929         thrd_t t1, t2;
 930         atomic_init(&mylock.lock, RW_LOCK_BIAS);
 931
 932         thrd_create(&t1, (thrd_start_t)&a, NULL);
 933         thrd_create(&t2, (thrd_start_t)&b, NULL);
 934
 935         thrd_join(t1);
 936         thrd_join(t2);
 937
 938         return 0;
 939 }
 940