blocking-mpmc-example/example.txt

   1 class Queue {
   2 /** @DeclareState: IntList *q;
   3 @Commutativity:enq<->deq(true)
   4 @Commutativity:deq<->deq(!M1->RET||!M2->RET) */
   5 public: atomic<Node*> tail, head;
   6 Queue() { tail = head = new Node(); }
   7 /** @Transition: STATE(q)->push_back(val); */
   8 void Queue::enq(unsigned int val) {
   9   Node *n = new Node(val);
  10   while(true) {
  11     Node *t = tail.load(acquire);
  12     Node *next = t->next.load(relaxed);
  13     if(next) continue;
  14     if(t->next.CAS(next, n, relaxed)) {
  15           /** @OPDefine: true */
  16       tail.store(n, release);
  17       return;
  18     }
  19   }
  20 }
  21 /**@PreCondition:
  22 return RET ? !STATE(q)->empty()
  23         && STATE(q)->front() == RET : true;
  24 @Transition: if (RET) {
  25         if (STATE(q)->empty()) return false;
  26         STATE(q)->pop_front();
  27 } */
  28 unsigned int Queue::deq() {
  29   while(true) {
  30     Node *h = head.load(acquire);
  31     Node *t = tail.load(acquire);
  32     Node *next = h->next.load(relaxed);
  33         /** @OPClearDefine: true */
  34     if(h == t) return 0;
  35     if(head.CAS(h, next, release))
  36           return next->data;
  37   }
  38 }
  39 };