85903d08907a9fe213111b1827c81f7c50899c90
[model-checker-benchmarks.git] / spsc-bugfix / queue.cc
1 #include "queue.h"
2
3 template<typename T>
4 void spsc_queue<T>::enqueue(T data)
5 {
6         node* n = new node (data);
7         /**********    Detected Correctness    **********/
8         //head($)->next.store(n, std::memory_order_release);
9         head->next.store(n, std::memory_order_release);
10         /** @OPDefine: true */
11         head = n;
12         ec.signal();
13 }
14
15
16 template<typename T>
17 T spsc_queue<T>::dequeue()
18 {
19         T data = try_dequeue();
20         while (0 == data)
21         {
22                 int cmp = ec.get();
23                 data = try_dequeue();
24                 if (data)
25                         break;
26                 ec.wait(cmp);
27                 data = try_dequeue();
28                 if (data)
29                         break;
30         }
31         return data;
32 }
33
34 template<typename T>
35 T spsc_queue<T>::try_dequeue()
36 {
37         //node* t = tail($);
38         node* t = tail;
39         /**********    Detected Correctness    **********/
40         node* n = t->next.load(std::memory_order_acquire);
41         /** @OPClearDefine: true */
42         if (0 == n)
43                 return 0;
44         //T data = n->data($);
45         T data = n->data;
46         delete (t);
47         tail = n;
48         return data;
49 }
50
51 /** @DeclareState: IntList *q; */
52
53 /** @Transition: STATE(q)->push_back(data); */
54 void enqueue(spsc_queue<int> *q, int data) {
55         q->enqueue(data);
56 }
57
58 /** @PreCondition: return STATE(q)->empty() ? !C_RET : STATE(q)->front() == C_RET;
59         @Transition: if (!C_RET) STATE(q)->pop_front(); */
60 int dequeue(spsc_queue<int> *q) {
61         return q->dequeue();
62 }