changes to mpmc spec and add notes to ms-queue
[cdsspec-compiler.git] / benchmark / mpmc-queue / mpmc-queue.h
index e6d5485..1b737bd 100644 (file)
@@ -73,7 +73,7 @@ public:
        /**
                @Begin
                @Interface: Fetch
-               @Commit_point_set: Fetch_Empty_Point | Fetch_Succ_Point
+               @Commit_point_set: Fetch_RW_Load_Empty | Fetch_RW_RMW | Fetch_W_Load
                @ID: (call_id_t) __RET__
                //@Check:
                        //__RET__ == NULL || has_elem(list, __RET__)
@@ -86,7 +86,7 @@ public:
                /**
                        @Begin
                        @Potential_commit_point_define: true
-                       @Label: Fetch_Potential_Point
+                       @Label: Fetch_Potential_RW_Load
                        @End
                */
                unsigned int rd,wr;
@@ -99,8 +99,8 @@ public:
                                /**
                                        @Begin
                                        @Commit_point_define: true
-                                       @Potential_commit_point_label: Fetch_Potential_Point 
-                                       @Label: Fetch_Empty_Point
+                                       @Potential_commit_point_label: Fetch_Potential_RW_Load
+                                       @Label: Fetch_RW_Load_Empty
                                        @End
                                */
 
@@ -110,8 +110,8 @@ public:
                        bool succ = m_rdwr.compare_exchange_weak(rdwr,rdwr+(1<<16),mo_acq_rel);
                        /**
                                @Begin
-                               @Commit_point_define_check: succ == true
-                               @Label: Fetch_Succ_Point
+                               @Commit_point_define_check: succ
+                               @Label: Fetch_RW_RMW
                                @End
                        */
                        if (succ)
@@ -122,9 +122,28 @@ public:
 
                // (*1)
                rl::backoff bo;
-               while ( (m_written.load(mo_acquire) & 0xFFFF) != wr ) {
-                       thrd_yield();
+               while (true) {
+                       int written = m_written.load(mo_acquire);
+                       /**
+                               @Begin
+                               @Potential_commit_point_define: true
+                               @Label: Fetch_Potential_W_Load
+                               @End
+                       */
+                       if ((written & 0xFFFF) != wr) {
+                               thrd_yield();
+                       } else {
+                               break;
+                       }
                }
+               
+               /**
+                       @Begin
+                       @Commit_point_define: true
+                       @Potential_commit_point_label: Fetch_Potential_W_Load
+                       @Label: Fetch_W_Load
+                       @End
+               */
 
                t_element * p = & ( m_array[ rd % t_size ] );
                
@@ -134,7 +153,7 @@ public:
        /**
                @Begin
                @Interface: Consume
-               @Commit_point_set: Consume_Point
+               @Commit_point_set: Consume_R_RMW
                @ID: (call_id_t) bin 
                //@Check:
                //      consume_check(__TID__)
@@ -148,7 +167,7 @@ public:
                /**
                        @Begin
                        @Commit_point_define_check: true
-                       @Label: Consume_Point
+                       @Label: Consume_R_RMW
                        @End
                */
        }
@@ -158,7 +177,7 @@ public:
        /**
                @Begin
                @Interface: Prepare 
-               @Commit_point_set: Prepare_Full_Point | Prepare_Succ_Point
+               @Commit_point_set: Prepare_RW_Load_Full | Prepare_RW_RMW | Prepare_R_Load
                @ID: (call_id_t) __RET__
                //@Check:
                        //prepare_check(__RET__, __TID__)
@@ -173,7 +192,7 @@ public:
                /**
                        @Begin
                        @Potential_commit_point_define: true
-                       @Label: Prepare_Potential_Point
+                       @Label: Prepare_Potential_RW_Load
                        @End
                */
                unsigned int rd,wr;
@@ -186,8 +205,8 @@ public:
                                /**
                                        @Begin
                                        @Commit_point_define: true
-                                       @Potential_commit_point_label: Prepare_Potential_Point 
-                                       @Label: Prepare_Full_Point
+                                       @Potential_commit_point_label: Prepare_Potential_RW_Load
+                                       @Label: Prepare_RW_Load_Full
                                        @End
                                */
                                return NULL;
@@ -197,8 +216,8 @@ public:
                                ((wr+1)&0xFFFF),mo_acq_rel);
                        /**
                                @Begin
-                               @Commit_point_define_check: succ == true
-                               @Label: Prepare_Succ_Point
+                               @Commit_point_define_check: succ
+                               @Label: Prepare_RW_RMW
                                @End
                        */
                        if (succ)
@@ -209,10 +228,28 @@ public:
 
                // (*1)
                rl::backoff bo;
-               while ( (m_read.load(mo_acquire) & 0xFFFF) != rd ) {
-                       thrd_yield();
+               while (true) {
+                       int read = m_read.load(mo_acquire);
+                       /**
+                               @Begin
+                               @Potential_commit_point_define: true
+                               @Label: Prepare_Potential_R_Load
+                               @End
+                       */
+                       if ((read & 0xFFFF) != rd)
+                               thrd_yield();
+                       else
+                               break;
                }
 
+               /**
+                       @Begin
+                       @Commit_point_define: true
+                       @Potential_commit_point_label: Prepare_Potential_R_Load
+                       @Label: Prepare_R_Load
+                       @End
+               */
+
                t_element * p = & ( m_array[ wr % t_size ] );
 
                return p;
@@ -221,7 +258,7 @@ public:
        /**
                @Begin
                @Interface: Publish 
-               @Commit_point_set: Publish_Point
+               @Commit_point_set: Publish_W_RMW
                @ID: (call_id_t) bin 
                //@Check:
                        //publish_check(__TID__)
@@ -236,7 +273,7 @@ public:
                /**
                        @Begin
                        @Commit_point_define_check: true
-                       @Label: Publish_Point
+                       @Label: Publish_W_RMW
                        @End
                */
        }