spsc-queue: don't statically construct the queue
authorBrian Norris <banorris@uci.edu>
Fri, 12 Oct 2012 17:44:58 +0000 (10:44 -0700)
committerBrian Norris <banorris@uci.edu>
Fri, 12 Oct 2012 17:44:58 +0000 (10:44 -0700)
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.

spsc-queue/spsc-queue.cc

index b689936..f8528a8 100644 (file)
@@ -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;
 }