From 2e8cf83a7015535e33eb8ccf14586ea59fa9776a Mon Sep 17 00:00:00 2001 From: Peizhao Ou Date: Sun, 22 Mar 2015 11:31:25 -0700 Subject: [PATCH] results for mpmc --- mpmc-queue/Makefile | 3 +++ mpmc-queue/mpmc-queue-wildcard.h | 6 +++--- mpmc-queue/note.txt | 13 +++++++++++++ mpmc-queue/result1.txt | 17 +++++++++++++++++ mpmc-queue/testcase1.cc | 18 ++++++++++++------ mpmc-queue/testcase2.cc | 20 ++++++++++++++------ 6 files changed, 62 insertions(+), 15 deletions(-) create mode 100644 mpmc-queue/result1.txt diff --git a/mpmc-queue/Makefile b/mpmc-queue/Makefile index 25ff7a1..17d7e2a 100644 --- a/mpmc-queue/Makefile +++ b/mpmc-queue/Makefile @@ -17,6 +17,9 @@ mpmc-1r2w-noinit: CPPFLAGS += -DCONFIG_MPMC_READERS=1 -DCONFIG_MPMC_WRITERS=2 -D mpmc-2r1w-noinit: CPPFLAGS += -DCONFIG_MPMC_READERS=2 -DCONFIG_MPMC_WRITERS=1 -DCONFIG_MPMC_NO_INITIAL_ELEMENT mpmc-rdwr-noinit: CPPFLAGS += -DCONFIG_MPMC_READERS=0 -DCONFIG_MPMC_WRITERS=0 -DCONFIG_MPMC_RDWR=2 -DCONFIG_MPMC_NO_INITIAL_ELEMENT +testcase1: CPPFLAGS += -DCONFIG_MPMC_READERS=1 -DCONFIG_MPMC_WRITERS=2 -DCONFIG_MPMC_RDWR=0 -DCONFIG_MPMC_NO_INITIAL_ELEMENT +testcase2: CPPFLAGS += -DCONFIG_MPMC_READERS=0 -DCONFIG_MPMC_WRITERS=0 -DCONFIG_MPMC_RDWR=1 -DCONFIG_MPMC_NO_INITIAL_ELEMENT + $(TESTS): $(TESTNAME).cc $(TESTNAME).h $(CXX) -o $@ $< $(CXXFLAGS) $(LDFLAGS) diff --git a/mpmc-queue/mpmc-queue-wildcard.h b/mpmc-queue/mpmc-queue-wildcard.h index d8711dc..4a77db3 100644 --- a/mpmc-queue/mpmc-queue-wildcard.h +++ b/mpmc-queue/mpmc-queue-wildcard.h @@ -34,14 +34,14 @@ public: //----------------------------------------------------- t_element * read_fetch() { - unsigned int rdwr = m_rdwr.load(wildcard(1)); // acquire + unsigned int rdwr = m_rdwr.load(wildcard(1)); // acquire, but can be relaxed unsigned int rd,wr; for(;;) { rd = (rdwr>>16) & 0xFFFF; wr = rdwr & 0xFFFF; if ( wr == rd ) { // empty - return false; + return NULL; } // acq_rel @@ -84,7 +84,7 @@ public: //----------------------------------------------------- t_element * write_prepare() { - unsigned int rdwr = m_rdwr.load(wildcard(5)); // acquire + unsigned int rdwr = m_rdwr.load(wildcard(5)); // acquire, but can be relaxed unsigned int rd,wr; for(;;) { rd = (rdwr>>16) & 0xFFFF; diff --git a/mpmc-queue/note.txt b/mpmc-queue/note.txt index e8597d3..f5f1490 100644 --- a/mpmc-queue/note.txt +++ b/mpmc-queue/note.txt @@ -18,3 +18,16 @@ m_written.load; // a m_rdwr.load; // The first in the read_fetch() // b a & b can both read old value and it's non-SC. However, the later loads and CAS in the loops will finally fix this problem. + + + +Run testcase1 with -Y, we got w3 & w7 to be acquire, and w4 & w8 release. Then +if we run testcase1 with -Y on its "-y" result, we will make other parameters +seq_cst. + +However, we might have a bug in the model-checker when we ran with -y, +explanation as follows: + +After we strengthen w1 & w6 to be sc, w1 can still read a value from a store +that is modification ordered before w6 (w6 is SC before w1). We should deal with +this after the OOPSLA deadline. diff --git a/mpmc-queue/result1.txt b/mpmc-queue/result1.txt new file mode 100644 index 0000000..07a4013 --- /dev/null +++ b/mpmc-queue/result1.txt @@ -0,0 +1,17 @@ +peizhaoo@dw-2:~/test/model-checker-priv/model-checker-priv$ time ./run.sh +benchmarks/mpmc-queue/testcase1 -m2 -Y -u3 -tSCFENCE -o weaken -o +fbenchmarks/mpmc-queue/result1.txt &> /scratch/a + +real 0m0.162s +user 0m0.143s +sys 0m0.010s + +Result 0: +wildcard 1 -> memory_order_relaxed +wildcard 2 -> memory_order_relaxed +wildcard 3 -> memory_order_acquire +wildcard 4 -> memory_order_release +wildcard 5 -> memory_order_relaxed +wildcard 6 -> memory_order_relaxed +wildcard 7 -> memory_order_acquire +wildcard 8 -> memory_order_release diff --git a/mpmc-queue/testcase1.cc b/mpmc-queue/testcase1.cc index 071c55d..708136e 100644 --- a/mpmc-queue/testcase1.cc +++ b/mpmc-queue/testcase1.cc @@ -8,10 +8,13 @@ #include "mpmc-queue-wildcard.h" +atomic_int x; + void threadA(struct mpmc_boundq_1_alt *queue) { int32_t *bin = queue->write_prepare(); - store_32(bin, 1); + //store_32(bin, 1); + x.store(1, memory_order_relaxed); queue->write_publish(); } @@ -19,7 +22,8 @@ void threadB(struct mpmc_boundq_1_alt *queue) { int32_t *bin; while ((bin = queue->read_fetch()) != NULL) { - printf("Read: %d\n", load_32(bin)); + x.load(memory_order_relaxed); + //printf("Read: %d\n", load_32(bin)); queue->read_consume(); } } @@ -27,15 +31,15 @@ void threadB(struct mpmc_boundq_1_alt *queue) void threadC(struct mpmc_boundq_1_alt *queue) { int32_t *bin = queue->write_prepare(); - store_32(bin, 1); + //store_32(bin, 1); + queue->write_publish(); while ((bin = queue->read_fetch()) != NULL) { - printf("Read: %d\n", load_32(bin)); + //printf("Read: %d\n", load_32(bin)); queue->read_consume(); } -} - +} #define MAXREADERS 3 #define MAXWRITERS 3 #define MAXRDWR 3 @@ -110,6 +114,8 @@ int user_main(int argc, char **argv) //process_params(argc, argv); printf("%d reader(s), %d writer(s)\n", readers, writers); + + x.store(0); #ifndef CONFIG_MPMC_NO_INITIAL_ELEMENT printf("Adding initial element\n"); int32_t *bin = queue.write_prepare(); diff --git a/mpmc-queue/testcase2.cc b/mpmc-queue/testcase2.cc index 071c55d..a55e8c4 100644 --- a/mpmc-queue/testcase2.cc +++ b/mpmc-queue/testcase2.cc @@ -8,10 +8,13 @@ #include "mpmc-queue-wildcard.h" +atomic_int x; + void threadA(struct mpmc_boundq_1_alt *queue) { int32_t *bin = queue->write_prepare(); - store_32(bin, 1); + //store_32(bin, 1); + x.store(1, memory_order_relaxed); queue->write_publish(); } @@ -19,7 +22,8 @@ void threadB(struct mpmc_boundq_1_alt *queue) { int32_t *bin; while ((bin = queue->read_fetch()) != NULL) { - printf("Read: %d\n", load_32(bin)); + x.load(memory_order_relaxed); + //printf("Read: %d\n", load_32(bin)); queue->read_consume(); } } @@ -27,15 +31,17 @@ void threadB(struct mpmc_boundq_1_alt *queue) void threadC(struct mpmc_boundq_1_alt *queue) { int32_t *bin = queue->write_prepare(); - store_32(bin, 1); + //store_32(bin, 1); + x.store(1, memory_order_relaxed); + queue->write_publish(); while ((bin = queue->read_fetch()) != NULL) { - printf("Read: %d\n", load_32(bin)); + x.load(memory_order_relaxed); + //printf("Read: %d\n", load_32(bin)); queue->read_consume(); } -} - +} #define MAXREADERS 3 #define MAXWRITERS 3 #define MAXRDWR 3 @@ -110,6 +116,8 @@ int user_main(int argc, char **argv) //process_params(argc, argv); printf("%d reader(s), %d writer(s)\n", readers, writers); + + x.store(0); #ifndef CONFIG_MPMC_NO_INITIAL_ELEMENT printf("Adding initial element\n"); int32_t *bin = queue.write_prepare(); -- 2.34.1