From e6766cda044641ae6ddab5eb08c3e9ab44564066 Mon Sep 17 00:00:00 2001 From: Peizhao Ou Date: Wed, 11 Feb 2015 22:54:45 -0800 Subject: [PATCH] changes --- linuxrwlocks/Makefile | 9 +- linuxrwlocks/linuxrwlocks-wildcard.h | 276 +++++++++++++++++++++++++++ linuxrwlocks/linuxrwlocks.c | 75 +------- linuxrwlocks/linuxrwlocks.h | 78 ++++++++ linuxrwlocks/testcase1.c | 72 +++++++ 5 files changed, 433 insertions(+), 77 deletions(-) create mode 100644 linuxrwlocks/linuxrwlocks-wildcard.h create mode 100644 linuxrwlocks/linuxrwlocks.h create mode 100644 linuxrwlocks/testcase1.c diff --git a/linuxrwlocks/Makefile b/linuxrwlocks/Makefile index 90dafcf..2940b58 100644 --- a/linuxrwlocks/Makefile +++ b/linuxrwlocks/Makefile @@ -1,11 +1,14 @@ include ../benchmarks.mk TESTNAME = linuxrwlocks +WILDCARD_TESTS = testcase1 +all: $(TESTNAME) $(WILDCARD_TESTS) -all: $(TESTNAME) +$(TESTNAME): $(TESTNAME).c $(TESTNAME).h + $(CC) -o $@ $< $(CFLAGS) $(LDFLAGS) -$(TESTNAME): $(TESTNAME).c +$(WILDCARD_TESTS): % : %.c $(TESTNAME)-wildcard.h $(CC) -o $@ $< $(CFLAGS) $(LDFLAGS) clean: - rm -f $(TESTNAME) *.o + rm -f $(TESTNAME) *.o $(WILDCARD_TESTS) diff --git a/linuxrwlocks/linuxrwlocks-wildcard.h b/linuxrwlocks/linuxrwlocks-wildcard.h new file mode 100644 index 0000000..1a75594 --- /dev/null +++ b/linuxrwlocks/linuxrwlocks-wildcard.h @@ -0,0 +1,276 @@ +#include +#include +#include +#include "wildcard.h" + +#include "librace.h" + +#define RW_LOCK_BIAS 0x00100000 +#define WRITE_LOCK_CMP RW_LOCK_BIAS + +/** Example implementation of linux rw lock along with 2 thread test + * driver... */ + +/** + 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. +*/ + +/** + @Begin + @Global_define: + bool __writer_lock_acquired = false; + int __reader_lock_cnt = 0; + + @Happens_before: + # Since commit_point_set has no ID attached, A -> B means that for any B, + # the previous A happens before B. + Read_Unlock -> Write_Lock + Read_Unlock -> Write_Trylock(HB_Write_Trylock_Succ) + + Write_Unlock -> Write_Lock + Write_Unlock -> Write_Trylock(HB_Write_Trylock_Succ) + + Write_Unlock -> Read_Lock + Write_Unlock -> Read_Trylock(HB_Read_Trylock_Succ) + @End +*/ + +/** + */ + +typedef union { + atomic_int lock; +} rwlock_t; + +static inline int read_can_lock(rwlock_t *lock) +{ + // relaxed + return atomic_load_explicit(&lock->lock, wildcard(1)) > 0; +} + +static inline int write_can_lock(rwlock_t *lock) +{ + // relaxed + return atomic_load_explicit(&lock->lock, wildcard(2)) == RW_LOCK_BIAS; +} + + +/** + @Begin + @Interface: Read_Lock + @Commit_point_set: + Read_Lock_Success_1 | Read_Lock_Success_2 + @Check: + !__writer_lock_acquired + @Action: + @Code: + __reader_lock_cnt++; + @End +*/ +static inline void read_lock(rwlock_t *rw) +{ + // acquire + int priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, wildcard(3)); + /** + @Begin + @Commit_point_define_check: __ATOMIC_RET__ > 0 + @Label:Read_Lock_Success_1 + @End + */ + while (priorvalue <= 0) { + // relaxed + atomic_fetch_add_explicit(&rw->lock, 1, wildcard(4)); + // relaxed + while (atomic_load_explicit(&rw->lock, wildcard(5)) <= 0) { + thrd_yield(); + } + // acquire + priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, wildcard(6)); + /** + @Begin + @Commit_point_define_check: __ATOMIC_RET__ > 0 + @Label:Read_Lock_Success_2 + @End + */ + } +} + + +/** + @Begin + @Interface: Write_Lock + @Commit_point_set: + Write_Lock_Success_1 | Write_Lock_Success_2 + @Check: + !__writer_lock_acquired && __reader_lock_cnt == 0 + @Action: + @Code: + __writer_lock_acquired = true; + @End +*/ +static inline void write_lock(rwlock_t *rw) +{ + // acquire + int priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, wildcard(7)); + /** + @Begin + @Commit_point_define_check: __ATOMIC_RET__ == RW_LOCK_BIAS + @Label: Write_Lock_Success_1 + @End + */ + while (priorvalue != RW_LOCK_BIAS) { + // relaxed + atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, wildcard(8)); + // relaxed + while (atomic_load_explicit(&rw->lock, wildcard(9)) != RW_LOCK_BIAS) { + thrd_yield(); + } + // acquire + priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, wildcard(10)); + /** + @Begin + @Commit_point_define_check: __ATOMIC_RET__ == RW_LOCK_BIAS + @Label: Write_Lock_Success_2 + @End + */ + } +} + +/** + @Begin + @Interface: Read_Trylock + @Commit_point_set: + Read_Trylock_Point + @Condition: + __writer_lock_acquired == false + @HB_condition: + HB_Read_Trylock_Succ :: __RET__ == 1 + @Action: + @Code: + if (COND_SAT) + __reader_lock_cnt++; + @Post_check: + COND_SAT ? __RET__ == 1 : __RET__ == 0 + @End +*/ +static inline int read_trylock(rwlock_t *rw) +{ + // acquire + int priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, wildcard(11)); + /** + @Begin + @Commit_point_define_check: true + @Label:Read_Trylock_Point + @End + */ + if (priorvalue > 0) + return 1; + + // relaxed + atomic_fetch_add_explicit(&rw->lock, 1, wildcard(12)); + return 0; +} + +/** + @Begin + @Interface: Write_Trylock + @Commit_point_set: + Write_Trylock_Point + @Condition: + !__writer_lock_acquired && __reader_lock_cnt == 0 + @HB_condition: + HB_Write_Trylock_Succ :: __RET__ == 1 + @Action: + @Code: + if (COND_SAT) + __writer_lock_acquired = true; + @Post_check: + COND_SAT ? __RET__ == 1 : __RET__ == 0 + @End +*/ +static inline int write_trylock(rwlock_t *rw) +{ + // acquire + int priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, wildcard(13)); + /** + @Begin + @Commit_point_define_check: true + @Label: Write_Trylock_Point + @End + */ + if (priorvalue == RW_LOCK_BIAS) + return 1; + + // relaxed + atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, wildcard(14)); + return 0; +} + +/** + @Begin + @Interface: Read_Unlock + @Commit_point_set: Read_Unlock_Point + @Check: + __reader_lock_cnt > 0 && !__writer_lock_acquired + @Action: + @Code: + reader_lock_cnt--; + @End +*/ +static inline void read_unlock(rwlock_t *rw) +{ + // release + atomic_fetch_add_explicit(&rw->lock, 1, wildcard(15)); + /** + @Begin + @Commit_point_define_check: true + @Label: Read_Unlock_Point + @End + */ +} + +/** + @Begin + @Interface: Write_Unlock + @Commit_point_set: Write_Unlock_Point + @Check: + reader_lock_cnt == 0 && writer_lock_acquired + @Action: + @Code: + __writer_lock_acquired = false; + @End +*/ + +static inline void write_unlock(rwlock_t *rw) +{ + // release + atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, wildcard(16)); + /** + @Begin + @Commit_point_define_check: true + @Label: Write_Unlock_Point + @End + */ +} diff --git a/linuxrwlocks/linuxrwlocks.c b/linuxrwlocks/linuxrwlocks.c index be3550e..bf60f16 100644 --- a/linuxrwlocks/linuxrwlocks.c +++ b/linuxrwlocks/linuxrwlocks.c @@ -3,80 +3,7 @@ #include #include "librace.h" - -#define RW_LOCK_BIAS 0x00100000 -#define WRITE_LOCK_CMP RW_LOCK_BIAS - -/** 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) -{ - return atomic_load_explicit(&lock->lock, memory_order_relaxed) > 0; -} - -static inline 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) -{ - int priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire); - while (priorvalue <= 0) { - atomic_fetch_add_explicit(&rw->lock, 1, memory_order_relaxed); - while (atomic_load_explicit(&rw->lock, memory_order_relaxed) <= 0) { - thrd_yield(); - } - priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire); - } -} - -static inline void write_lock(rwlock_t *rw) -{ - int priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire); - while (priorvalue != RW_LOCK_BIAS) { - atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_relaxed); - while (atomic_load_explicit(&rw->lock, memory_order_relaxed) != RW_LOCK_BIAS) { - thrd_yield(); - } - priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire); - } -} - -static inline int read_trylock(rwlock_t *rw) -{ - int priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire); - 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) -{ - int priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire); - 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) -{ - atomic_fetch_add_explicit(&rw->lock, 1, memory_order_release); -} - -static inline void write_unlock(rwlock_t *rw) -{ - atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_release); -} +#include "linuxrwlocks.h" rwlock_t mylock; int shareddata; diff --git a/linuxrwlocks/linuxrwlocks.h b/linuxrwlocks/linuxrwlocks.h new file mode 100644 index 0000000..1e300ab --- /dev/null +++ b/linuxrwlocks/linuxrwlocks.h @@ -0,0 +1,78 @@ +#include +#include + +#include "librace.h" + +#define RW_LOCK_BIAS 0x00100000 +#define WRITE_LOCK_CMP RW_LOCK_BIAS + +/** 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) +{ + return atomic_load_explicit(&lock->lock, memory_order_relaxed) > 0; +} + +static inline 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) +{ + int priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire); + while (priorvalue <= 0) { + atomic_fetch_add_explicit(&rw->lock, 1, memory_order_relaxed); + while (atomic_load_explicit(&rw->lock, memory_order_relaxed) <= 0) { + thrd_yield(); + } + priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire); + } +} + +static inline void write_lock(rwlock_t *rw) +{ + int priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire); + while (priorvalue != RW_LOCK_BIAS) { + atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_relaxed); + while (atomic_load_explicit(&rw->lock, memory_order_relaxed) != RW_LOCK_BIAS) { + thrd_yield(); + } + priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire); + } +} + +static inline int read_trylock(rwlock_t *rw) +{ + int priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire); + 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) +{ + int priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire); + 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) +{ + atomic_fetch_add_explicit(&rw->lock, 1, memory_order_release); +} + +static inline void write_unlock(rwlock_t *rw) +{ + atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_release); +} diff --git a/linuxrwlocks/testcase1.c b/linuxrwlocks/testcase1.c new file mode 100644 index 0000000..0becb24 --- /dev/null +++ b/linuxrwlocks/testcase1.c @@ -0,0 +1,72 @@ +#include +#include +#include +#include "wildcard.h" + +#include "librace.h" +#include "linuxrwlocks-wildcard.h" + +rwlock_t mylock; +int shareddata; + +atomic_int x, y; + +static void a(void *obj) +{ + write_lock(&mylock); + atomic_store_explicit(&x, 17, relaxed); + write_unlock(&mylock); + +/* + + if (!write_can_lock(&mylock)) + return; + + if (write_trylock(&mylock)) { + atomic_store_explicit(&x, 17, relaxed); + write_unlock(&mylock); + } +*/ +} + +static void b(void *obj) +{ + + write_lock(&mylock); + atomic_store_explicit(&x, 16, relaxed); + write_unlock(&mylock); + + read_lock(&mylock); + atomic_load_explicit(&x, relaxed); + read_unlock(&mylock); + +/* + if (write_trylock(&mylock)) { + atomic_store_explicit(&x, 16, relaxed); + write_unlock(&mylock); + } + + if (!read_can_lock(&mylock)) + return; + if (read_trylock(&mylock)) { + atomic_load_explicit(&x, relaxed); + read_unlock(&mylock); + } +*/ +} + +int user_main(int argc, char **argv) +{ + thrd_t t1, t2; + atomic_init(&mylock.lock, RW_LOCK_BIAS); + atomic_init(&x, 0); + atomic_init(&y, 0); + + thrd_create(&t1, (thrd_start_t)&a, NULL); + thrd_create(&t2, (thrd_start_t)&b, NULL); + + thrd_join(t1); + thrd_join(t2); + + return 0; +} -- 2.34.1