From 69183e69892799fb310a328c88c55cd2c71632ce Mon Sep 17 00:00:00 2001 From: Peizhao Ou Date: Thu, 23 Jan 2014 17:07:00 -0800 Subject: [PATCH] save --- benchmark/mpmc-queue/mpmc-queue.cc | 3 + benchmark/mpmc-queue/mpmc-queue.h | 188 +++++++++++++++--- .../codeGenerator/CodeGenerator.java | 7 +- .../codeGenerator/CodeVariables.java | 3 + .../specExtraction/ParserUtils.java | 2 +- 5 files changed, 172 insertions(+), 31 deletions(-) diff --git a/benchmark/mpmc-queue/mpmc-queue.cc b/benchmark/mpmc-queue/mpmc-queue.cc index b62d8d3..cfa82f2 100644 --- a/benchmark/mpmc-queue/mpmc-queue.cc +++ b/benchmark/mpmc-queue/mpmc-queue.cc @@ -12,6 +12,7 @@ void threadA(struct mpmc_boundq_1_alt *queue) { int32_t *bin = queue->write_prepare(); store_32(bin, 1); + printf("write_bin %d, val %d\n", bin, 1); queue->write_publish(); } @@ -20,6 +21,7 @@ void threadB(struct mpmc_boundq_1_alt *queue) int32_t *bin; 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(); } } @@ -114,6 +116,7 @@ int user_main(int argc, char **argv) printf("Adding initial element\n"); int32_t *bin = queue.write_prepare(); store_32(bin, 17); + printf("init_write_bin %d, val %d\n", bin, 17); queue.write_publish(); #endif diff --git a/benchmark/mpmc-queue/mpmc-queue.h b/benchmark/mpmc-queue/mpmc-queue.h index a1f5b1c..627a58b 100644 --- a/benchmark/mpmc-queue/mpmc-queue.h +++ b/benchmark/mpmc-queue/mpmc-queue.h @@ -1,6 +1,12 @@ #include #include +#include +/** + @Begin + @Class_begin + @End +*/ template struct mpmc_boundq_1_alt { @@ -19,6 +25,11 @@ public: mpmc_boundq_1_alt() { + /** + @Begin + @Entry_point + @End + */ m_rdwr = 0; m_read = 0; m_written = 0; @@ -26,15 +37,17 @@ public: /** - @Global_define: + @Begin @Options: LANG = CPP; CLASS = mpmc_boundq_1_alt; + @Global_define: @DeclareStruct: typedef struct elem { t_element *pos; - boolean written; + bool written; thread_id_t tid; + thread_id_t fetch_tid; call_id_t id; } elem; @DeclareVar: @@ -50,6 +63,7 @@ public: e->written = false; e->id = id; e->tid = tid; + e->fetch_tid = -1; } @DefineFunc: elem* get_elem_by_pos(t_element *pos) { @@ -61,6 +75,14 @@ public: } 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++) { @@ -71,6 +93,16 @@ public: } 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++) { @@ -91,79 +123,121 @@ public: } 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() { - return get_and_inc(tag); + 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) { - elem *e = get_elem_by_tid(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) { - call_id_t id = get_and_inc(tag); + 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; - return e->written; + 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) { - int idx = elem_idx_by_pos(pos); - if (idx == -1) + 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; - else - return true; + return true; } @DefineFunc: - void fetch(t_element *pos) { - int idx = elem_idx_by_pos(pos); - if (idx == -1) - return; - remove_at_index(list, idx); + 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) { - elem *e = get_elem_by_tid(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_tid(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) { - int idx = elem_idx_by_tid(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); @@ -179,26 +253,40 @@ public: /** @Begin @Interface: Fetch - @Commit_point_set: Fetch_Point + @Commit_point_set: Fetch_Empty_Point | Fetch_Succ_Point @ID: fetch_id(__RET__) @Check: fetch_check(__RET__) @Action: - fetch(__RET__); + fetch(__RET__, __TID__); @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_Empty_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(); @@ -209,6 +297,13 @@ public: while ( (m_written.load(mo_acquire) & 0xFFFF) != wr ) { thrd_yield(); } + /** + @Begin + @Commit_point_define: true + @Potential_commit_point_label: Fetch_Potential_Point + @Label: Fetch_Succ_Point + @End + */ t_element * p = & ( m_array[ rd % t_size ] ); @@ -228,6 +323,12 @@ public: */ void read_consume() { m_read.fetch_add(1,mo_release); + /** + @Begin + @Commit_point_define_check: true + @Label: Consume_Point + @End + */ } //----------------------------------------------------- @@ -235,23 +336,37 @@ public: /** @Begin @Interface: Prepare - @Commit_point_set: Prepare_Point - @ID: prepare_id(__RET__) + @Commit_point_set: Prepare_Full_Point | Prepare_Succ_Point + @ID: prepare_id() @Check: - prepare_check(__RET__) + prepare_check(__RET__, __TID__) @Action: - prepare(__RET__); + prepare(__ID__, __RET__, __TID__); @End */ t_element * write_prepare() { unsigned int rdwr = m_rdwr.load(mo_acquire); + /** + @Begin + @Potential_commit_point_define: true + @Label: Prepare_Potential_Point + @End + */ unsigned int rd,wr; for(;;) { rd = (rdwr>>16) & 0xFFFF; wr = rdwr & 0xFFFF; - if ( wr == ((rd + t_size)&0xFFFF) ) // full + if ( wr == ((rd + t_size)&0xFFFF) ) { // full + /** + @Begin + @Commit_point_define: true + @Potential_commit_point_label: Prepare_Potential_Point + @Label: Prepare_Full_Point + @End + */ return NULL; + } if ( m_rdwr.compare_exchange_weak(rdwr,(rd<<16) | ((wr+1)&0xFFFF),mo_acq_rel) ) break; @@ -264,7 +379,13 @@ public: while ( (m_read.load(mo_acquire) & 0xFFFF) != rd ) { thrd_yield(); } - + /** + @Begin + @Commit_point_define: true + @Potential_commit_point_label: Prepare_Potential_Point + @Label: Prepare_Succ_Point + @End + */ t_element * p = & ( m_array[ wr % t_size ] ); @@ -285,9 +406,20 @@ public: void write_publish() { m_written.fetch_add(1,mo_release); + /** + @Begin + @Commit_point_define_check: true + @Label: Publish_Point + @End + */ } //----------------------------------------------------- }; +/** + @Begin + @Class_end + @End +*/ diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java index 30e185d..323ca98 100644 --- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java +++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java @@ -282,8 +282,8 @@ public class CodeGenerator { public static void main(String[] argvs) { String homeDir = Environment.HOME_DIRECTORY; File[] srcFiles = { - new File(homeDir - + "/benchmark/linuxrwlocks/linuxrwlocks.c") }; +// new File(homeDir +// + "/benchmark/linuxrwlocks/linuxrwlocks.c") }; // new File(homeDir // + // "/benchmark/cliffc-hashtable/simplified_cliffc_hashtable.h"), @@ -308,6 +308,9 @@ public class CodeGenerator { // new File(homeDir + "/benchmark/spsc-bugfix/eventcount.h"), // new File(homeDir + "/benchmark/spsc-bugfix/queue.h") }; + new File(homeDir + "/benchmark/mpmc-queue/mpmc-queue.h"), + new File(homeDir + "/benchmark/mpmc-queue/mpmc-queue.cc") }; + CodeGenerator gen = new CodeGenerator(srcFiles); gen.generateCode(); diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java index 47c2e9c..5f2ef35 100644 --- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java +++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java @@ -764,7 +764,10 @@ public class CodeVariables { newCode.add(STRUCT_NEW_DECLARE_DEFINE(ANNO_CP_DEFINE, structName)); String labelNum = Integer.toString(semantics.commitPointLabel2Num .get(construct.label)); + String potentialLabelNum = Integer.toString(semantics.commitPointLabel2Num + .get(construct.potentialCPLabel)); newCode.add(ASSIGN_TO_PTR(structName, "label_num", labelNum)); + newCode.add(ASSIGN_TO_PTR(structName, "potential_cp_label_num", potentialLabelNum)); newCode.add(STRUCT_NEW_DECLARE_DEFINE(SPEC_ANNOTATION, anno)); newCode.add(ASSIGN_TO_PTR(anno, "type", SPEC_ANNO_TYPE_CP_DEFINE)); newCode.add(ASSIGN_TO_PTR(anno, "annotation", structName)); diff --git a/src/edu/uci/eecs/specCompiler/specExtraction/ParserUtils.java b/src/edu/uci/eecs/specCompiler/specExtraction/ParserUtils.java index 4df375c..232f483 100644 --- a/src/edu/uci/eecs/specCompiler/specExtraction/ParserUtils.java +++ b/src/edu/uci/eecs/specCompiler/specExtraction/ParserUtils.java @@ -51,7 +51,7 @@ public class ParserUtils { ArrayList templateArgs = SpecParser.getTemplateArg(templateLine); templateStr = "<" + templateArgs.get(0).name; for (int i = 1; i < templateArgs.size(); i++) { - templateStr = templateStr + ", " + templateArgs.get(i); + templateStr = templateStr + ", " + templateArgs.get(i).name; } templateStr = templateStr + ">"; } catch (ParseException e) { -- 2.34.1