edits

[cdsspec-compiler.git] / benchmark / spsc-bugfix / queue.h

diff --git a/benchmark/spsc-bugfix/queue.h b/benchmark/spsc-bugfix/queue.h
index 76c520036e7dc3b37aaf436e75014c987dfa6397..fa996181e9eaf5883955870c4411f2c840e734ec 100644 (file)
--- a/benchmark/spsc-bugfix/queue.h
+++ b/benchmark/spsc-bugfix/queue.h
@@ -9,6 +9,7 @@
 #include <cdsannotate.h>
 #include <specannotation.h>
 #include <model_memory.h>
+#include "common.h" 
 
 #include "eventcount.h"
 
@@ -40,8 +41,9 @@ public:
 
        ~spsc_queue()
        {
-               RL_ASSERT(head == tail);
-               delete ((node*)head($));
+               //RL_ASSERT(head == tail);
+               //delete ((node*)head($));
+               delete ((node*)head);
        }
 
        /**
@@ -50,35 +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)
+               @ID: data
                @Action:
-                       tag_elem_t *elem = new_tag_elem(__ID__, data);
-                       push_back(__queue, elem);
+                       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,12 +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()
@@ -140,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)
@@ -149,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
@@ -166,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;