X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=linuxrwlocks%2Flinuxrwlocks.c;h=4fa29a1aecf12c46b41c1032bffcbbcaca4d190d;hb=refs%2Fheads%2Fppopp17-artifact;hp=7e317aa9fcf019b91336823985d5054c9b23166d;hpb=959cbe93cdc3c0f7a3e8340c86f53db488e25aa1;p=model-checker-benchmarks.git diff --git a/linuxrwlocks/linuxrwlocks.c b/linuxrwlocks/linuxrwlocks.c index 7e317aa..4fa29a1 100644 --- a/linuxrwlocks/linuxrwlocks.c +++ b/linuxrwlocks/linuxrwlocks.c @@ -3,110 +3,155 @@ #include #include "librace.h" - -#define RW_LOCK_BIAS 0x00100000 -#define WRITE_LOCK_CMP RW_LOCK_BIAS +#include "linuxrwlocks.h" /** Example implementation of linux rw lock along with 2 thread test * driver... */ -typedef union { - atomic_int lock; -} rwlock_t; - -static inline int read_can_lock(rwlock_t *lock) +/** + Properties to check: + 1. At most 1 thread can acquire the write lock, and at the same time, no + other threads can acquire any lock (including read/write lock). + 2. At most RW_LOCK_BIAS threads can successfully acquire the read lock. + 3. A read_unlock release 1 read lock, and a write_unlock release the write + lock. They can not release a lock that they don't acquire. + ### + 4. Read_lock and write_lock can not be grabbed at the same time. + 5. Happpens-before relationship should be checked and guaranteed, which + should be as the following: + a. read_unlock hb-> write_lock + b. write_unlock hb-> write_lock + c. write_unlock hb-> read_lock +*/ + +/** + Interesting point for locks: + a. If the users unlock() before any lock(), then the model checker will fail. + For this case, we can not say that the data structure is buggy, how can we + tell them from a real data structure bug??? + b. We should specify that for a specific thread, successful locks and + unlocks should always come in pairs. We could make this check as an + auxiliary check since it is an extra rule for how the interfaces should called. +*/ + +/** @DeclareState: bool writerLockAcquired; + int readerLockCnt; */ + +int read_can_lock(rwlock_t *lock) { return atomic_load_explicit(&lock->lock, memory_order_relaxed) > 0; } -static inline int write_can_lock(rwlock_t *lock) +int write_can_lock(rwlock_t *lock) { return atomic_load_explicit(&lock->lock, memory_order_relaxed) == RW_LOCK_BIAS; } -static inline void read_lock(rwlock_t *rw) + +/** @PreCondition: return !STATE(writerLockAcquired); +@Transition: STATE(readerLockCnt)++; */ +void read_lock(rwlock_t *rw) { + + // XXX-injection-#1: Weaken the parameter "memory_order_acquire" to + // "memory_order_relaxed", run "make" to recompile, and then run: + // "./run.sh ./linuxrwlocks/testcase1 -m2 -y -u3 -tSPEC" + /********** Detected Correctness (testcase1) **********/ int priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire); + /** @OPDefine: priorvalue > 0 */ while (priorvalue <= 0) { atomic_fetch_add_explicit(&rw->lock, 1, memory_order_relaxed); - do { - priorvalue = atomic_load_explicit(&rw->lock, memory_order_relaxed); - } while (priorvalue <= 0); + while (atomic_load_explicit(&rw->lock, memory_order_relaxed) <= 0) { + thrd_yield(); + } + // XXX-injection-#2: Weaken the parameter "memory_order_acquire" to + // "memory_order_relaxed", run "make" to recompile, and then run: + // "./run.sh ./linuxrwlocks/testcase1 -m2 -y -u3 -tSPEC" + /********** Detected Correctness (testcase1) **********/ priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire); + /** @OPDefine: priorvalue > 0 */ } } -static inline void write_lock(rwlock_t *rw) + +/** @PreCondition: return !STATE(writerLockAcquired) && STATE(readerLockCnt) == 0; +@Transition: STATE(writerLockAcquired) = true; */ +void write_lock(rwlock_t *rw) { + // XXX-injection-#3: Weaken the parameter "memory_order_acquire" to + // "memory_order_relaxed", run "make" to recompile, and then run: + // "./run.sh ./linuxrwlocks/testcase1 -m2 -y -u3 -tSPEC" + /********** Detected Correctness (testcase1) **********/ int priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire); + /** @OPDefine: priorvalue == RW_LOCK_BIAS */ while (priorvalue != RW_LOCK_BIAS) { atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_relaxed); - do { - priorvalue = atomic_load_explicit(&rw->lock, memory_order_relaxed); - } while (priorvalue != RW_LOCK_BIAS); + while (atomic_load_explicit(&rw->lock, memory_order_relaxed) != RW_LOCK_BIAS) { + thrd_yield(); + } + // XXX-injection-#4: Weaken the parameter "memory_order_acquire" to + // "memory_order_relaxed", run "make" to recompile, and then run: + // "./run.sh ./linuxrwlocks/testcase1 -m2 -y -u3 -tSPEC" + /********** Detected Correctness (testcase1) **********/ priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire); + /** @OPDefine: priorvalue == RW_LOCK_BIAS */ } } -static inline int read_trylock(rwlock_t *rw) +/** @PreCondition: return !C_RET || !STATE(writerLockAcquired); +@Transition: if (C_RET) STATE(readerLockCnt)++; */ +int read_trylock(rwlock_t *rw) { + // XXX-injection-#5: Weaken the parameter "memory_order_acquire" to + // "memory_order_relaxed", run "make" to recompile, and then run: + // "./run.sh ./linuxrwlocks/testcase2 -m2 -y -u3 -tSPEC" + /********** Detected Correctness (testcase2) **********/ int priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire); - if (priorvalue > 0) + /** @OPDefine: true */ + if (priorvalue > 0) { return 1; - + } atomic_fetch_add_explicit(&rw->lock, 1, memory_order_relaxed); return 0; } -static inline int write_trylock(rwlock_t *rw) +/** @PreCondition: return !C_RET || !STATE(writerLockAcquired) && STATE(readerLockCnt) == 0; +@Transition: if (C_RET) STATE(writerLockAcquired) = true; */ +int write_trylock(rwlock_t *rw) { + // XXX-injection-#6: Weaken the parameter "memory_order_acquire" to + // "memory_order_relaxed", run "make" to recompile, and then run: + // "./run.sh ./linuxrwlocks/testcase2 -m2 -y -u3 -tSPEC" + /********** Detected Correctness (testcase2) **********/ int priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire); - if (priorvalue == RW_LOCK_BIAS) + /** @OPDefine: true */ + if (priorvalue == RW_LOCK_BIAS) { return 1; - + } atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_relaxed); return 0; } -static inline void read_unlock(rwlock_t *rw) +/** @PreCondition: return STATE(readerLockCnt) > 0 && !STATE(writerLockAcquired); +@Transition: STATE(readerLockCnt)--; */ +void read_unlock(rwlock_t *rw) { + // XXX-injection-#7: Weaken the parameter "memory_order_release" to + // "memory_order_relaxed", run "make" to recompile, and then run: + // "./run.sh ./linuxrwlocks/testcase1 -m2 -y -u3 -tSPEC" + /********** Detected Correctness (testcase1) **********/ atomic_fetch_add_explicit(&rw->lock, 1, memory_order_release); + /** @OPDefine: true */ } -static inline void write_unlock(rwlock_t *rw) +/** @PreCondition: return STATE(readerLockCnt) == 0 && STATE(writerLockAcquired); +@Transition: STATE(writerLockAcquired) = false; */ +void write_unlock(rwlock_t *rw) { + // XXX-injection-#8: Weaken the parameter "memory_order_release" to + // "memory_order_relaxed", run "make" to recompile, and then run: + // "./run.sh ./linuxrwlocks/testcase1 -m2 -y -u3 -tSPEC" + /********** Detected Correctness (testcase1) **********/ atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_release); -} - -rwlock_t mylock; -int shareddata; - -static void a(void *obj) -{ - int i; - for(i = 0; i < 2; i++) { - if ((i % 2) == 0) { - read_lock(&mylock); - load_32(&shareddata); - read_unlock(&mylock); - } else { - write_lock(&mylock); - store_32(&shareddata,(unsigned int)i); - write_unlock(&mylock); - } - } -} - -int user_main(int argc, char **argv) -{ - thrd_t t1, t2; - atomic_init(&mylock.lock, RW_LOCK_BIAS); - - thrd_create(&t1, (thrd_start_t)&a, NULL); - thrd_create(&t2, (thrd_start_t)&a, NULL); - - thrd_join(t1); - thrd_join(t2); - - return 0; + /** @OPDefine: true */ }