test/spsc-queue.cc

   1 #include <threads.h>
   2 #include "libinterface.h"
   3
   4 struct node {
   5         // atomic<struct node*> next;
   6         struct node * next;
   7         int data;
   8
   9         node(MCID _md, int d = 0) : data(d) {
  10         MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
  11         store_64(&next, 0);
  12         }
  13 };
  14
  15
  16 class spsc_queue {
  17 public:
  18         spsc_queue()
  19         {
  20                 MCID _mn; node* n = new node (MCID_NODEP); _mn = MC2_function(0, MC2_PTR_LENGTH, (uint64_t) n);
  21                 head = n;
  22                 tail = n;
  23         }
  24
  25         ~spsc_queue()
  26         {
  27         }
  28
  29         void enqueue(MCID _mdata, int data)
  30         {
  31                 MCID _mn; node* n = new node(MCID_NODEP, data); _mn = MC2_function(0, MC2_PTR_LENGTH, (uint64_t) n);
  32                 MC2_nextOpStore(MCID_NODEP, _mn);
  33                 store_64(&head->next->data, (uint64_t)n);
  34                 head = n;
  35         }
  36
  37         int dequeue() {
  38                 int data=0;
  39                 MC2_enterLoop();
  40                 while (0 == data) {
  41                         data = try_dequeue();
  42                 }
  43 MC2_exitLoop();
  44
  45                 return data;
  46         }
  47
  48 private:
  49
  50         struct node* head;
  51         struct node* tail;
  52
  53         int try_dequeue() {
  54                 node* t = tail;
  55                 MCID _mn;
  56                 void * _p0 = &t->next;
  57                 MCID _fn0 = MC2_function(1, MC2_PTR_LENGTH, (uint64_t)_p0, MCID_NODEP); _mn=MC2_nextOpLoad(_fn0); node* n = (node *)load_64(_p0);
  58                 MCID _br0;
  59                 if (0 == n) {
  60                         _br0 = MC2_branchUsesID(_mn, 1, 2, true);
  61                         return 0;
  62                 } else { _br0 = MC2_branchUsesID(_mn, 0, 2, true);      MC2_merge(_br0);
  63                  }
  64                 MCID _mdata;
  65                 void * _p1 = &n->data;
  66                 MCID _fn1 = MC2_function(1, MC2_PTR_LENGTH, (uint64_t)_p1, _mn); _mdata=MC2_nextOpLoad(_fn1); int data = load_64(_p1);
  67                 tail = n;
  68                 return data;
  69         }
  70 };
  71
  72
  73 spsc_queue *q;
  74
  75 void thread(unsigned thread_index)
  76 {
  77         MC2_enterLoop();
  78         for (int i = 0; i < 40; i++) {
  79                 MCID _br1;
  80                 if (0 == thread_index)
  81                         {
  82                                 _br1 = MC2_branchUsesID(MCID_NODEP, 1, 2, true);
  83                                 q->enqueue(MCID_NODEP, 11);
  84                                 MC2_merge(_br1);
  85                         }
  86                 else
  87                         {
  88                                 _br1 = MC2_branchUsesID(MCID_NODEP, 0, 2, true);
  89                                 int d = q->dequeue();
  90                                 // RL_ASSERT(11 == d);
  91                                 MC2_merge(_br1);
  92                         }
  93         }
  94 MC2_exitLoop();
  95
  96 }
  97
  98 int user_main(int argc, char **argv)
  99 {
 100         thrd_t A; thrd_t B;
 101
 102         q = new spsc_queue();
 103
 104         thrd_create(&A, (thrd_start_t)&thread, (void *)0);
 105         thrd_create(&B, (thrd_start_t)&thread, (void *)1);
 106         thrd_join(A);
 107         thrd_join(B);
 108
 109
 110         return 0;
 111 }