reset mpmc spec
authorPeizhao Ou <peizhaoo@uci.edu>
Tue, 25 Mar 2014 12:01:49 +0000 (05:01 -0700)
committerPeizhao Ou <peizhaoo@uci.edu>
Tue, 25 Mar 2014 12:01:49 +0000 (05:01 -0700)
benchmark/mpmc-queue/mpmc-queue.cc
benchmark/mpmc-queue/mpmc-queue.h

index cfa82f2..ca063e9 100644 (file)
@@ -12,8 +12,9 @@ void threadA(struct mpmc_boundq_1_alt<int32_t, sizeof(int32_t)> *queue)
 {
        int32_t *bin = queue->write_prepare();
        store_32(bin, 1);
+       *bin = 1;
        printf("write_bin %d, val %d\n", bin, 1);
-       queue->write_publish();
+       queue->write_publish(bin);
 }
 
 void threadB(struct mpmc_boundq_1_alt<int32_t, sizeof(int32_t)> *queue)
@@ -22,7 +23,8 @@ void threadB(struct mpmc_boundq_1_alt<int32_t, sizeof(int32_t)> *queue)
        while (bin = queue->read_fetch()) {
                printf("Read: %d\n", load_32(bin));
                printf("read_bin %d, val %d\n", bin, load_32(bin));
-               queue->read_consume();
+               printf("Read: %d\n", *bin);
+               queue->read_consume(bin);
        }
 }
 
@@ -30,11 +32,13 @@ void threadC(struct mpmc_boundq_1_alt<int32_t, sizeof(int32_t)> *queue)
 {
        int32_t *bin = queue->write_prepare();
        store_32(bin, 1);
-       queue->write_publish();
+       *bin = 1;
+       queue->write_publish(bin);
 
        while (bin = queue->read_fetch()) {
                printf("Read: %d\n", load_32(bin));
-               queue->read_consume();
+               printf("Read: %d\n", *bin);
+               queue->read_consume(bin);
        }
 }
 
