From 7919b41aeee6c8d5f572299f80f2e91d389ae164 Mon Sep 17 00:00:00 2001 From: Peizhao Ou Date: Tue, 17 Nov 2015 23:30:59 -0800 Subject: [PATCH] edits --- benchmark/spsc-bugfix/eventcount.h | 4 +- benchmark/spsc-bugfix/queue.h | 82 +++++++++---------- output/Makefile | 3 +- output/mpmc-queue/Makefile | 22 +++++ output/spsc-bugfix/Makefile | 23 ++++++ .../codeGenerator/CodeGenerator.java | 21 ++--- .../codeGenerator/CodeVariables.java | 1 + 7 files changed, 103 insertions(+), 53 deletions(-) create mode 100644 output/mpmc-queue/Makefile create mode 100644 output/spsc-bugfix/Makefile diff --git a/benchmark/spsc-bugfix/eventcount.h b/benchmark/spsc-bugfix/eventcount.h index b5d1c2f..b22b6f2 100644 --- a/benchmark/spsc-bugfix/eventcount.h +++ b/benchmark/spsc-bugfix/eventcount.h @@ -1,7 +1,7 @@ #ifndef _EVENTCOUNT_H #define _EVENTCOUNT_H -#include +//#include #include #include #include @@ -22,6 +22,8 @@ public: void signal() { + // We might be able to use release here because it basically only needs + // to synchronize with the get() unsigned cmp = count.fetch_add(0, std::memory_order_seq_cst); signal_impl(cmp); } diff --git a/benchmark/spsc-bugfix/queue.h b/benchmark/spsc-bugfix/queue.h index 67be1b7..fa99618 100644 --- a/benchmark/spsc-bugfix/queue.h +++ b/benchmark/spsc-bugfix/queue.h @@ -42,7 +42,8 @@ public: ~spsc_queue() { //RL_ASSERT(head == tail); - delete ((node*)head($)); + //delete ((node*)head($)); + delete ((node*)head); } /** @@ -51,34 +52,18 @@ public: 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; + IntegerList *__queue; @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 + __queue = createIntegerList(); + @Finalize: + if (__queue) + destroyIntegerList(__queue); + return true; + @Happens_before: Enqueue -> Dequeue + @Commutativity: Enqueue <-> Dequeue: true + @Commutativity: Dequeue <-> Dequeue: !_Method1.__RET__ || !_Method2.__RET__ + @End */ @@ -87,16 +72,18 @@ public: @Begin @Interface: Enqueue @Commit_point_set: Enqueue_Point - @ID: get_and_inc(tag) - @Action: push_back(__queue, new_tag_elem(__ID__, data)); - //tag_elem_t *elem = new_tag_elem(__ID__, data); - //push_back(__queue, elem); + @ID: data + @Action: + push_back(__queue, data); + //model_print("Enqueue: val=%d\n", val); @End */ void enqueue(T data) { node* n = new node (data); - head($)->next.store(n, std::memory_order_release); + /********** DR & SPEC (sequential) **********/ + //head($)->next.store(n, std::memory_order_release); + head->next.store(n, std::memory_order_release); /** @Begin @Commit_point_define_check: true @@ -111,11 +98,16 @@ public: @Begin @Interface: Dequeue @Commit_point_set: Dequeue_Point - @ID: get_id(front(__queue)) + @ID: __RET__ ? __RET__ : 0 @Action: - T _Old_Val = get_data(front(__queue)); - pop_front(__queue); - @Post_check: _Old_Val == __RET__ + int elem = 0; + if (__RET__) { + elem = front(__queue); + pop_front(__queue); + } + //model_print("Dequeue: __RET__=%d, retVal=%d, elem=%d, \n", __RET__, *retVal, elem); + //model_print("Result: %d\n", __RET__ ? *retVal == elem : true); + @Post_check: __RET__ ? __RET__ == elem : true @End */ T dequeue() @@ -139,7 +131,8 @@ private: struct node { std::atomic next; - rl::var data; + //rl::var data; + T data; node(T data = T()) : data(data) @@ -148,14 +141,20 @@ private: } }; - rl::var head; - rl::var tail; + //rl::var head; + //rl::var tail; + node *head; + node *tail; + + eventcount ec; T try_dequeue() { - node* t = tail($); + //node* t = tail($); + node *t = tail; + /********** DR & SPEC (sequential) **********/ node* n = t->next.load(std::memory_order_acquire); /** @Begin @@ -165,7 +164,8 @@ private: */ if (0 == n) return 0; - T data = n->data($); + //T data = n->data($); + T data = n->data; delete (t); tail = n; return data; diff --git a/output/Makefile b/output/Makefile index 06184fe..a5b333b 100644 --- a/output/Makefile +++ b/output/Makefile @@ -3,7 +3,8 @@ concurrent-hashmap seqlock spsc-example spsc-queue-scfence \ treiber-stack -DIRS := ms-queue concurrent-hashmap linuxrwlocks mcs-lock read-copy-update chase-lev-deque-bugfix +DIRS := ms-queue concurrent-hashmap linuxrwlocks mcs-lock read-copy-update \ + chase-lev-deque-bugfix spsc-bugfix mpmc-queue .PHONY: $(DIRS) diff --git a/output/mpmc-queue/Makefile b/output/mpmc-queue/Makefile new file mode 100644 index 0000000..8d9ad1e --- /dev/null +++ b/output/mpmc-queue/Makefile @@ -0,0 +1,22 @@ +include ../benchmarks.mk + +TESTNAME = mpmc-queue +TESTS = mpmc-queue mpmc-1r2w mpmc-2r1w mpmc-queue-rdwr +TESTS += mpmc-queue-noinit mpmc-1r2w-noinit mpmc-2r1w-noinit mpmc-rdwr-noinit + +all: $(TESTS) + +mpmc-queue: CPPFLAGS += -DCONFIG_MPMC_READERS=2 -DCONFIG_MPMC_WRITERS=2 +mpmc-queue-rdwr: CPPFLAGS += -DCONFIG_MPMC_READERS=0 -DCONFIG_MPMC_WRITERS=0 -DCONFIG_MPMC_RDWR=2 +mpmc-1r2w: CPPFLAGS += -DCONFIG_MPMC_READERS=1 -DCONFIG_MPMC_WRITERS=2 +mpmc-2r1w: CPPFLAGS += -DCONFIG_MPMC_READERS=2 -DCONFIG_MPMC_WRITERS=1 +mpmc-queue-noinit: CPPFLAGS += -DCONFIG_MPMC_READERS=2 -DCONFIG_MPMC_WRITERS=2 -DCONFIG_MPMC_NO_INITIAL_ELEMENT +mpmc-1r2w-noinit: CPPFLAGS += -DCONFIG_MPMC_READERS=1 -DCONFIG_MPMC_WRITERS=2 -DCONFIG_MPMC_NO_INITIAL_ELEMENT +mpmc-2r1w-noinit: CPPFLAGS += -DCONFIG_MPMC_READERS=2 -DCONFIG_MPMC_WRITERS=1 -DCONFIG_MPMC_NO_INITIAL_ELEMENT +mpmc-rdwr-noinit: CPPFLAGS += -DCONFIG_MPMC_READERS=0 -DCONFIG_MPMC_WRITERS=0 -DCONFIG_MPMC_RDWR=2 -DCONFIG_MPMC_NO_INITIAL_ELEMENT + +$(TESTS): $(TESTNAME).cc $(TESTNAME).h + $(CXX) -o $@ $< $(CXXFLAGS) $(LDFLAGS) + +clean: + rm -f $(TESTS) *.o diff --git a/output/spsc-bugfix/Makefile b/output/spsc-bugfix/Makefile new file mode 100644 index 0000000..33b9d01 --- /dev/null +++ b/output/spsc-bugfix/Makefile @@ -0,0 +1,23 @@ +include ../benchmarks.mk + +TESTNAME = spsc-queue +RELACYNAME = spsc-relacy + +all: $(TESTNAME) + +$(TESTNAME): $(TESTNAME).cc queue.h eventcount.h + $(CXX) -o $@ $< $(CXXFLAGS) $(LDFLAGS) + +relacy: $(RELACYNAME) + +$(RELACYNAME): spsc-relacy.cc queue-relacy.h eventcount-relacy.h +ifdef RELACYPATH + $(CXX) -o $(RELACYNAME) spsc-relacy.cc -I$(RELACYPATH) -Wno-deprecated +else + @echo "Please define RELACYPATH" + @echo " e.g., make RELACYPATH=/path-to-relacy" + @exit 1 +endif + +clean: + rm -f $(TESTNAME) $(RELACYNAME) *.o diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java index fe4fd3b..492263f 100644 --- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java +++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java @@ -329,19 +329,20 @@ public class CodeGenerator { new File(homeDir + "/benchmark/mcs-lock/mcs-lock.cc"), new File(homeDir + "/benchmark/mcs-lock/mcs-lock.h") }; // -// File[] srcSPSCQueue = { -// 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") }; + File[] srcSPSCQueue = { + 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") }; + + File[] srcMPMCQueue = { + new File(homeDir + "/benchmark/mpmc-queue/mpmc-queue.h"), + new File(homeDir + "/benchmark/mpmc-queue/mpmc-queue.cc") }; // -// File[] srcMPMCQueue = { -// new File(homeDir + "/benchmark/mpmc-queue/mpmc-queue.h"), -// new File(homeDir + "/benchmark/mpmc-queue/mpmc-queue.cc") }; -// -// File[][] sources = { srcLinuxRWLocks, srcMSQueue, srcRCU, +// File[][] sources = {srcLinuxRWLock1 , srcMSQueue, srcRCU, // srcDeque, srcMCSLock, srcSPSCQueue, srcMPMCQueue, srcHashtable }; - File[][] sources = {srcDeque}; +// File[][] sources = {srcDeque, srcLinuxRWLock1, srcLinuxRWLock2, srcLinuxRWLock3, srcMCSLock, srcHashtable, srcRCU}; + File[][] sources = {srcMPMCQueue}; // Compile all the benchmarks for (int i = 0; i < sources.length; i++) { CodeGenerator gen = new CodeGenerator(sources[i]); diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java index 469006b..2653383 100644 --- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java +++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java @@ -571,6 +571,7 @@ public class CodeVariables { newCode.add(DECLARE("void**", varPrefix + "func_ptr_table")); newCode.add(templateDecl); newCode.add(DECLARE("hb_rule**", varPrefix + "hb_rule_table")); + newCode.add(templateDecl); newCode.add(DECLARE("commutativity_rule**", varPrefix + "commutativity_rule_table")); for (int i = 0; i < construct.code.declareVar.size(); i++) { VariableDeclaration varDecl = construct.code.declareVar.get(i); -- 2.34.1