edits
[cdsspec-compiler.git] / benchmark / mpmc-queue / mpmc-queue.h
index ff6a168..046a248 100644 (file)
@@ -134,7 +134,7 @@ public:
                // (*1)
                rl::backoff bo;
                while (true) {
                // (*1)
                rl::backoff bo;
                while (true) {
-                       /**** Inadmissibility ****/
+                       /**** Inadmissibility (testcase2.c) ****/
                        int written = m_written.load(mo_acquire);
                        if ((written & MASK) != wr) {
                                thrd_yield();
                        int written = m_written.load(mo_acquire);
                        if ((written & MASK) != wr) {
                                thrd_yield();
@@ -173,7 +173,7 @@ public:
                @End
        */
        void read_consume(t_element *bin) {
                @End
        */
        void read_consume(t_element *bin) {
-               /**** Inadmissibility ****/
+               /**** Inadmissibility (testcase1.c) ****/
                m_read.fetch_add(1,mo_release);
                /**
                        @Begin
                m_read.fetch_add(1,mo_release);
                /**
                        @Begin
@@ -214,6 +214,14 @@ public:
                                return NULL;
                        }
                        
                                return NULL;
                        }
                        
+                       // FIXME: Theoretically we have a bug here, it is not so likely to
+                       // happen!!! The following acq_rel can not guarantee that the load
+                       // acquire on m_read to read the most recent value. However, it can
+                       // decrease the chance of the load acquire of m_read to read a too
+                       // old value. Same as the case in read_fetch(). Maybe making things
+                       // SC can fix it. We can run testcase3.c to expose this bug (set the
+                       // array size  = 1, the MASK = 1).
+                       
                        /**** Inadmissibility (testcase3.cc, MASK = 1, size = 1) ****/
                        bool succ = m_rdwr.compare_exchange_weak(rdwr,(rd<<16) |
                                ((wr+1)&MASK),mo_acq_rel);
                        /**** Inadmissibility (testcase3.cc, MASK = 1, size = 1) ****/
                        bool succ = m_rdwr.compare_exchange_weak(rdwr,(rd<<16) |
                                ((wr+1)&MASK),mo_acq_rel);
@@ -241,7 +249,7 @@ public:
                // (*1)
                rl::backoff bo;
                while (true) {
                // (*1)
                rl::backoff bo;
                while (true) {
-                       /**** Inadmissibility ****/
+                       /**** Inadmissibility (testcase1.c) ****/
                        int read = m_read.load(mo_acquire);
                        if ((read & MASK) != rd)
                                thrd_yield();
                        int read = m_read.load(mo_acquire);
                        if ((read & MASK) != rd)
                                thrd_yield();
@@ -273,19 +281,19 @@ public:
        /**
                @Begin
                @Interface: Publish 
        /**
                @Begin
                @Interface: Publish 
-               @Commit_point_set: Publish_W_RMW
+               @Commit_point_set: PublishFetchAdd
                @ID: (call_id_t) bin 
                //@Action: model_print("Publish: %d\n", bin);
                @End
        */
        void write_publish(t_element *bin)
        {
                @ID: (call_id_t) bin 
                //@Action: model_print("Publish: %d\n", bin);
                @End
        */
        void write_publish(t_element *bin)
        {
-               /**** Inadmissibility ****/
+               /**** Inadmissibility (testcase2.c) ****/
                int tmp = m_written.fetch_add(1,mo_release);
                /**
                        @Begin
                        @Commit_point_define_check: true
                int tmp = m_written.fetch_add(1,mo_release);
                /**
                        @Begin
                        @Commit_point_define_check: true
-                       @Label: Publish_W_RMW
+                       @Label: PublishFetchAdd
                        @End
                */
                printf("publish: m_written=%d\n", tmp + 1);
                        @End
                */
                printf("publish: m_written=%d\n", tmp + 1);