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         /**********  Detected Correctness (testcase1) **********/
  57         int priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
  58         /** @OPDefine: priorvalue > 0 */
  59         while (priorvalue <= 0) {
  60                 atomic_fetch_add_explicit(&rw->lock, 1, memory_order_relaxed);
  61                 while (atomic_load_explicit(&rw->lock, memory_order_relaxed) <= 0) {
  62                         thrd_yield();
  63                 }
  64             /**********  Detected Correctness (testcase1) **********/
  65                 priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
  66                 /** @OPDefine: priorvalue > 0 */
  67         }
  68 }
  69
  70
  71 /** @PreCondition: return !STATE(writerLockAcquired) && STATE(readerLockCnt) == 0;
  72 @Transition: STATE(writerLockAcquired) = true; */
  73 void write_lock(rwlock_t *rw)
  74 {
  75         /**********  Detected Correctness (testcase1) **********/
  76         int priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
  77         /** @OPDefine: priorvalue == RW_LOCK_BIAS */
  78         while (priorvalue != RW_LOCK_BIAS) {
  79                 atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_relaxed);
  80                 while (atomic_load_explicit(&rw->lock, memory_order_relaxed) != RW_LOCK_BIAS) {
  81                         thrd_yield();
  82                 }
  83             /**********  Detected Correctness (testcase1) **********/
  84                 priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
  85                 /** @OPDefine: priorvalue == RW_LOCK_BIAS */
  86         }
  87 }
  88
  89 /** @PreCondition: return !C_RET || !STATE(writerLockAcquired);
  90 @Transition: if (C_RET) STATE(readerLockCnt)++; */
  91 int read_trylock(rwlock_t *rw)
  92 {
  93         /**********  Detected Correctness (testcase2) **********/
  94         int priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
  95         /** @OPDefine: true */
  96         if (priorvalue > 0) {
  97                 return 1;
  98         }
  99         atomic_fetch_add_explicit(&rw->lock, 1, memory_order_relaxed);
 100         return 0;
 101 }
 102
 103 /** @PreCondition: return !C_RET || !STATE(writerLockAcquired) && STATE(readerLockCnt) == 0;
 104 @Transition: if (C_RET) STATE(writerLockAcquired) = true; */
 105 int write_trylock(rwlock_t *rw)
 106 {
 107         /**********  Detected Correctness (testcase2) **********/
 108         int priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
 109         /** @OPDefine: true */
 110         if (priorvalue == RW_LOCK_BIAS) {
 111                 return 1;
 112         }
 113         atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_relaxed);
 114         return 0;
 115 }
 116
 117 /** @PreCondition: return STATE(readerLockCnt) > 0 && !STATE(writerLockAcquired);
 118 @Transition: STATE(readerLockCnt)--; */
 119 void read_unlock(rwlock_t *rw)
 120 {
 121         /**********  Detected Correctness (testcase1) **********/
 122         atomic_fetch_add_explicit(&rw->lock, 1, memory_order_release);
 123         /** @OPDefine: true */
 124 }
 125
 126 /** @PreCondition: return STATE(readerLockCnt) == 0 && STATE(writerLockAcquired);
 127 @Transition: STATE(writerLockAcquired) = false; */
 128 void write_unlock(rwlock_t *rw)
 129 {
 130         /**********  Detected Correctness (testcase1) **********/
 131         atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_release);
 132         /** @OPDefine: true */
 133 }