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 }