X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=benchmark%2Fspsc-bugfix%2Fqueue.h;fp=benchmark%2Fspsc-bugfix%2Fqueue.h;h=0000000000000000000000000000000000000000;hb=d2ea20dfe024fdf297e6776d56bc9066cb040f38;hp=fa996181e9eaf5883955870c4411f2c840e734ec;hpb=facdc9fd49c05b968c55c54deb21ba5d3a673f52;p=cdsspec-compiler.git

diff --git a/benchmark/spsc-bugfix/queue.h b/benchmark/spsc-bugfix/queue.h
deleted file mode 100644
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