ms-queue: remove more externs and unintended shared data
[model-checker-benchmarks.git] / spsc-bugfix / spsc-relacy.cc
1 #include <relacy/relacy_std.hpp>
2
3 #include "queue-relacy.h"
4
5 struct spsc_queue_test : rl::test_suite<spsc_queue_test, 2>
6 {
7         spsc_queue<int> q;
8
9         void thread(unsigned thread_index)
10         {
11                 if (0 == thread_index)
12                 {
13                         q.enqueue(11);
14                 }
15                 else
16                 {
17                         int d = q.dequeue();
18                         RL_ASSERT(11 == d);
19                 }
20         }
21 };
22
23
24 int main()
25 {
26         rl::test_params params;
27         params.search_type = rl::fair_full_search_scheduler_type;
28         rl::simulate<spsc_queue_test>(params);
29 }