linuxrwlocks/linuxrwlocks.c

   1 #include <stdio.h>
   2 #include <threads.h>
   3 #include <stdatomic.h>
   4
   5 #include "librace.h"
   6 #include "linuxrwlocks.h"
   7
   8 /** Example implementation of linux rw lock along with 2 thread test
   9  *  driver... */
  10
  11 /**
  12         Properties to check:
  13         1. At most 1 thread can acquire the write lock, and at the same time, no
  14                 other threads can acquire any lock (including read/write lock).
  15         2. At most RW_LOCK_BIAS threads can successfully acquire the read lock.
  16         3. A read_unlock release 1 read lock, and a write_unlock release the write
  17         lock. They can not release a lock that they don't acquire.
  18         ###
  19         4. Read_lock and write_lock can not be grabbed at the same time.
  20         5. Happpens-before relationship should be checked and guaranteed, which
  21         should be as the following:
  22                 a. read_unlock hb-> write_lock
  23                 b. write_unlock hb-> write_lock
  24                 c. write_unlock hb-> read_lock
  25 */
  26
  27 /**
  28         Interesting point for locks:
  29         a. If the users unlock() before any lock(), then the model checker will fail.
  30         For this case, we can not say that the data structure is buggy, how can we
  31         tell them from a real data structure bug???
  32         b. We should specify that for a specific thread, successful locks and
  33         unlocks should always come in pairs. We could make this check as an
  34         auxiliary check since it is an extra rule for how the interfaces should called.
  35 */
  36
  37 /** @DeclareState: bool writerLockAcquired;
  38                 int readerLockCnt; */
  39
  40 int read_can_lock(rwlock_t *lock)
  41 {
  42         return atomic_load_explicit(&lock->lock, memory_order_relaxed) > 0;
  43 }
  44
  45 int write_can_lock(rwlock_t *lock)
  46 {
  47         return atomic_load_explicit(&lock->lock, memory_order_relaxed) == RW_LOCK_BIAS;
  48 }
  49
  50
  51 /** @PreCondition: return !STATE(writerLockAcquired);
  52 @Transition: STATE(readerLockCnt)++; */
  53 void read_lock(rwlock_t *rw)
  54 {
  55
  56         // XXX-injection-#1: Weaken the parameter "memory_order_acquire" to
  57     // "memory_order_relaxed", run "make" to recompile, and then run:
  58     // "./run.sh ./linuxrwlocks/testcase1 -m2 -y -u3 -tSPEC"
  59         /**********  Detected Correctness (testcase1) **********/
  60         int priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
  61         /** @OPDefine: priorvalue > 0 */
  62         while (priorvalue <= 0) {
  63                 atomic_fetch_add_explicit(&rw->lock, 1, memory_order_relaxed);
  64                 while (atomic_load_explicit(&rw->lock, memory_order_relaxed) <= 0) {
  65                         thrd_yield();
  66                 }
  67         // XXX-injection-#2: Weaken the parameter "memory_order_acquire" to
  68         // "memory_order_relaxed", run "make" to recompile, and then run:
  69         // "./run.sh ./linuxrwlocks/testcase1 -m2 -y -u3 -tSPEC"
  70             /**********  Detected Correctness (testcase1) **********/
  71                 priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
  72                 /** @OPDefine: priorvalue > 0 */
  73         }
  74 }
  75
  76
  77 /** @PreCondition: return !STATE(writerLockAcquired) && STATE(readerLockCnt) == 0;
  78 @Transition: STATE(writerLockAcquired) = true; */
  79 void write_lock(rwlock_t *rw)
  80 {
  81     // XXX-injection-#3: Weaken the parameter "memory_order_acquire" to
  82     // "memory_order_relaxed", run "make" to recompile, and then run:
  83     // "./run.sh ./linuxrwlocks/testcase1 -m2 -y -u3 -tSPEC"
  84         /**********  Detected Correctness (testcase1) **********/
  85         int priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
  86         /** @OPDefine: priorvalue == RW_LOCK_BIAS */
  87         while (priorvalue != RW_LOCK_BIAS) {
  88                 atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_relaxed);
  89                 while (atomic_load_explicit(&rw->lock, memory_order_relaxed) != RW_LOCK_BIAS) {
  90                         thrd_yield();
  91                 }
  92         // XXX-injection-#4: Weaken the parameter "memory_order_acquire" to
  93         // "memory_order_relaxed", run "make" to recompile, and then run:
  94         // "./run.sh ./linuxrwlocks/testcase1 -m2 -y -u3 -tSPEC"
  95             /**********  Detected Correctness (testcase1) **********/
  96                 priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
  97                 /** @OPDefine: priorvalue == RW_LOCK_BIAS */
  98         }
  99 }
 100
 101 /** @PreCondition: return !C_RET || !STATE(writerLockAcquired);
 102 @Transition: if (C_RET) STATE(readerLockCnt)++; */
 103 int read_trylock(rwlock_t *rw)
 104 {
 105     // XXX-injection-#5: Weaken the parameter "memory_order_acquire" to
 106     // "memory_order_relaxed", run "make" to recompile, and then run:
 107     // "./run.sh ./linuxrwlocks/testcase2 -m2 -y -u3 -tSPEC"
 108         /**********  Detected Correctness (testcase2) **********/
 109         int priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
 110         /** @OPDefine: true */
 111         if (priorvalue > 0) {
 112                 return 1;
 113         }
 114         atomic_fetch_add_explicit(&rw->lock, 1, memory_order_relaxed);
 115         return 0;
 116 }
 117
 118 /** @PreCondition: return !C_RET || !STATE(writerLockAcquired) && STATE(readerLockCnt) == 0;
 119 @Transition: if (C_RET) STATE(writerLockAcquired) = true; */
 120 int write_trylock(rwlock_t *rw)
 121 {
 122     // XXX-injection-#6: Weaken the parameter "memory_order_acquire" to
 123     // "memory_order_relaxed", run "make" to recompile, and then run:
 124     // "./run.sh ./linuxrwlocks/testcase2 -m2 -y -u3 -tSPEC"
 125         /**********  Detected Correctness (testcase2) **********/
 126         int priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
 127         /** @OPDefine: true */
 128         if (priorvalue == RW_LOCK_BIAS) {
 129                 return 1;
 130         }
 131         atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_relaxed);
 132         return 0;
 133 }
 134
 135 /** @PreCondition: return STATE(readerLockCnt) > 0 && !STATE(writerLockAcquired);
 136 @Transition: STATE(readerLockCnt)--; */
 137 void read_unlock(rwlock_t *rw)
 138 {
 139     // XXX-injection-#7: Weaken the parameter "memory_order_release" to
 140     // "memory_order_relaxed", run "make" to recompile, and then run:
 141     // "./run.sh ./linuxrwlocks/testcase1 -m2 -y -u3 -tSPEC"
 142         /**********  Detected Correctness (testcase1) **********/
 143         atomic_fetch_add_explicit(&rw->lock, 1, memory_order_release);
 144         /** @OPDefine: true */
 145 }
 146
 147 /** @PreCondition: return STATE(readerLockCnt) == 0 && STATE(writerLockAcquired);
 148 @Transition: STATE(writerLockAcquired) = false; */
 149 void write_unlock(rwlock_t *rw)
 150 {
 151     // XXX-injection-#8: Weaken the parameter "memory_order_release" to
 152     // "memory_order_relaxed", run "make" to recompile, and then run:
 153     // "./run.sh ./linuxrwlocks/testcase1 -m2 -y -u3 -tSPEC"
 154         /**********  Detected Correctness (testcase1) **********/
 155         atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_release);
 156         /** @OPDefine: true */
 157 }