edits: add comments to demonstrate the found bugs and bug injections
[model-checker-benchmarks.git] / spsc-bugfix / queue.h
1 #ifndef _SPSC_QUEUE_H
2 #define _SPSC_QUEUE_H
3
4 #include <unrelacy.h>
5 #include <atomic>
6
7 #include "eventcount.h"
8
9 template<typename T>
10 class spsc_queue
11 {
12 public:
13         spsc_queue()
14         {
15                 node* n = new node ();
16                 head = n;
17                 tail = n;
18         }
19
20         ~spsc_queue()
21         {
22                 RL_ASSERT(head == tail);
23                 //delete ((node*)head($));
24                 delete ((node*)head);
25         }
26
27         void enqueue(T data);
28
29         T dequeue();
30
31 private:
32         struct node
33         {
34                 std::atomic<node*> next;
35                 //rl::var<T> data;
36                 T data;
37
38                 node(T data = T())
39                         : data(data)
40                 {
41                         next = 0;
42                 }
43         };
44
45         /* Use normal memory access
46         rl::var<node*> head;
47         rl::var<node*> tail;
48         */
49         node *head;
50         node *tail;
51
52         eventcount ec;
53
54         T try_dequeue();
55 };
56
57 // C Interface
58 void enqueue(spsc_queue<int> *q, int data);
59 int dequeue(spsc_queue<int> *q);
60
61 #endif