results for mpmc

diff --git a/mpmc-queue/Makefile b/mpmc-queue/Makefile
index 25ff7a11203c3bb64838150b9d75e82b289b6d3a..17d7e2ad6b75c545fd552c2d17083e31a6744e06 100644 (file)
--- 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 d8711dc23fd3f526df27555f1ecaf4f6ba0e7c80..4a77db3087d74759febdd04a0629145bf610c1aa 100644 (file)
--- 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 e8597d300db8740373d1135f80812222512abf0c..f5f1490bc30bbeef66ff40f57d3ae644e49b9f2b 100644 (file)
--- 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 (file)
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 071c55d79927d4417698b944916bff02e6bdf69d..708136e4f71a23ff8cafb01a90afb9d77699f0a8 100644 (file)
--- 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<int32_t, sizeof(int32_t)> *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<int32_t, sizeof(int32_t)> *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<int32_t, sizeof(int32_t)> *queue)
 void threadC(struct mpmc_boundq_1_alt<int32_t, sizeof(int32_t)> *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 071c55d79927d4417698b944916bff02e6bdf69d..a55e8c406de93079cc13e473b9760083f3f2b53d 100644 (file)
--- 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<int32_t, sizeof(int32_t)> *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<int32_t, sizeof(int32_t)> *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<int32_t, sizeof(int32_t)> *queue)
 void threadC(struct mpmc_boundq_1_alt<int32_t, sizeof(int32_t)> *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();