edits

[cdsspec-compiler.git] / benchmark / mpmc-queue / mpmc-queue.h

diff --git a/benchmark/mpmc-queue/mpmc-queue.h b/benchmark/mpmc-queue/mpmc-queue.h
index dff677773971717e6c584be1fdd021d347ed293d..ff6a168f1c248cc2db457f8fa7b7da8dc818f91a 100644 (file)
--- a/benchmark/mpmc-queue/mpmc-queue.h
+++ b/benchmark/mpmc-queue/mpmc-queue.h
@@ -19,7 +19,9 @@ struct mpmc_boundq_1_alt
 private:
        
        unsigned int MASK;
-
+       
+       atomic<t_element*> arr;
+       
        // elements should generally be cache-line-size padded :
        t_element               m_array[t_size];
 
@@ -31,7 +33,7 @@ private:
 
 public:
 
-       mpmc_boundq_1_alt()
+       mpmc_boundq_1_alt(int _MASK = 0xFFFF)
        {
        /**
                @Begin
@@ -42,7 +44,8 @@ public:
                m_read = 0;
                m_written = 0;
                // For this we want MASK = 1; MASK wrap around
-               MASK = 0x1; // 11
+               MASK = _MASK; //0x11;
+               arr = m_array;
        }
        
 
@@ -82,7 +85,7 @@ public:
        /**
                @Begin
                @Interface: Fetch
-               @Commit_point_set: Fetch_RW_Load_Empty | Fetch_RW_RMW | Fetch_W_Load
+               @Commit_point_set: FetchReadRW1 | FetchReadRW2 | FetchReadPointer
                @ID: (call_id_t) __RET__
                //@Action: model_print("Fetch: %d\n", __RET__);
                @End
@@ -93,8 +96,8 @@ public:
                //unsigned int rdwr = m_rdwr.load(mo_relaxed);
                /**
                        @Begin
-                       @Potential_commit_point_define: true
-                       @Label: Fetch_Potential_RW_Load
+                       @Commit_point_define_check: true
+                       @Label: FetchReadRW1
                        @End
                */
                unsigned int rd,wr;
@@ -103,31 +106,29 @@ public:
                        wr = rdwr & MASK;
 
                        if ( wr == rd ) { // empty
-
-                               /**
-                                       @Begin
-                                       @Commit_point_define: true
-                                       @Potential_commit_point_label: Fetch_Potential_RW_Load
-                                       @Label: Fetch_RW_Load_Empty
-                                       @End
-                               */
-
                                return false;
                        }
-                       
                        /**** Inadmissibility (testcase2.cc, MASK = 1, size = 1) ****/
                        bool succ =
-                       m_rdwr.compare_exchange_weak(rdwr,rdwr+(1<<16),mo_acq_rel);
-                       /**
-                               @Begin
-                               @Commit_point_define_check: succ
-                               @Label: Fetch_RW_RMW
-                               @End
-                       */
-                       if (succ)
+                               m_rdwr.compare_exchange_weak(rdwr,rdwr+(1<<16),mo_acq_rel);
+                       if (succ) {
                                break;
-                       else
+                       } else {
+                               /**
+                                       @Begin
+                                       @Commit_point_clear: true
+                                       @Label: FetchClear1
+                                       @End
+                               */
+
+                               /**
+                                       @Begin
+                                       @Commit_point_define_check: true
+                                       @Label: FetchReadRW2
+                                       @End
+                               */
                                thrd_yield();
+                       }
                }
 
                // (*1)
@@ -135,12 +136,6 @@ public:
                while (true) {
                        /**** Inadmissibility ****/
                        int written = m_written.load(mo_acquire);
-                       /**
-                               @Begin
-                               @Potential_commit_point_define: true
-                               @Label: Fetch_Potential_W_Load
-                               @End
-                       */
                        if ((written & MASK) != wr) {
                                thrd_yield();
                        } else {
@@ -148,16 +143,23 @@ public:
                                break;
                        }
                }
-               
+               t_element * p = & ( m_array[ rd % t_size ] );
+
+               // This is just a hack to tell the CDSChecker that we have a memory
+               // operation here
+               arr.load(memory_order_relaxed);
                /**
                        @Begin
-                       @Commit_point_define: true
-                       @Potential_commit_point_label: Fetch_Potential_W_Load
-                       @Label: Fetch_W_Load
+                       @Commit_point_clear: true
+                       @Label: FetchClear2
+                       @End
+               */
+               /**
+                       @Begin
+                       @Commit_point_define_check: true
+                       @Label: FetchReadPointer
                        @End
                */
