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     // XXX-injection-#1: Weaken the parameter "memory_order_release" to
   8     // "memory_order_relaxed", run "make" to recompile, and then run:
   9     // "./run.sh ./spsc-bugfix/testcase1 -m2 -y -u3 -tSPEC"
  10         /**********    Detected Correctness    **********/
  11         //head($)->next.store(n, std::memory_order_release);
  12         head->next.store(n, std::memory_order_release);
  13         /** @OPDefine: true */
  14         head = n;
  15         ec.signal();
  16 }
  17
  18
  19 template<typename T>
  20 T spsc_queue<T>::dequeue()
  21 {
  22         T data = try_dequeue();
  23         while (0 == data)
  24         {
  25                 int cmp = ec.get();
  26                 data = try_dequeue();
  27                 if (data)
  28                         break;
  29                 ec.wait(cmp);
  30                 data = try_dequeue();
  31                 if (data)
  32                         break;
  33         }
  34         return data;
  35 }
  36
  37 template<typename T>
  38 T spsc_queue<T>::try_dequeue()
  39 {
  40         //node* t = tail($);
  41         node* t = tail;
  42     // XXX-injection-#2: Weaken the parameter "memory_order_acquire" to
  43     // "memory_order_relaxed", run "make" to recompile, and then run:
  44     // "./run.sh ./spsc-bugfix/testcase1 -m2 -y -u3 -tSPEC"
  45         /**********    Detected Correctness    **********/
  46         node* n = t->next.load(std::memory_order_acquire);
  47         /** @OPClearDefine: true */
  48         if (0 == n)
  49                 return 0;
  50         //T data = n->data($);
  51         T data = n->data;
  52         delete (t);
  53         tail = n;
  54         return data;
  55 }
  56
  57 /** @DeclareState: IntList *q; */
  58
  59 /** @Transition: STATE(q)->push_back(data); */
  60 void enqueue(spsc_queue<int> *q, int data) {
  61         q->enqueue(data);
  62 }
  63
  64 /** @PreCondition: return STATE(q)->empty() ? !C_RET : STATE(q)->front() == C_RET;
  65         @Transition: if (!C_RET) STATE(q)->pop_front(); */
  66 int dequeue(spsc_queue<int> *q) {
  67         return q->dequeue();
  68 }