From: Peizhao Ou Date: Thu, 16 Jan 2014 07:49:15 +0000 (-0800) Subject: add spsc X-Git-Url: http://plrg.eecs.uci.edu/git/?p=cdsspec-compiler.git;a=commitdiff_plain;h=b779fde36fd5836709293c63945964d8c42cee1f add spsc --- diff --git a/benchmark/ms-queue/my_queue.h b/benchmark/ms-queue/my_queue.h index 883a13d..fa64d60 100644 --- a/benchmark/ms-queue/my_queue.h +++ b/benchmark/ms-queue/my_queue.h @@ -80,7 +80,7 @@ void init_queue(queue_t *q, int num_threads); @Begin @Interface: Enqueue @Commit_point_set: Enqueue_Success_Point - @ID: get_and_inc(tag); + @ID: get_and_inc(tag) @Action: # __ID__ is an internal macro that refers to the id of the current # interface call diff --git a/benchmark/spsc-bugfix/eventcount.h b/benchmark/spsc-bugfix/eventcount.h index aec3e8c..b5d1c2f 100644 --- a/benchmark/spsc-bugfix/eventcount.h +++ b/benchmark/spsc-bugfix/eventcount.h @@ -1,3 +1,6 @@ +#ifndef _EVENTCOUNT_H +#define _EVENTCOUNT_H + #include #include #include @@ -67,3 +70,5 @@ private: } } }; + +#endif diff --git a/benchmark/spsc-bugfix/queue.h b/benchmark/spsc-bugfix/queue.h index 802d455..8ff765e 100644 --- a/benchmark/spsc-bugfix/queue.h +++ b/benchmark/spsc-bugfix/queue.h @@ -1,34 +1,32 @@ +#ifndef _QUEUE_H +#define _QUEUE_H + #include #include #include "eventcount.h" +/** + @Begin + @Class_begin + @End +*/ template class spsc_queue { - /** - @Begin - @Global_define: - typedef struct tag_elem { - Tag id; - T data; - } tag_elem_t; - - Tag tag; - spec_queue __queue; - - static bool _is_elem_equals(void *ptr1, void *ptr2) { - // ... - // return if the elements pointed to are equal - } - - @Happens-before: - Enqueue -> Dequeue - @End - **/ + public: + + spsc_queue() { + + /** + @Begin + @Entry_point + @End + */ + node* n = new node (); head = n; tail = n; @@ -39,15 +37,54 @@ public: RL_ASSERT(head == tail); delete ((node*)head($)); } + + /** + @Begin + @Options: + LANG = CPP; + CLASS = spsc_queue; + @Global_define: + @DeclareStruct: + typedef struct tag_elem { + call_id_t id; + T data; + } tag_elem_t; + + @DeclareVar: + spec_list *__queue; + id_tag_t *tag; + @InitVar: + __queue = new_spec_list(); + tag = new_id_tag(); + @DefineFunc: + tag_elem_t* new_tag_elem(call_id_t id, T data) { + tag_elem_t *e = (tag_elem_t*) MODEL_MALLOC(sizeof(tag_elem_t)); + e->id = id; + e->data = data; + return e; + } + @DefineFunc: + call_id_t get_id(void *wrapper) { + return ((tag_elem_t*) wrapper)->id; + } + @DefineFunc: + unsigned int get_data(void *wrapper) { + return ((tag_elem_t*) wrapper)->data; + } + @Happens_before: + Enqueue -> Dequeue + @End + */ + /** @Begin - @Commit_point_set: - Enqueue = Enqueue_Success_Point - @ID: tag.current() + @Interface: Enqueue + @Commit_point_set: Enqueue_Point + @ID: get_and_inc(tag) @Action: - __queue.enqueue(tag_elem_t(tag.current(), node(data)); - tag.next(); + tag_elem_t *elem = new_tag_elem(__ID__, data); + push_back(__queue, elem); @End */ void enqueue(T data) @@ -56,22 +93,24 @@ public: head($)->next.store(n, std::memory_order_release); /** @Begin - @Commit_point_define: true - @Label: Enqueue_Success_Point + @Commit_point_define_check: true + @Label: Enqueue_Point @End */ head = n; // #Mark delete this ec.signal(); } - /** @Begin - @Commit_point_set: - Dequeue = Try_Dequeue_Success_Point - @ID: __queue.peak().tag - @Check: __queue.size() > 0 && _is_elem_equals(&RET, &__queue.peek().data) - @Action: __queue.dequeue(); + @Interface: Dequeue + @Commit_point_set: Dequeue_Point + @ID: get_id(front(__queue)) + @Action: + T _Old_Val = get_data(front(__queue)); + pop_front(__queue); + @Post_check: + _Old_Val == __RET__ @End */ T dequeue() @@ -115,8 +154,8 @@ private: node* n = t->next.load(std::memory_order_acquire); /** @Begin - @Commit_point_define: ATOMIC_RET != NULL - @Label: Try_Dequeue_Success_Point + @Commit_point_define_check: n != 0 + @Label: Dequeue_Point @End */ if (0 == n) @@ -127,3 +166,10 @@ private: return data; } }; +/** + @Begin + @Class_end + @End +*/ + +#endif diff --git a/grammer/spec_compiler.jj b/grammer/spec_compiler.jj index 150ad94..a58db93 100644 --- a/grammer/spec_compiler.jj +++ b/grammer/spec_compiler.jj @@ -414,6 +414,8 @@ SKIP : { | /* C/C++ only token*/ +| + | | @@ -766,7 +768,7 @@ ArrayList C_CPP_CODE(ArrayList headers) : t = | t = | t = | t = | t = | t = | t = | - t = | t = | t = | t = | t = | t = | t = | t = | + t = | t = | t = | t = | t = | t = | t = | t = | t = | t = | t = | t = | t = | t = | t = | (t = { if (inTemplate) newLine = true; }) | diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java index 802dd3e..7c45488 100644 --- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java +++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java @@ -301,8 +301,13 @@ public class CodeGenerator { // new File(homeDir + // "/benchmark/chase-lev-deque-bugfix/deque.h") }; - new File(homeDir + "/benchmark/mcs-lock/mcs-lock.cc"), - new File(homeDir + "/benchmark/mcs-lock/mcs-lock.h") }; +// new File(homeDir + "/benchmark/mcs-lock/mcs-lock.cc"), +// new File(homeDir + "/benchmark/mcs-lock/mcs-lock.h") }; + + new File(homeDir + "/benchmark/spsc-bugfix/spsc-queue.cc"), + new File(homeDir + "/benchmark/spsc-bugfix/eventcount.h"), + new File(homeDir + "/benchmark/spsc-bugfix/queue.h") }; + 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 0953eef..ea1cb66 100644 --- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java +++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java @@ -269,7 +269,7 @@ public class CodeVariables { headers.add(HEADER_MODELMEMORY); headers.add(HEADER_STDINT); headers.add(HEADER_CDSANNOTATE); - headers.add(HEADER_COMMON); +// headers.add(HEADER_COMMON); headers.add(HEADER_SPEC_LIB); headers.add(HEADER_SPECANNOTATION); return headers; @@ -449,7 +449,7 @@ public class CodeVariables { newCode.add(templateDecl); newCode.add(DECLARE("void**", varPrefix + "func_ptr_table")); newCode.add(templateDecl); - newCode.add(DECLARE("void**", varPrefix + "hb_init_table")); + newCode.add(DECLARE("anno_hb_init**", varPrefix + "hb_init_table")); for (int i = 0; i < construct.code.declareVar.size(); i++) { VariableDeclaration varDecl = construct.code.declareVar.get(i); newCode.add(templateDecl);