From 2b4ad7d1230c791d6ffaf3903ff7c475c5ce3e8b Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Fri, 12 Oct 2012 10:44:58 -0700 Subject: [PATCH] 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. --- spsc-queue/spsc-queue.cc | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) 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 q; +spsc_queue *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 q; int user_main(int argc, char **argv) { thrd_t A, B; + + q = new spsc_queue(); + 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; } -- 2.34.1