From d6d7be6d248751fe7a8b751ecc73fa51aca0e4d6 Mon Sep 17 00:00:00 2001 From: Peizhao Ou Date: Fri, 13 Feb 2015 12:45:28 -0800 Subject: [PATCH] changes to linuxrwlock; --- linuxrwlocks/Makefile | 2 +- linuxrwlocks/note.txt | 8 ++++++ linuxrwlocks/result1.txt | 13 +++++++++ linuxrwlocks/result2.txt | 17 +++++++++++ linuxrwlocks/results.txt | 16 +++++++++++ linuxrwlocks/testcase1.c | 8 +++--- linuxrwlocks/testcase2.c | 54 +++++++++++++++++++++++++++++++++++ linuxrwlocks/testcase_full.c | 55 ++++++++++++++++++++++++++++++++++++ 8 files changed, 168 insertions(+), 5 deletions(-) create mode 100644 linuxrwlocks/note.txt create mode 100644 linuxrwlocks/result1.txt create mode 100644 linuxrwlocks/result2.txt create mode 100644 linuxrwlocks/results.txt create mode 100644 linuxrwlocks/testcase2.c create mode 100644 linuxrwlocks/testcase_full.c diff --git a/linuxrwlocks/Makefile b/linuxrwlocks/Makefile index 2940b58..8a43635 100644 --- a/linuxrwlocks/Makefile +++ b/linuxrwlocks/Makefile @@ -1,7 +1,7 @@ include ../benchmarks.mk TESTNAME = linuxrwlocks -WILDCARD_TESTS = testcase1 +WILDCARD_TESTS = testcase1 testcase2 testcase_full all: $(TESTNAME) $(WILDCARD_TESTS) $(TESTNAME): $(TESTNAME).c $(TESTNAME).h diff --git a/linuxrwlocks/note.txt b/linuxrwlocks/note.txt new file mode 100644 index 0000000..8f5a8af --- /dev/null +++ b/linuxrwlocks/note.txt @@ -0,0 +1,8 @@ +We can run the testcase_full (a testcase that contains all the method calls of +the data structure) to infer all the parameters in one file, but that takes a +long time that is mainly spent on the model-checking for unknown wrong +inferences. To make things faster, we could split the big testcase into small +cases (plus corner cases) and then run each of them one after another. + +We ran testcase1 and then got inference result1.txt, then we ran testcase2 based +on result1.txt, and we got result2.txt, which is the correct inference. diff --git a/linuxrwlocks/result1.txt b/linuxrwlocks/result1.txt new file mode 100644 index 0000000..a62c7e3 --- /dev/null +++ b/linuxrwlocks/result1.txt @@ -0,0 +1,13 @@ +Result 0: +wildcard 3 -> memory_order_acquire +wildcard 4 -> memory_order_relaxed +wildcard 5 -> memory_order_relaxed +wildcard 6 -> memory_order_acquire +wildcard 7 -> memory_order_acquire +wildcard 8 -> memory_order_relaxed +wildcard 9 -> memory_order_relaxed +wildcard 10 -> memory_order_acquire +wildcard 13 -> memory_order_relaxed +wildcard 14 -> memory_order_relaxed +wildcard 15 -> memory_order_release +wildcard 16 -> memory_order_release diff --git a/linuxrwlocks/result2.txt b/linuxrwlocks/result2.txt new file mode 100644 index 0000000..fcaca92 --- /dev/null +++ b/linuxrwlocks/result2.txt @@ -0,0 +1,17 @@ +Result 0: +wildcard 1 -> memory_order_relaxed +wildcard 2 -> memory_order_relaxed +wildcard 3 -> memory_order_acquire +wildcard 4 -> memory_order_relaxed +wildcard 5 -> memory_order_relaxed +wildcard 6 -> memory_order_acquire +wildcard 7 -> memory_order_acquire +wildcard 8 -> memory_order_relaxed +wildcard 9 -> memory_order_relaxed +wildcard 10 -> memory_order_acquire +wildcard 11 -> memory_order_acquire +wildcard 12 -> memory_order_relaxed +wildcard 13 -> memory_order_acquire +wildcard 14 -> memory_order_relaxed +wildcard 15 -> memory_order_release +wildcard 16 -> memory_order_release diff --git a/linuxrwlocks/results.txt b/linuxrwlocks/results.txt new file mode 100644 index 0000000..9564a40 --- /dev/null +++ b/linuxrwlocks/results.txt @@ -0,0 +1,16 @@ +Result 1: +wildcard 1 -> memory_order_relaxed +wildcard 3 -> memory_order_acquire +wildcard 4 -> memory_order_relaxed +wildcard 5 -> memory_order_relaxed +wildcard 6 -> memory_order_acquire +wildcard 7 -> memory_order_acquire +wildcard 8 -> memory_order_relaxed +wildcard 9 -> memory_order_relaxed +wildcard 10 -> memory_order_acquire +wildcard 11 -> memory_order_acquire +wildcard 12 -> memory_order_relaxed +wildcard 13 -> memory_order_relaxed +wildcard 14 -> memory_order_relaxed +wildcard 15 -> memory_order_release +wildcard 16 -> memory_order_release diff --git a/linuxrwlocks/testcase1.c b/linuxrwlocks/testcase1.c index 0becb24..2118561 100644 --- a/linuxrwlocks/testcase1.c +++ b/linuxrwlocks/testcase1.c @@ -31,10 +31,10 @@ static void a(void *obj) static void b(void *obj) { - - write_lock(&mylock); - atomic_store_explicit(&x, 16, relaxed); - write_unlock(&mylock); + if (write_trylock(&mylock)) { + atomic_store_explicit(&x, 16, relaxed); + write_unlock(&mylock); + } read_lock(&mylock); atomic_load_explicit(&x, relaxed); diff --git a/linuxrwlocks/testcase2.c b/linuxrwlocks/testcase2.c new file mode 100644 index 0000000..b49031e --- /dev/null +++ b/linuxrwlocks/testcase2.c @@ -0,0 +1,54 @@ +#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) +{ + if (!write_can_lock(&mylock)) + return; + + if (write_trylock(&mylock)) { + atomic_store_explicit(&x, 17, relaxed); + write_unlock(&mylock); + } +} + +static void b(void *obj) +{ + 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; +} diff --git a/linuxrwlocks/testcase_full.c b/linuxrwlocks/testcase_full.c new file mode 100644 index 0000000..295963b --- /dev/null +++ b/linuxrwlocks/testcase_full.c @@ -0,0 +1,55 @@ +#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 (!read_can_lock(&mylock)) + return; + if (read_trylock(&mylock)) { + atomic_load_explicit(&x, relaxed); + read_unlock(&mylock); + } +} + +static void b(void *obj) +{ + + if (write_trylock(&mylock)) { + atomic_store_explicit(&x, 16, relaxed); + write_unlock(&mylock); + } + + read_lock(&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