spsc-example/spsc-queue.cc

   1 #include <threads.h>
   2 #include <atomic>
   3
   4 #include "wildcard.h"
   5
   6 using namespace std;
   7
   8 struct node {
   9         node(int d) {
  10                 data.store(d, memory_order_normal);
  11                 next.store(0, wildcard(1));
  12         }
  13         atomic<node*> next;
  14         atomic_int data;
  15 };
  16
  17 class spsc_queue {
  18         atomic<node*> head, tail;/*@ \label{line:spscBegin} @*/
  19         public:
  20         spsc_queue() {
  21                 head = tail = new node(-1);
  22         }
  23         void enqueue(int val) {
  24                 node* n = new node(val);
  25                 node *h = head.load(wildcard(2));
  26                 h->next.store(n, wildcard(3));/*@ \label{line:spscRelease} @*/
  27                 head.store(n, wildcard(4));
  28         }
  29         bool dequeue(int *v) {
  30                 node* t = tail.load(wildcard(5));
  31                 node* n = t->next.load(wildcard(6));/*@ \label{line:spscAcquire} @*/
  32                 if (0 == n)
  33                         return false;
  34                 *v = n->data.load(memory_order_normal);
  35                 tail.store(n, wildcard(7));
  36                 delete (t);
  37                 return true;
  38         }
  39 };
  40
  41
  42 spsc_queue *q;/*@ \label{line:testcaseBegin} @*/
  43 atomic_int arr[2];
  44 void thrd1() { // Thread 1/*@ \label{line:thrd1} @*/
  45         arr[1].store(47, relaxed);
  46         q->enqueue(1);
  47 }
  48 void thrd2() { // Thread 2/*@ \label{line:thrd2} @*/
  49         int idx;
  50         if (q->dequeue(&idx))
  51                 arr[idx].load(relaxed);
  52 }
  53
  54 int user_main(int argc, char **argv)
  55 {
  56         thrd_t A, B;
  57         q = new spsc_queue;
  58         thrd_create(&A, (thrd_start_t)&thrd1, NULL);
  59         thrd_create(&B, (thrd_start_t)&thrd2, NULL);
  60         thrd_join(A);
  61         thrd_join(B);
  62
  63         //delete q;
  64
  65         return 0;
  66 }