fixed command line

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

diff --git a/benchmark/spsc-bugfix/queue.h b/benchmark/spsc-bugfix/queue.h
deleted file mode 100644 (file)
index fa99618..0000000
--- a/benchmark/spsc-bugfix/queue.h
+++ /dev/null
@@ -1,180 +0,0 @@
-#ifndef _QUEUE_H
-#define _QUEUE_H
-
-#include <unrelacy.h>
-#include <atomic>
-
-#include <spec_lib.h>
-#include <stdlib.h>
-#include <cdsannotate.h>
-#include <specannotation.h>
-#include <model_memory.h>
-#include "common.h" 
-
-#include "eventcount.h"
-
-/**
-       @Begin
-       @Class_begin
-       @End
-*/
-template<typename T>
-class spsc_queue
-{
-       
-public:
-
-       
-       spsc_queue()
-       {
-
-               /**
-                       @Begin
-                       @Entry_point
-                       @End
-               */
-
-               node* n = new node ();
-               head = n;
-               tail = n;
-       }
-
-       ~spsc_queue()
-       {
-               //RL_ASSERT(head == tail);
-               //delete ((node*)head($));
-               delete ((node*)head);
-       }
-
-       /**
-               @Begin
-               @Options:
-                       LANG = CPP;
-                       CLASS = spsc_queue;
-               @Global_define:
-               @DeclareVar:
-                       IntegerList *__queue;
-               @InitVar:
-                       __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
-       */
-
-       
-       /**
-               @Begin
-               @Interface: Enqueue
-               @Commit_point_set: Enqueue_Point
-               @ID: data
-               @Action:
-                       push_back(__queue, data);
-                       //model_print("Enqueue: val=%d\n", val);
-               @End
-       */
-       void enqueue(T data)
-       {
-               node* n = new node (data);
-               /********** 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
-                       @Label: Enqueue_Point
-                       @End
-               */
-               head = n;
-               // #Mark delete this
-               ec.signal();
-       }
-       /**
-               @Begin
-               @Interface: Dequeue
-               @Commit_point_set: Dequeue_Point
-               @ID: __RET__ ? __RET__ : 0
-               @Action:
-                       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()
-       {
-               T data = try_dequeue();
-               while (0 == data)
-               {
-                       int cmp = ec.get();
-                       data = try_dequeue();
-                       if (data)
-                               break;
-                       ec.wait(cmp);
-                       data = try_dequeue();
-                       if (data)
-                               break;
-               }
-               return data;
-       }
-
-private:
-       struct node
-       {
-               std::atomic<node*> next;
-               //rl::var<T> data;
-               T data;
-
-               node(T data = T())
-                       : data(data)
-               {
-                       next = 0;
-               }
-       };
-
-       //rl::var<node*> head;
-       //rl::var<node*> tail;
-       node *head;
-       node *tail;
-
-
-
-       eventcount ec;
-
-       T try_dequeue()
-       {
-               //node* t = tail($);
-               node *t = tail;
-               /********** DR & SPEC (sequential) **********/
-               node* n = t->next.load(std::memory_order_acquire);
-               /**
-                       @Begin
-                       @Commit_point_define_check: n != 0
-                       @Label: Dequeue_Point
-                       @End
-               */
-               if (0 == n)
-                       return 0;
-               //T data = n->data($);
-               T data = n->data;
-               delete (t);
-               tail = n;
-               return data;
-       }
-};
-/**
-       @Begin
-       @Class_end
-       @End
-*/
-
-#endif