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.
#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);
}
}
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;
}