X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=spsc-bugfix%2Fqueue-relacy.h;fp=spsc-bugfix%2Fqueue-relacy.h;h=71aac2a3992bd4be17499cb32297301648597d39;hb=991d0fdc0fb17f85d485c97dc2c5d8d57a98dad9;hp=0000000000000000000000000000000000000000;hpb=91db0c118d7135f69846bcedfb8a26c0afb44045;p=model-checker-benchmarks.git

diff --git a/spsc-bugfix/queue-relacy.h b/spsc-bugfix/queue-relacy.h
new file mode 100644
index 0000000..71aac2a
--- /dev/null
+++ b/spsc-bugfix/queue-relacy.h
@@ -0,0 +1,74 @@
+#include "eventcount-relacy.h"
+
+template<typename T>
+class spsc_queue
+{
+public:
+	spsc_queue()
+	{
+		node* n = new node ();
+		head($) = n;
+		tail($) = n;
+	}
+
+	~spsc_queue()
+	{
+		RL_ASSERT(head($) == tail($));
+		delete ((node*)head($));
+	}
+
+	void enqueue(T data)
+	{
+		node* n = new node (data);
+		head($)->next.store(n, std::memory_order_release);
+		head($) = n;
+		ec.signal_relaxed();
+	}
+
+	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;
+
+		node(T data = T())
+			: data(data)
+		{
+			next($) = 0;
+		}
+	};
+
+	rl::var<node*> head;
+	rl::var<node*> tail;
+
+	eventcount ec;
+
+	T try_dequeue()
+	{
+		node* t = tail($);
+		node* n = t->next.load(std::memory_order_acquire);
+		if (0 == n)
+			return 0;
+		T data = n->data($);
+		delete (t);
+		tail($) = n;
+		return data;
+	}
+};