save

[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 863710139c2e196d0e0ae8a40f6d6325b4a16989..5d20f3067f4674dde6b5dc936bdbd41e7c45eedf 100644 (file)
--- a/benchmark/mpmc-queue/mpmc-queue.h
+++ b/benchmark/mpmc-queue/mpmc-queue.h
@@ -1,6 +1,19 @@
 #include <stdatomic.h>
 #include <unrelacy.h>
-
+#include <common.h>
+
+#include <spec_lib.h>
+#include <stdlib.h>
+#include <cdsannotate.h>
+#include <specannotation.h>
+#include <model_memory.h>
+#include "common.h" 
+
+/**
+       @Begin
+       @Class_begin
+       @End
+*/
 template <typename t_element, size_t t_size>
 struct mpmc_boundq_1_alt
 {
@@ -19,6 +32,11 @@ public:
 
        mpmc_boundq_1_alt()
        {
+       /**
+               @Begin
+                       @Entry_point
+                       @End
+               */
                m_rdwr = 0;
                m_read = 0;
                m_written = 0;
@@ -26,74 +44,56 @@ public:
        
 
        /**
-               @Global_define:
+               @Begin
                @Options:
                        LANG = CPP;
                        CLASS = mpmc_boundq_1_alt;
-               @DeclareStruct:
-                       typedef struct elem {
-                               t_element* pos;
-                               boolean written;
-                               call_id_t id;
-                       } elem;
+               @Global_define:
                @DeclareVar:
-                       spec_list *list;
                        id_tag_t *tag;
                @InitVar:
-                       list = new_spec_list();
-                       tag = new_id_tag();
-               @DefineFunc:
-                       elem* new_elem(t_element *pos, call_id_t id) {
-                               elem *e = (elem*) MODEL_MALLOC(sizeof(elem));
-                               e->pos = pos;
-                               e->written = false;
-                               e->id = id;
-                       }
-               @DefineFunc:
-                       elem* get_elem(t_element *pos) {
-                               for (int i = 0; i < size(list); i++) {
-                                       elem *e = (elem*) elem_at_index(list, i);
-                                       if (e->pos == pos) {
-                                               return e;
-                                       }
-                               }
-                               return NULL;
-                       }
-               @DefineFunc:
-                       bool has_elem(elem *e) {
-                               for (int i = 0; i < size(list); i++) {
-                                       elem *existing = (elem*) elem_at_index(list, i);
-                                       if (e->pos == existing->pos) {
-                                               return true;
-                                       }
-                               }
-                               return false;
-                       }
-               @DefineFunc:
-                       bool insert_elem(elem *e) {
-                               push_back(list, e);
-                       }
-               @DefineFunc:
-                       void consume_elem(t_element *pos) {
-                               
-                       }
-
+                       tag = NULL;
+       @Happens_before:
+               Publish -> Fetch
+       @End
        */
 
        //-----------------------------------------------------
 
+       /**
+               @Begin
+               @Interface: Fetch
+               @Commit_point_set: Fetch_Succ_Point | Fetch_Fail_Point
+               @ID: (call_id_t) __RET__
+               @End
+       */
        t_element * read_fetch() {
                unsigned int rdwr = m_rdwr.load(mo_acquire);
+               /**
+                       @Begin
+                       @Potential_commit_point_define: true
+                       @Label: Fetch_Potential_Point
+                       @End
+               */
                unsigned int rd,wr;
                for(;;) {
                        rd = (rdwr>>16) & 0xFFFF;
                        wr = rdwr & 0xFFFF;
 
                        if ( wr == rd ) { // empty
+                               /**
+                                       @Begin
+                                       @Commit_point_define: true
+                                       @Potential_commit_point_label: Fetch_Potential_Point 
+                                       @Label: Fetch_Fail_Point
+                                       @End
+                               */
                                return false;
                        }
-
-                       if ( m_rdwr.compare_exchange_weak(rdwr,rdwr+(1<<16),mo_acq_rel) )
+                       
+                       bool succ = m_rdwr.compare_exchange_weak(rdwr,rdwr+(1<<16),mo_acq_rel);
+                       
+                       if (succ)
                                break;
                        else
                                thrd_yield();
@@ -101,7 +101,16 @@ public:
 
                // (*1)
                rl::backoff bo;
-               while ( (m_written.load(mo_acquire) & 0xFFFF) != wr ) {
+               while ( true ) {
+                       unsigned int tmp = m_written.load(mo_acquire);
+                       /**
+                               @Begin
+                               @Commit_point_define_check: (tmp & 0xFFFF) == wr
+                               @Label: Fetch_Succ_Point
+                               @End
+                       */
+                       if ((tmp & 0xFFFF) == wr)
+                               break;
                        thrd_yield();
                }
 
@@ -123,10 +132,13 @@ public:
                        rd = (rdwr>>16) & 0xFFFF;
                        wr = rdwr & 0xFFFF;
 
-                       if ( wr == ((rd + t_size)&0xFFFF) ) // full
+                       if ( wr == ((rd + t_size)&0xFFFF) ) { // full
                                return NULL;
-
-                       if ( m_rdwr.compare_exchange_weak(rdwr,(rd<<16) | ((wr+1)&0xFFFF),mo_acq_rel) )
+                       }
+                       
+                       bool succ = m_rdwr.compare_exchange_weak(rdwr,(rd<<16) |
+                               ((wr+1)&0xFFFF),mo_acq_rel);
+                       if (succ)
                                break;
                        else
                                thrd_yield();
@@ -138,18 +150,35 @@ public:
                        thrd_yield();
                }
 
-
                t_element * p = & ( m_array[ wr % t_size ] );
 
                return p;
        }
 
-       void write_publish()
+       /**
+               @Begin
+               @Interface: Publish 
+               @Commit_point_set: Publish_Point
+               @ID: (uint64_t) elem
+               @End
+       */
+       void write_publish(t_element *elem)
        {
                m_written.fetch_add(1,mo_release);
+               /**
+                       @Begin
+                       @Commit_point_define_check: true
+                       @Label: Publish_Point
+                       @End
+               */
        }
 
        //-----------------------------------------------------
 
 
 };
+/**
+       @Begin
+       @Class_end
+       @End
+*/