benchmark/trylock/trylock.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
  15 atomic<bool> flag(false); // Shared variables
  16 /**
  17 @Structure_Define:
  18 @DeclareVar: bool locked;
  19 @InitVar: locked = false;
  20 @Happens_Before: Unlock -> Try_Lock(Trylock_Succ)
  21 */
  22
  23 /**
  24 @Method: Try_Lock
  25 @Commit_Point_Set:
  26     Lock_Fail_Point | Lock_Succ_Point
  27 @HB_Condition:
  28     Trylock_Succ :: __RET__
  29 @ID: DEFAULT
  30 @PreCondition:
  31     (!locked && __RET__) || (locked && !__RET__)
  32 @SideEffect:
  33     if (__RET__) locked = true;
  34 */
  35 bool try_lock() {
  36     bool succ = flag.compare_exchange_strong(false,/*@ \label{line:extendedlock_CAS} @*/
  37         true, memory_order_acquire,
  38             memory_order_relaxed);
  39     /**
  40     @Commit_Point_Label_Check: succ
  41     @Label: Lock_Succ_Point
  42     @End
  43     */
  44     /**
  45     @Commit_Point_Label_Check: !succ
  46     @Label: Lock_Fail_Point
  47     @End
  48     */
  49     return succ;
  50 }
  51
  52 /**
  53 @Method: Lock
  54 @Commit_Point_Set: Lock_Succ_Point
  55 @ID: DEFAULT
  56 @PreCondition: !locked
  57 @SideEffect: locked = true;
  58 */
  59 void lock() {
  60     do {
  61         bool succ = try_lock();/*@ \label{line:lockacquirespec} @*/
  62     } while (!succ);
  63 }
  64
  65 /**
  66 @Method: Unlock
  67 @Commit_Point_Set: Unlock_Point
  68 @ID: DEFAULT
  69 @PreCondition: locked
  70 @SideEffect: locked = false;
  71 */
  72 void unlock() {
  73     flag.store(false, memory_order_release);/*@ \label{line:unlock_store} @*/
  74     /**
  75     @Commit_Point_Label_Check: true
  76     @Label: Unlock_Point
  77     */
  78 }
  79
  80 static void b(void *obj)
  81 {
  82         int i;
  83         for(i = 0; i < 2; i++) {
  84                 if ((i % 2) == 0) {
  85                         if (read_trylock(&mylock) == 1) {
  86                                 //printf("%d\n", shareddata);
  87                                 read_unlock(&mylock);
  88                         }
  89                 } else {
  90                         if (write_trylock(&mylock) == 1) {
  91                                 //shareddata = 47;
  92                                 write_unlock(&mylock);
  93                         }
  94                 }
  95         }
  96 }
  97
  98 int user_main(int argc, char **argv)
  99 {
 100         /**
 101                 @Begin
 102                 @Entry_point
 103                 @End
 104         */
 105         thrd_t t1, t2;
 106         atomic_init(&mylock.lock, RW_LOCK_BIAS);
 107
 108         thrd_create(&t1, (thrd_start_t)&a, NULL);
 109         thrd_create(&t2, (thrd_start_t)&b, NULL);
 110
 111         thrd_join(t1);
 112         thrd_join(t2);
 113
 114         return 0;
 115 }