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