benchmark/linuxrwlocks/linuxrwlocks.c

   1 #include <stdio.h>
   2 #include <threads.h>
   3 #include <stdatomic.h>
   4
   5 #include "librace.h"
   6
   7 #define RW_LOCK_BIAS            0x00100000
   8 #define WRITE_LOCK_CMP          RW_LOCK_BIAS
   9
  10 /** Example implementation of linux rw lock along with 2 thread test
  11  *  driver... */
  12
  13 /**
  14         Properties to check:
  15         1. At most 1 thread can acquire the write lock, and at the same time, no
  16                 other threads can acquire any lock (including read/write lock).
  17         2. At most RW_LOCK_BIAS threads can successfully acquire the read lock.
  18         3. A read_unlock release 1 read lock, and a write_unlock release the write
  19         lock. They can not release a lock that they don't acquire.
  20         ###
  21         4. Read_lock and write_lock can not be grabbed at the same time.
  22         5. Happpens-before relationship should be checked and guaranteed, which
  23         should be as the following:
  24                 a. read_unlock hb-> write_lock
  25                 b. write_unlock hb-> write_lock
  26                 c. write_unlock hb-> read_lock
  27 */
  28
  29 /**
  30         Interesting point for locks:
  31         a. If the users unlock() before any lock(), then the model checker will fail.
  32         For this case, we can not say that the data structure is buggy, how can we
  33         tell them from a real data structure bug???
  34         b. We should specify that for a specific thread, successful locks and
  35         unlocks should always come in pairs. We could make this check as an
  36         auxiliary check since it is an extra rule for how the interfaces should called.
  37 */
  38
  39 /**
  40         @Begin
  41         @Global_define:
  42                 @DeclareVar:
  43                         bool writer_lock_acquired;
  44                         int reader_lock_cnt;
  45                 @InitVar:
  46                         writer_lock_acquired = false;
  47                         reader_lock_cnt = 0;
  48                 @DefineFunc:
  49         @Happens_before:
  50                 # Since commit_point_set has no ID attached, A -> B means that for any B,
  51                 # the previous A happens before B.
  52                 Read_Unlock -> Write_Lock
  53                 Read_Unlock -> Write_Trylock(HB_Write_Trylock_Succ)
  54
  55                 Write_Unlock -> Write_Lock
  56                 Write_Unlock -> Write_Trylock(HB_Write_Trylock_Succ)
  57
  58                 Write_Unlock -> Read_Lock
  59                 Write_Unlock -> Read_Trylock(HB_Read_Trylock_Succ)
  60         @End
  61 */
  62
  63 /**
  64         */
  65
  66 typedef union {
  67         atomic_int lock;
  68 } rwlock_t;
  69
  70 static inline int read_can_lock(rwlock_t *lock)
  71 {
  72         return atomic_load_explicit(&lock->lock, memory_order_relaxed) > 0;
  73 }
  74
  75 static inline int write_can_lock(rwlock_t *lock)
  76 {
  77         return atomic_load_explicit(&lock->lock, memory_order_relaxed) == RW_LOCK_BIAS;
  78 }
  79
  80
  81 /**
  82         @Begin
  83         @Interface: Read_Lock
  84         @Commit_point_set:
  85                 Read_Lock_Success_1 | Read_Lock_Success_2
  86         @Check:
  87                 !__sequential.writer_lock_acquired
  88         @Action:
  89                 @Code:
  90                 __sequential.reader_lock_cnt++;
  91         @End
  92 */
  93 static inline void read_lock(rwlock_t *rw)
  94 {
  95         int priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
  96         /**
  97                 @Begin
  98                 @Commit_point_define_check: __ATOMIC_RET__ > 0
  99                 @Label:Read_Lock_Success_1
 100                 @End
 101         */
 102         while (priorvalue <= 0) {
 103                 atomic_fetch_add_explicit(&rw->lock, 1, memory_order_relaxed);
 104                 while (atomic_load_explicit(&rw->lock, memory_order_relaxed) <= 0) {
 105                         thrd_yield();
 106                 }
 107                 priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
 108                 /**
 109                         @Begin
 110                         @Commit_point_define_check: __ATOMIC_RET__ > 0
 111                         @Label:Read_Lock_Success_2
 112                         @End
 113                 */
 114         }
 115 }
 116
 117
 118 /**
 119         @Begin
 120         @Interface: Write_Lock
 121         @Commit_point_set:
 122                 Write_Lock_Success_1 | Write_Lock_Success_2
 123         @Check:
 124                 !__sequential.writer_lock_acquired && __sequential.reader_lock_cnt == 0
 125         @Action:
 126                 @Code:
 127                 __sequential.writer_lock_acquired = true;
 128         @End
 129 */
 130 static inline void write_lock(rwlock_t *rw)
 131 {
 132         int priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
 133         /**
 134                 @Begin
 135                 @Commit_point_define_check: __ATOMIC_RET__ == RW_LOCK_BIAS
 136                 @Label: Write_Lock_Success_1
 137                 @End
 138         */
 139         while (priorvalue != RW_LOCK_BIAS) {
 140                 atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_relaxed);
 141                 while (atomic_load_explicit(&rw->lock, memory_order_relaxed) != RW_LOCK_BIAS) {
 142                         thrd_yield();
 143                 }
 144                 priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
 145                 /**
 146                         @Begin
 147                         @Commit_point_define_check: __ATOMIC_RET__ == RW_LOCK_BIAS
 148                         @Label: Write_Lock_Success_2
 149                         @End
 150                 */
 151         }
 152 }
 153
 154 /**
 155         @Begin
 156         @Interface: Read_Trylock
 157         @Commit_point_set:
 158                 Read_Trylock_Point
 159         @Condition:
 160                 __sequential.writer_lock_acquired == false
 161         @HB_condition:
 162                 HB_Read_Trylock_Succ :: __RET__ == 1
 163         @Action:
 164                 @Code:
 165                 if (__COND_SAY__)
 166                         __sequential.reader_lock_cnt++;
 167         @Post_check:
 168                 __COND_SAY__ ? __RET__ == 1 : __RET__ == 0
 169         @End
 170 */
 171 static inline int read_trylock(rwlock_t *rw)
 172 {
 173         int priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
 174         /**
 175                 @Begin
 176                 @Commit_point_define_check: true
 177                 @Label:Read_Trylock_Point
 178                 @End
 179         */
 180         if (priorvalue > 0)
 181                 return 1;
 182
 183         atomic_fetch_add_explicit(&rw->lock, 1, memory_order_relaxed);
 184         return 0;
 185 }
 186
 187 /**
 188         @Begin
 189         @Interface: Write_Trylock
 190         @Commit_point_set:
 191                 Write_Trylock_Point
 192         @Condition:
 193                 !__sequential.writer_lock_acquired && __sequential.reader_lock_cnt == 0
 194         @HB_condition:
 195                 HB_Write_Trylock_Succ :: __RET__ == 1
 196         @Action:
 197                 @Code:
 198                 if (__COND_SAY__)
 199                         __sequential.writer_lock_acquired = true;
 200         @Post_check:
 201                 __COND_SAY__ ? __RET__ == 1 : __RET__ == 0
 202         @End
 203 */
 204 static inline int write_trylock(rwlock_t *rw)
 205 {
 206         int priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
 207         /**
 208                 @Begin
 209                 @Commit_point_define_check: true
 210                 @Label: Write_Trylock_Point
 211                 @End
 212         */
 213         if (priorvalue == RW_LOCK_BIAS)
 214                 return 1;
 215
 216         atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_relaxed);
 217         return 0;
 218 }
 219
 220 /**
 221         @Begin
 222         @Interface: Read_Unlock
 223         @Commit_point_set: Read_Unlock_Point
 224         @Check:
 225                 __sequential.reader_lock_cnt > 0 && !__sequential.writer_lock_acquired
 226         @Action:
 227                 @Code:
 228                 reader_lock_cnt--;
 229         @End
 230 */
 231 static inline void read_unlock(rwlock_t *rw)
 232 {
 233         atomic_fetch_add_explicit(&rw->lock, 1, memory_order_release);
 234         /**
 235                 @Begin
 236                 @Commit_point_define_check: true
 237                 @Label: Read_Unlock_Point
 238                 @End
 239         */
 240 }
 241
 242 /**
 243         @Begin
 244         @Interface: Write_Unlock
 245         @Commit_point_set: Write_Unlock_Point
 246         @Check:
 247                 reader_lock_cnt == 0 && writer_lock_acquired
 248         @Action:
 249                 @Code:
 250                 __sequential.writer_lock_acquired = false;
 251         @End
 252 */
 253
 254 static inline void write_unlock(rwlock_t *rw)
 255 {
 256         atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_release);
 257         /**
 258                 @Begin
 259                 @Commit_point_define_check: true
 260                 @Label: Write_Unlock_Point
 261                 @End
 262         */
 263 }
 264
 265 rwlock_t mylock;
 266 int shareddata;
 267
 268 static void a(void *obj)
 269 {
 270         int i;
 271         for(i = 0; i < 2; i++) {
 272                 if ((i % 2) == 0) {
 273                         read_lock(&mylock);
 274                         load_32(&shareddata);
 275                         read_unlock(&mylock);
 276                 } else {
 277                         write_lock(&mylock);
 278                         store_32(&shareddata,(unsigned int)i);
 279                         write_unlock(&mylock);
 280                 }
 281         }
 282 }
 283
 284 int user_main(int argc, char **argv)
 285 {
 286         thrd_t t1, t2;
 287         atomic_init(&mylock.lock, RW_LOCK_BIAS);
 288
 289         thrd_create(&t1, (thrd_start_t)&a, NULL);
 290         thrd_create(&t2, (thrd_start_t)&a, NULL);
 291
 292         thrd_join(t1);
 293         thrd_join(t2);
 294
 295         return 0;
 296 }