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 a0797bc28bd5435ca101181d0a66c20514dab48b..aa1012976ee8501596d27cc7852f9006ea0e1e0c 100644 (file)
--- a/benchmark/mpmc-queue/mpmc-queue.h
+++ b/benchmark/mpmc-queue/mpmc-queue.h
@@ -7,7 +7,6 @@
 #include <cdsannotate.h>
 #include <specannotation.h>
 #include <model_memory.h>
-#include "common.h" 
 
 /**
        @Begin
@@ -49,12 +48,26 @@ public:
                        LANG = CPP;
                        CLASS = mpmc_boundq_1_alt;
                @Global_define:
-               @DeclareVar:
-                       id_tag_t *tag;
-               @InitVar:
-                       tag = NULL;
+               //@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();
+                       //tag = new_id_tag();
+       //      @Cleanup:
+//                     if (list)
+//                             free_spec_list();
        @Happens_before:
                Publish -> Fetch
+               Consume -> Prepare
        @End
        */
 
@@ -63,16 +76,20 @@ public:
        /**
                @Begin
                @Interface: Fetch
-               @Commit_point_set: 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__)
                @End
        */
        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);
                /**
                        @Begin
-                       @Commit_point_define_check: (rdwr>>16) & 0xFFFF == rdwr & 0xFFFF
-                       @Label: Fetch_Succ_Point1
+                       @Potential_commit_point_define: true
+                       @Label: Fetch_Potential_RW_Load
                        @End
                */
                unsigned int rd,wr;
@@ -81,11 +98,25 @@ public:
                        wr = rdwr & 0xFFFF;
 
                        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;
                        }
                        
                        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)
                                break;
                        else
@@ -94,43 +125,104 @@ public:
 
                // (*1)
                rl::backoff bo;
-               while ( true ) {
-                       unsigned int tmp = m_written.load(mo_acquire);
+               while (true) {
+                       int written = m_written.load(mo_acquire);
                        /**
                                @Begin
-                               @Commit_point_define_check: (tmp & 0xFFFF) == wr
-                               @Label: Fetch_Succ_Point2
+                               @Potential_commit_point_define: true
+                               @Label: Fetch_Potential_W_Load
                                @End
                        */
-                       if ((tmp & 0xFFFF) == wr)
+                       if ((written & 0xFFFF) != wr) {
+                               thrd_yield();
+                       } else {
                                break;
-                       thrd_yield();
+                       }
                }
+               
+               /**
+                       @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 ] );
                
                return p;
        }
 
-       void read_consume() {
+       /**
+               @Begin
+               @Interface: Consume
+               @Commit_point_set: Consume_R_RMW
+               @ID: (call_id_t) bin 
+               //@Check:
+               //      consume_check(__TID__)
+               //@Action:
+                       //consume(__TID__);
+               @End
+       */
+       void read_consume(t_element *bin) {
+               /**** FIXME: miss ****/
                m_read.fetch_add(1,mo_release);
+               /**
+                       @Begin
+                       @Commit_point_define_check: true
+                       @Label: Consume_R_RMW
+                       @End
+               */
        }
 
        //-----------------------------------------------------
 
+       /**
+               @Begin
+               @Interface: Prepare 
+               @Commit_point_set: Prepare_RW_Load_Full | Prepare_RW_RMW | Prepare_R_Load
+               @ID: (call_id_t) __RET__
+               //@Check:
+                       //prepare_check(__RET__, __TID__)
+               //@Action:
+                       //push_back(list, __RET__);
+               @End
+       */
        t_element * write_prepare() {
+               // Try weaker semantics
                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_RW_Load
+                       @End
+               */
                unsigned int rd,wr;
                for(;;) {
                        rd = (rdwr>>16) & 0xFFFF;
                        wr = rdwr & 0xFFFF;
 
                        if ( wr == ((rd + t_size)&0xFFFF) ) { // full
+
+                               /**
+                                       @Begin
+                                       @Commit_point_define: true
+                                       @Potential_commit_point_label: Prepare_Potential_RW_Load
+                                       @Label: Prepare_RW_Load_Full
+                                       @End
+                               */
                                return NULL;
                        }
                        
                        bool succ = m_rdwr.compare_exchange_weak(rdwr,(rd<<16) |
                                ((wr+1)&0xFFFF),mo_acq_rel);
+                       /**
+                               @Begin
+                               @Commit_point_define_check: succ
+                               @Label: Prepare_RW_RMW
+                               @End
+                       */
                        if (succ)
                                break;
                        else
@@ -139,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;
@@ -151,17 +261,22 @@ public:
        /**
                @Begin
                @Interface: Publish 
-               @Commit_point_set: Publish_Point
-               @ID: (uint64_t) elem
+               @Commit_point_set: Publish_W_RMW
+               @ID: (call_id_t) bin 
+               //@Check:
+                       //publish_check(__TID__)
+               //@Action:
+                       //publish(__TID__);
                @End
        */
-       void write_publish(t_element *elem)
+       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
                */
        }