blocking-mpmc-example/queue.cc

   1 #include "queue.h"
   2
   3 // Make them C-callable interfaces
   4
   5 /** @DeclareState: IntList *q;
   6 @Commutativity: enq <-> deq (true)
   7 @Commutativity: deq <-> deq (M1->C_RET!=-1||M2->C_RET!=-1) */
   8
   9 void Queue::enq(int val) {
  10   Node *n = new Node(val);
  11   while(true) {
  12     Node *t = tail.load(acquire);
  13     Node *next = t->next.load(relaxed);
  14     if(next) continue;
  15     if(t->next.CAS(next, n, relaxed)) {
  16           /** @OPDefine: true */
  17       tail.store(n, release);
  18       return;
  19     }
  20   }
  21 }
  22 int Queue::deq() {
  23   while(true) {
  24     Node *h = head.load(acquire);
  25     Node *t = tail.load(acquire);
  26     Node *next = h->next.load(relaxed);
  27         /** @OPClearDefine: true */
  28     if(h == t) return -1;
  29     if(head.CAS(h, next, release))
  30           return next->data;
  31   }
  32 }
  33
  34 /** @Transition: STATE(q)->push_back(val); */
  35 void enq(Queue *q, int val) {
  36         q->enq(val);
  37 }
  38
  39 /** @Transition:
  40 S_RET = STATE(q)->empty() ? -1 : STATE(q)->front();
  41 if (S_RET != -1)
  42     STATE(q)->pop_front();
  43 @PostCondition:
  44     return C_RET == -1 ? true : C_RET == S_RET;
  45 @JustifyingPostcondition: if (C_RET == -1)
  46     return S_RET == -1; */
  47 int deq(Queue *q) {
  48         return q->deq();
  49 }