From: Brian Norris <banorris@uci.edu>
Date: Fri, 12 Oct 2012 17:44:58 +0000 (-0700)
Subject: spsc-queue: don't statically construct the queue
X-Git-Tag: pldi2013~30
X-Git-Url: http://demsky.eecs.uci.edu/git/?p=model-checker-benchmarks.git;a=commitdiff_plain;h=2b4ad7d1230c791d6ffaf3903ff7c475c5ce3e8b

spsc-queue: don't statically construct the queue

Our model-checker doesn't support constructors which perform
model-checking actions (e.g, atomic initialization) at load time (e.g.,
in a static execution of the constructor), since this happens before the
model-check object is created. Maybe we'll fix that in the future, but
for now, don't construct the queue at load time.
---

diff --git a/spsc-queue/spsc-queue.cc b/spsc-queue/spsc-queue.cc
index b689936..f8528a8 100644
--- a/spsc-queue/spsc-queue.cc
+++ b/spsc-queue/spsc-queue.cc
@@ -2,17 +2,17 @@
 
 #include "queue.h"
 
-spsc_queue<int> q;
+spsc_queue<int> *q;
 
 	void thread(unsigned thread_index)
 	{
 		if (0 == thread_index)
 		{
-			q.enqueue(11);
+			q->enqueue(11);
 		}
 		else
 		{
-			int d = q.dequeue();
+			int d = q->dequeue();
 			RL_ASSERT(11 == d);
 		}
 	}
@@ -20,9 +20,15 @@ spsc_queue<int> q;
 int user_main(int argc, char **argv)
 {
 	thrd_t A, B;
+
+	q = new spsc_queue<int>();
+
 	thrd_create(&A, (thrd_start_t)&thread, (void *)0);
 	thrd_create(&B, (thrd_start_t)&thread, (void *)1);
 	thrd_join(A);
 	thrd_join(B);
+
+	delete q;
+
 	return 0;
 }