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 d482c9e9790b62d430637b1ec9c222a386199b4a..aa1012976ee8501596d27cc7852f9006ea0e1e0c 100644 (file)
--- a/benchmark/mpmc-queue/mpmc-queue.h
+++ b/benchmark/mpmc-queue/mpmc-queue.h
@@ -48,20 +48,23 @@ public:
                        LANG = CPP;
                        CLASS = mpmc_boundq_1_alt;
                @Global_define:
-               @DeclareStruct:
-                       typedef struct elem {
-                               t_element *pos;
-                               bool written;
-                               thread_id_t tid;
-                               thread_id_t fetch_tid;
-                               call_id_t id;
-                       } elem;
-               @DeclareVar:
-                       spec_list *list;
+               //@DeclareStruct:
+                       //typedef struct elem {
+                       //      t_element *pos;
+                       //      bool written;
+                       //      thread_id_t tid;
+                       //      thread_id_t fetch_tid;
+                       //      call_id_t id;
+               //      } elem;
+       //      @DeclareVar:
+       //              spec_list *list;
                        //id_tag_t *tag;
-               @InitVar:
-                       list = new_spec_list();
+       //      @InitVar:
+       //              list = new_spec_list();
                        //tag = new_id_tag();
+       //      @Cleanup:
+//                     if (list)
+//                             free_spec_list();
        @Happens_before:
                Publish -> Fetch
                Consume -> Prepare
@@ -73,7 +76,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__)
@@ -81,12 +84,12 @@ public:
        */
        t_element * read_fetch() {
                // Try this new weaker semantics
-               //unsigned int rdwr = m_rdwr.load(mo_acquire);
-               unsigned int rdwr = m_rdwr.load(mo_relaxed);
+               unsigned int rdwr = m_rdwr.load(mo_acquire);
+               //unsigned int rdwr = m_rdwr.load(mo_relaxed);
                /**
                        @Begin
                        @Potential_commit_point_define: true
-                       @Label: Fetch_Potential_Point
+                       @Label: Fetch_Potential_RW_Load
                        @End
                */
                unsigned int rd,wr;
@@ -99,8 +102,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 +113,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 +125,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 +156,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__)
@@ -143,11 +165,12 @@ public:
                @End
        */
        void read_consume(t_element *bin) {
+               /**** FIXME: miss ****/
                m_read.fetch_add(1,mo_release);
                /**
                        @Begin
                        @Commit_point_define_check: true
-                       @Label: Consume_Point
+                       @Label: Consume_R_RMW
                        @End
                */
        }
@@ -157,7 +180,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__)
@@ -167,12 +190,12 @@ public:
        */
        t_element * write_prepare() {
                // Try weaker semantics
-               //unsigned int rdwr = m_rdwr.load(mo_acquire);
-               unsigned int rdwr = m_rdwr.load(mo_relaxed);
+               unsigned int rdwr = m_rdwr.load(mo_acquire);
+               //unsigned int rdwr = m_rdwr.load(mo_relaxed);
                /**
                        @Begin
                        @Potential_commit_point_define: true
-                       @Label: Prepare_Potential_Point
+                       @Label: Prepare_Potential_RW_Load
                        @End
                */
                unsigned int rd,wr;
@@ -185,8 +208,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;
@@ -196,8 +219,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)
@@ -208,10 +231,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;
@@ -220,7 +261,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__)
@@ -230,11 +271,12 @@ public:
        */
        void write_publish(t_element *bin)
        {
+               /**** hb violation ****/
                m_written.fetch_add(1,mo_release);
                /**
                        @Begin
                        @Commit_point_define_check: true
-                       @Label: Publish_Point
+                       @Label: Publish_W_RMW
                        @End
                */
        }