From: Brian Norris <banorris@uci.edu>
Date: Tue, 6 Nov 2012 20:32:52 +0000 (-0800)
Subject: spsc-queue: add spsc-relacy build
X-Git-Tag: pldi2013~13
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker-benchmarks.git;a=commitdiff_plain;h=12f92a94d28b2a674f5ec2c0b112fa654734f19d

spsc-queue: add spsc-relacy build

Now we can test a version of spsc-queue using Relacy. There were some
small modifications necessary, so I duplicated the source code, renamed
with "-relacy" in the name.

To use it, you need to do something like the following, from the
spsc-queue directory:

  make RELACYPATH=/path-to-relacy
  ./spsc-relacy
---

diff --git a/spsc-queue/.gitignore b/spsc-queue/.gitignore
index b7d03a7..2485456 100644
--- a/spsc-queue/.gitignore
+++ b/spsc-queue/.gitignore
@@ -1 +1,2 @@
 /spsc-queue
+/spsc-relacy
diff --git a/spsc-queue/Makefile b/spsc-queue/Makefile
index 65a4686..6465176 100644
--- a/spsc-queue/Makefile
+++ b/spsc-queue/Makefile
@@ -1,11 +1,23 @@
 include ../benchmarks.mk
 
 TESTNAME = spsc-queue
+RELACYNAME = spsc-relacy
 
 all: $(TESTNAME)
 
 $(TESTNAME): $(TESTNAME).cc queue.h eventcount.h
 	$(CXX) -o $@ $< $(CPPFLAGS) $(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) *.o
+	rm -f $(TESTNAME) $(RELACYNAME) *.o
diff --git a/spsc-queue/eventcount-relacy.h b/spsc-queue/eventcount-relacy.h
new file mode 100644
index 0000000..9eadcf3
--- /dev/null
+++ b/spsc-queue/eventcount-relacy.h
@@ -0,0 +1,64 @@
+class eventcount
+{
+public:
+	eventcount() : waiters(0)
+	{
+		count($) = 0;
+	}
+
+	void signal_relaxed()
+	{
+		unsigned cmp = count.load(std::memory_order_relaxed);
+		signal_impl(cmp);
+	}
+
+	void signal()
+	{
+		unsigned cmp = count.fetch_add(0, std::memory_order_seq_cst);
+		signal_impl(cmp);
+	}
+
+	unsigned get()
+	{
+		unsigned cmp = count.fetch_or(0x80000000,
+std::memory_order_seq_cst);
+		return cmp & 0x7FFFFFFF;
+	}
+
+	void wait(unsigned cmp)
+	{
+		unsigned ec = count.load(std::memory_order_seq_cst);
+		if (cmp == (ec & 0x7FFFFFFF))
+		{
+			guard.lock($);
+			ec = count.load(std::memory_order_seq_cst);
+			if (cmp == (ec & 0x7FFFFFFF))
+			{
+				waiters($) += 1;
+				cv.wait(guard, $);
+			}
+			guard.unlock($);
+		}
+	}
+
+private:
+	std::atomic<unsigned> count;
+	rl::var<unsigned> waiters;
+	std::mutex guard;
+	std::condition_variable cv;
+
+	void signal_impl(unsigned cmp)
+	{
+		if (cmp & 0x80000000)
+		{
+			guard.lock($);
+			while (false == count.compare_exchange_weak(cmp,
+				(cmp + 1) & 0x7FFFFFFF, std::memory_order_relaxed));
+			unsigned w = waiters($);
+			waiters($) = 0;
+			guard.unlock($);
+			if (w)
+				cv.notify_all($);
+		}
+	}
+};
diff --git a/spsc-queue/queue-relacy.h b/spsc-queue/queue-relacy.h
new file mode 100644
index 0000000..71aac2a
--- /dev/null
+++ b/spsc-queue/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;
+	}
+};
diff --git a/spsc-queue/spsc-relacy.cc b/spsc-queue/spsc-relacy.cc
new file mode 100644
index 0000000..37ed989
--- /dev/null
+++ b/spsc-queue/spsc-relacy.cc
@@ -0,0 +1,27 @@
+#include <relacy/relacy_std.hpp>
+
+#include "queue-relacy.h"
+
+struct spsc_queue_test : rl::test_suite<spsc_queue_test, 2>
+{
+	spsc_queue<int> q;
+
+	void thread(unsigned thread_index)
+	{
+		if (0 == thread_index)
+		{
+			q.enqueue(11);
+		}
+		else
+		{
+			int d = q.dequeue();
+			RL_ASSERT(11 == d);
+		}
+	}
+};
+
+
+int main()
+{
+	rl::simulate<spsc_queue_test>();
+}