spsc-bugfix: fix deadlocked signalling bug
[model-checker-benchmarks.git] / spsc-queue / 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::simulate<spsc_queue_test>();
27 }