-
-               t_element * p = & ( m_array[ rd % t_size ] );
                
                return p;
        }
@@ -165,7 +167,7 @@ public:
        /**
                @Begin
                @Interface: Consume
-               @Commit_point_set: Consume_R_RMW
+               @Commit_point_set: ConsumeFetchAdd
                @ID: (call_id_t) bin 
                //@Action: model_print("Consume: %d\n", bin);
                @End
@@ -176,7 +178,7 @@ public:
                /**
                        @Begin
                        @Commit_point_define_check: true
-                       @Label: Consume_R_RMW
+                       @Label: ConsumeFetchAdd
                        @End
                */
        }
@@ -186,7 +188,7 @@ public:
        /**
                @Begin
                @Interface: Prepare 
-               @Commit_point_set: Prepare_RW_Load_Full | Prepare_RW_RMW | Prepare_R_Load
+               @Commit_point_set: PrepareReadRW1 | PrepareReadRW2 | PrepareReadPointer
                @ID: (call_id_t) __RET__
                //@Action: model_print("Prepare: %d\n", __RET__);
                @End
@@ -198,8 +200,8 @@ public:
                //unsigned int rdwr = m_rdwr.load(mo_relaxed);
                /**
                        @Begin
-                       @Potential_commit_point_define: true
-                       @Label: Prepare_Potential_RW_Load
+                       @Commit_point_define_check: true
+                       @Label: PrepareReadRW1
                        @End
                */
                unsigned int rd,wr;
@@ -209,31 +211,31 @@ public:
                        //printf("write_prepare: rd=%d, wr=%d\n", rd, wr);
 
                        if ( wr == ((rd + t_size)&MASK) ) { // full
-
-                               /**
-                                       @Begin
-                                       @Commit_point_define: true
-                                       @Potential_commit_point_label: Prepare_Potential_RW_Load
-                                       @Label: Prepare_RW_Load_Full
-                                       @End
-                               */
                                return NULL;
                        }
                        
                        /**** Inadmissibility (testcase3.cc, MASK = 1, size = 1) ****/
                        bool succ = m_rdwr.compare_exchange_weak(rdwr,(rd<<16) |
                                ((wr+1)&MASK),mo_acq_rel);
-                       /**
-                               @Begin
-                               @Commit_point_define_check: succ
-                               @Label: Prepare_RW_RMW
-                               @End
-                       */
                        //printf("wr=%d\n", (wr+1)&MASK);
-                       if (succ)
+                       if (succ) {
                                break;
-                       else
+                       } else {
+                               /**
+                                       @Begin
+                                       @Commit_point_clear: true
+                                       @Label: PrepareClear1
+                                       @End
+                               */
+
+                               /**
+                                       @Begin
+                                       @Commit_point_define_check: true
+                                       @Label: PrepareReadRW2
+                                       @End
+                               */
                                thrd_yield();
+                       }
                }
 
                // (*1)
@@ -241,27 +243,29 @@ public:
                while (true) {
                        /**** Inadmissibility ****/
                        int read = m_read.load(mo_acquire);
-                       /**
-                               @Begin
-                               @Potential_commit_point_define: true
-                               @Label: Prepare_Potential_R_Load
-                               @End
-                       */
                        if ((read & MASK) != rd)
                                thrd_yield();
                        else
                                break;
                }
 
+               t_element * p = & ( m_array[ wr % t_size ] );
+
+               // This is also just a hack to tell the CDSChecker that we have a memory
+               // operation here
+               arr.load(memory_order_relaxed);
                /**
                        @Begin
-                       @Commit_point_define: true
-                       @Potential_commit_point_label: Prepare_Potential_R_Load
-                       @Label: Prepare_R_Load
+                       @Commit_point_clear: true
+                       @Label: PrepareClear2
+                       @End
+               */
+               /**
+                       @Begin
+                       @Commit_point_define_check: true
+                       @Label: PrepareReadPointer
                        @End
                */
-
-               t_element * p = & ( m_array[ wr % t_size ] );
 
                return p;
        }