From 4248575daeca107e83ab40cff5a0a9e4ec1d72d0 Mon Sep 17 00:00:00 2001 From: Peizhao Ou Date: Tue, 25 Mar 2014 05:01:49 -0700 Subject: [PATCH] reset mpmc spec --- benchmark/mpmc-queue/mpmc-queue.cc | 17 +- benchmark/mpmc-queue/mpmc-queue.h | 251 +++++------------------------ 2 files changed, 50 insertions(+), 218 deletions(-) diff --git a/benchmark/mpmc-queue/mpmc-queue.cc b/benchmark/mpmc-queue/mpmc-queue.cc index cfa82f2..ca063e9 100644 --- a/benchmark/mpmc-queue/mpmc-queue.cc +++ b/benchmark/mpmc-queue/mpmc-queue.cc @@ -12,8 +12,9 @@ void threadA(struct mpmc_boundq_1_alt *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 *queue) @@ -22,7 +23,8 @@ void threadB(struct mpmc_boundq_1_alt *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 *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 queue; + struct mpmc_boundq_1_alt 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"); diff --git a/benchmark/mpmc-queue/mpmc-queue.h b/benchmark/mpmc-queue/mpmc-queue.h index ee3950d..e6d5485 100644 --- a/benchmark/mpmc-queue/mpmc-queue.h +++ b/benchmark/mpmc-queue/mpmc-queue.h @@ -2,6 +2,12 @@ #include #include +#include +#include +#include +#include +#include + /** @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 -- 2.34.1