more fix
[cdsspec-compiler.git] / benchmark / mpmc-queue / mpmc-queue.h
index 1e59f43..a1f5b1c 100644 (file)
@@ -26,12 +26,167 @@ public:
        
 
        /**
-       @Global_define:
-       Order_queue<unsigned int*> spec_queue;
+               @Global_define:
+               @Options:
+                       LANG = CPP;
+                       CLASS = mpmc_boundq_1_alt;
+               @DeclareStruct:
+                       typedef struct elem {
+                               t_element *pos;
+                               boolean written;
+                               thread_id_t tid;
+                               call_id_t id;
+                       } elem;
+               @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, thread_id_t tid) {
+                               elem *e = (elem*) MODEL_MALLOC(sizeof(elem));
+                               e->pos = pos;
+                               e->written = false;
+                               e->id = id;
+                               e->tid = tid;
+                       }
+               @DefineFunc:
+                       elem* get_elem_by_pos(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:
+                       elem* get_elem_by_tid(thread_id_t tid) {
+                               for (int i = 0; i < size(list); i++) {
+                                       elem *e = (elem*) elem_at_index(list, i);
+                                       if (e->tid== tid) {
+                                               return e;
+                                       }
+                               }
+                               return NULL;
+                       }
+               @DefineFunc:
+                       int elem_idx_by_pos(t_element *pos) {
+                               for (int i = 0; i < size(list); i++) {
+                                       elem *existing = (elem*) elem_at_index(list, i);
+                                       if (pos == existing->pos) {
+                                               return i;
+                                       }
+                               }
+                               return -1;
+                       }
+               @DefineFunc:
+                       int elem_idx_by_tid(thread_id_t tid) {
+                               for (int i = 0; i < size(list); i++) {
+                                       elem *existing = (elem*) elem_at_index(list, i);
+                                       if (tid == existing->tid) {
+                                               return i;
+                                       }
+                               }
+                               return -1;
+                       }
+               @DefineFunc:
+                       call_id_t prepare_id() {
+                               return get_and_inc(tag);
+                       }
+               @DefineFunc:
+                       bool prepare_check(t_element *pos, thread_id_t tid) {
+                               elem *e = get_elem_by_tid(tid);
+                               return NULL == e;
+                       }
+               @DefineFunc:
+                       void prepare(call_id_t id, t_element *pos, thread_id_t tid) {
+                               call_id_t id = get_and_inc(tag);
+                               elem *e = new_elem(pos, id, tid);
+                               push_back(list, e);
+                       }
+               @DefineFunc:
+                       call_id_t publish_id(thread_id_t tid) {
+                               elem *e = get_elem_by_tid(tid);
+                               if (NULL == e)
+                                       return DEFAULT_CALL_ID;
+                               return e->id;
+                       }
+               @DefineFunc:
+                       bool publish_check(thread_id_t tid) {
+                               elem *e = get_elem_by_tid(tid);
+                               if (NULL == e)
+                                       return false;
+                               return e->written;
+                       }
+               @DefineFunc:
+                       void publish(thread_id_t tid) {
+                               elem *e = get_elem_by_tid(tid);
+                               e->written = true;
+                       }
+               @DefineFunc:
+                       call_id_t fetch_id(t_element *pos) {
+                               elem *e = get_elem_by_pos(pos);
+                               if (NULL == e)
+                                       return DEFAULT_CALL_ID;
+                               return e->id;
+                       }
+               @DefineFunc:
+                       bool fetch_check(t_element *pos) {
+                               int idx = elem_idx_by_pos(pos);
+                               if (idx == -1)
+                                       return false;
+                               else
+                                       return true;
+                       }
+               @DefineFunc:
+                       void fetch(t_element *pos) {
+                               int idx = elem_idx_by_pos(pos);
+                               if (idx == -1)
+                                       return;
+                               remove_at_index(list, idx);
+                       }
+               @DefineFunc:
+                       bool consume_check(thread_id_t tid) {
+                               elem *e = get_elem_by_tid(tid);
+                               if (NULL == e)
+                                       return false;
+                               return e->written;
+                       }
+               @DefineFunc:
+                       call_id_t consume_id(thread_id_t tid) {
+                               elem *e = get_elem_by_tid(tid);
+                               if (NULL == e)
+                                       return DEFAULT_CALL_ID;
+                               return e->id;
+                       }
+               @DefineFunc:
+                       void consume(thread_id_t tid) {
+                               int idx = elem_idx_by_tid(tid);
+                               if (idx == -1)
+                                       return;
+                               remove_at_index(list, idx);
+                       }
+       @Happens_before:
+               Prepare -> Fetch
+               Publish -> Consume
+       @End
        */
 
        //-----------------------------------------------------
 
+       /**
+               @Begin
+               @Interface: Fetch
+               @Commit_point_set: Fetch_Point
+               @ID: fetch_id(__RET__)
+               @Check:
+                       fetch_check(__RET__)
+               @Action:
+                       fetch(__RET__);
+               @End
+       */
        t_element * read_fetch() {
                unsigned int rdwr = m_rdwr.load(mo_acquire);
                unsigned int rd,wr;
@@ -57,29 +212,37 @@ public:
 
                t_element * p = & ( m_array[ rd % t_size ] );
                
-               /**
-                       @Commit_point_Check: true
-                       @Label: ANY
-                       @Check:
-                               spec_queue.peak() == p
-               */
                return p;
        }
 
+       /**
+               @Begin
+               @Interface: Consume
+               @Commit_point_set: Consume_Point
+               @ID: consume_id(__TID__)
+               @Check:
+                       consume_check(__TID__)
+               @Action:
+                       consume(__TID__);
+               @End
+       */
        void read_consume() {
                m_read.fetch_add(1,mo_release);
-               /**
-                       @Commit_point_define: true
-                       @Label: Read_Consume_Success
-                       @Check:
-                               spec_queue.size() > 0
-                       @Action:
-                               spec_queue.remove();
-               */
        }
 
        //-----------------------------------------------------
 
+       /**
+               @Begin
+               @Interface: Prepare 
+               @Commit_point_set: Prepare_Point
+               @ID: prepare_id(__RET__)
+               @Check:
+                       prepare_check(__RET__)
+               @Action:
+                       prepare(__RET__);
+               @End
+       */
        t_element * write_prepare() {
                unsigned int rdwr = m_rdwr.load(mo_acquire);
                unsigned int rd,wr;
@@ -105,13 +268,20 @@ public:
 
                t_element * p = & ( m_array[ wr % t_size ] );
 
-               /**
-                       @Commit_point_check: ANY
-                       @Action: spec_queue.add(p);
-               */
                return p;
        }
 
+       /**
+               @Begin
+               @Interface: Publish 
+               @Commit_point_set: Publish_Point
+               @ID: publish_id(__TID__)
+               @Check:
+                       publish_check(__TID__)
+               @Action:
+                       publish(__TID__);
+               @End
+       */
        void write_publish()
        {
                m_written.fetch_add(1,mo_release);