edits

diff --git a/benchmark/spsc-bugfix/eventcount.h b/benchmark/spsc-bugfix/eventcount.h
index b5d1c2fa25203f8918f056840e8a0b8c5c26c0c9..b22b6f2638f3bfd919915f5024319fc9418b21be 100644 (file)
--- a/benchmark/spsc-bugfix/eventcount.h
+++ b/benchmark/spsc-bugfix/eventcount.h
@@ -1,7 +1,7 @@
 #ifndef _EVENTCOUNT_H
 #define _EVENTCOUNT_H
 
-#include <unrelacy.h>
+//#include <unrelacy.h>
 #include <atomic>
 #include <mutex>
 #include <condition_variable>
@@ -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 67be1b7723489a3950f6c8585b44c2a59d8f66da..fa996181e9eaf5883955870c4411f2c840e734ec 100644 (file)
--- 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<node*> next;
-               rl::var<T> data;
+               //rl::var<T> data;
+               T data;
 
                node(T data = T())
                        : data(data)
@@ -148,14 +141,20 @@ private:
                }
        };
 
-       rl::var<node*> head;
-       rl::var<node*> tail;
+       //rl::var<node*> head;
+       //rl::var<node*> 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 06184fe5cbd2a3d07e6f8e4b626ac0746abbf162..a5b333b3b7cf1045974c43b57efdc3fa0a7e1464 100644 (file)
--- 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 (file)
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 (file)
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 fe4fd3bb85d6b00e45ace6c1dc9c83748f1f7360..492263f2f85801d39287d48de0820747f181f34e 100644 (file)
--- 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 469006b6ab8e4c94749d2f56833a9eb8d486c9e5..2653383326d5bc17719adbb09fc0085b37f772ff 100644 (file)
--- 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);