@@ -104,7 +108,7 @@ void process_params(int argc, char **argv)
 
 int user_main(int argc, char **argv)
 {
-       struct mpmc_boundq_1_alt<int32_t, sizeof(int32_t)> queue;
+       struct mpmc_boundq_1_alt<int32_t, 2> queue;
        thrd_t A[MAXWRITERS], B[MAXREADERS], C[MAXRDWR];
 
        /* Note: optarg() / optind is broken in model-checker - workaround is
@@ -116,8 +120,9 @@ int user_main(int argc, char **argv)
        printf("Adding initial element\n");
        int32_t *bin = queue.write_prepare();
        store_32(bin, 17);
+       *bin, 17;
        printf("init_write_bin %d, val %d\n", bin, 17);
-       queue.write_publish();
+       queue.write_publish(bin);
 #endif
 
        printf("Start threads\n");
index ee3950d..e6d5485 100644 (file)
@@ -2,6 +2,12 @@
 #include <unrelacy.h>
 #include <common.h>
 
+#include <spec_lib.h>
+#include <stdlib.h>
+#include <cdsannotate.h>
+#include <specannotation.h>
+#include <model_memory.h>
+
 /**
        @Begin
        @Class_begin
@@ -52,199 +58,13 @@ public:
                        } elem;
                @DeclareVar:
                        spec_list *list;
-                       id_tag_t *tag;
+                       //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;
-                               e->fetch_tid = -1;
-                       }
-               @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:
-                       void show_list() {
-                               //model_print("Status:\n");
-                               for (int i = 0; i < size(list); i++) {
-                                       elem *e = (elem*) elem_at_index(list, i);
-                                       //model_print("%d: pos %d, written %d, tid %d, fetch_tid %d, call_id %d\n", i, e->pos, e->written, e->tid, e->fetch_tid, e->id); 
-                               }
-                       }
-               @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:
-                       elem* get_elem_by_fetch_tid(thread_id_t fetch_tid) {
-                               for (int i = 0; i < size(list); i++) {
-                                       elem *e = (elem*) elem_at_index(list, i);
-                                       if (e->fetch_tid== fetch_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:
-                       int elem_idx_by_fetch_tid(thread_id_t fetch_tid) {
-                               for (int i = 0; i < size(list); i++) {
-                                       elem *existing = (elem*) elem_at_index(list, i);
-                                       if (fetch_tid == existing->fetch_tid) {
-                                               return i;
-                                       }
-                               }
-                               return -1;
-                       }
-               @DefineFunc:
-                       int elem_num(t_element *pos) {
-                               int cnt = 0;
-                               for (int i = 0; i < size(list); i++) {
-                                       elem *existing = (elem*) elem_at_index(list, i);
-                                       if (pos == existing->pos) {
-                                               cnt++;
-                                       }
-                               }
-                               return cnt;
-                       }
-               @DefineFunc:
-                       call_id_t prepare_id() {
-                               call_id_t res = get_and_inc(tag);
-                               //model_print("prepare_id: %d\n", res);
-                               return res;
-                       }
-               @DefineFunc:
-                       bool prepare_check(t_element *pos, thread_id_t tid) {
-                               show_list();
-                               elem *e = get_elem_by_pos(pos);
-                               //model_print("prepare_check: e %d\n", e);
-                               return NULL == e;
-                       }
-               @DefineFunc:
-                       void prepare(call_id_t id, t_element *pos, thread_id_t tid) {
-                               //model_print("prepare: id %d, pos %d, tid %d\n", id, pos, tid);
-                               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);
-                               //model_print("publish_id: id %d\n", e == NULL ? 0 : e->id);
-                               if (NULL == e)
-                                       return DEFAULT_CALL_ID;
-                               return e->id;
-                       }
-               @DefineFunc:
-                       bool publish_check(thread_id_t tid) {
-                               show_list();
-                               elem *e = get_elem_by_tid(tid);
-                               //model_print("publish_check: tid %d\n", tid);
-                               if (NULL == e)
-                                       return false;
-                               if (elem_num(e->pos) > 1)
-                                       return false;
-                               return !e->written;
-                       }
-               @DefineFunc:
-                       void publish(thread_id_t tid) {
-                               //model_print("publish: tid %d\n", 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);
-                               //model_print("fetch_id: id %d\n", e == NULL ? 0 : e->id);
-                               if (NULL == e)
-                                       return DEFAULT_CALL_ID;
-                               return e->id;
-                       }
-               @DefineFunc:
-                       bool fetch_check(t_element *pos) {
-                               show_list();
-                               if (pos == NULL) return true;
-                               elem *e = get_elem_by_pos(pos);
-                               //model_print("fetch_check: pos %d, e %d\n", pos, e);
-                               if (e == NULL) return false;
-                               if (elem_num(e->pos) > 1)
-                                       return false;
-                               return true;
-                       }
-               @DefineFunc:
-                       void fetch(t_element *pos, thread_id_t tid) {
-                               if (pos == NULL) return;
-                               elem *e = (elem*) get_elem_by_pos(pos);
-                               //model_print("fetch: pos %d, tid %d\n", pos, tid);
-                               // Remember the thread that fetches the position
-                               e->fetch_tid = tid;
-                       }
-               @DefineFunc:
-                       bool consume_check(thread_id_t tid) {
-                               show_list();
-                               elem *e = get_elem_by_fetch_tid(tid);
-                               //model_print("consume_check: tid %d, e %d\n", tid, e);
-                               if (NULL == e)
-                                       return false;
-                               if (elem_num(e->pos) > 1)
-                                       return false;
-                               return e->written;
-                       }
-               @DefineFunc:
-                       call_id_t consume_id(thread_id_t tid) {
-                               elem *e = get_elem_by_fetch_tid(tid);
-                               //model_print("consume_id: id %d\n", e == NULL ? 0 : e->id);
-                               if (NULL == e)
-                                       return DEFAULT_CALL_ID;
-                               return e->id;
-                       }
-               @DefineFunc:
-                       void consume(thread_id_t tid) {
-                               //model_print("consume: tid %d\n", tid);
-                               int idx = elem_idx_by_fetch_tid(tid);
-                               if (idx == -1)
-                                       return;
-                               remove_at_index(list, idx);
-                       }
+                       //tag = new_id_tag();
        @Happens_before:
-               Prepare -> Fetch
-               Publish -> Consume
+               Publish -> Fetch
+               Consume -> Prepare
        @End
        */
 
@@ -254,15 +74,15 @@ public:
                @Begin
                @Interface: Fetch
                @Commit_point_set: Fetch_Empty_Point | Fetch_Succ_Point
-               @ID: fetch_id(__RET__)
-               @Check:
-                       fetch_check(__RET__)
-               @Action:
-                       fetch(__RET__, __TID__);
+               @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
                        @Potential_commit_point_define: true
@@ -275,6 +95,7 @@ public:
                        wr = rdwr & 0xFFFF;
 
                        if ( wr == rd ) { // empty
+
                                /**
                                        @Begin
                                        @Commit_point_define: true
@@ -282,6 +103,7 @@ public:
                                        @Label: Fetch_Empty_Point
                                        @End
                                */
+
                                return false;
                        }
                        
@@ -313,14 +135,15 @@ public:
                @Begin
                @Interface: Consume
                @Commit_point_set: Consume_Point
-               @ID: consume_id(__TID__)
-               @Check:
-                       consume_check(__TID__)
-               @Action:
-                       consume(__TID__);
+               @ID: (call_id_t) bin 
+               //@Check:
+               //      consume_check(__TID__)
+               //@Action:
+                       //consume(__TID__);
                @End
        */
-       void read_consume() {
+       void read_consume(t_element *bin) {
+               /**** FIXME: miss ****/
                m_read.fetch_add(1,mo_release);
                /**
                        @Begin
@@ -336,15 +159,17 @@ public:
                @Begin
                @Interface: Prepare 
                @Commit_point_set: Prepare_Full_Point | Prepare_Succ_Point
-               @ID: prepare_id()
-               @Check:
-                       prepare_check(__RET__, __TID__)
-               @Action:
-                       prepare(__ID__, __RET__, __TID__);
+               @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
@@ -357,6 +182,7 @@ public:
                        wr = rdwr & 0xFFFF;
 
                        if ( wr == ((rd + t_size)&0xFFFF) ) { // full
+
                                /**
                                        @Begin
                                        @Commit_point_define: true
@@ -396,15 +222,16 @@ public:
                @Begin
                @Interface: Publish 
                @Commit_point_set: Publish_Point
-               @ID: publish_id(__TID__)
-               @Check:
-                       publish_check(__TID__)
-               @Action:
-                       publish(__TID__);
+               @ID: (call_id_t) bin 
+               //@Check:
+                       //publish_check(__TID__)
+               //@Action:
+                       //publish(__TID__);
                @End
        */
-       void write_publish()
+       void write_publish(t_element *bin)
        {
+               /**** hb violation ****/
                m_written.fetch_add(1,mo_release);
                /**
                        @Begin