test/ms-queue.c

   1 #include <threads.h>
   2 #include <stdlib.h>
   3 #include <stdio.h>
   4 #define true 1
   5 #define false 0
   6 #define bool int
   7
   8 #include "ms-queue.h"
   9 #include "libinterface.h"
  10
  11 void init_queue(MCID _mq, queue_t *q, MCID _mnum_threads, int num_threads);
  12 void enqueue(MCID _mq, queue_t *q, MCID _mval, unsigned int val);
  13 bool dequeue(MCID _mq, queue_t *q, MCID _mretVal, unsigned int *retVal);
  14
  15 void init_queue(MCID _mq, queue_t *q, MCID _mnum_threads, int num_threads) {
  16         int i, j;
  17         MCID _fn11; struct node *newnode=malloc(sizeof (struct node));
  18         _fn11 = MC2_function(0, sizeof (newnode), newnode);
  19
  20         void * _p0 = &newnode->value;
  21         MCID _fn0 = MC2_function(1, MC2_PTR_LENGTH, _p0, _fn11); MC2_nextOpStore(_fn0, MCID_NODEP);
  22         store_32(_p0, 0);
  23
  24
  25         void * _p1 = &newnode->next;
  26         MCID _fn1 = MC2_function(1, MC2_PTR_LENGTH, _p1, _fn11); MC2_nextOpStore(_fn1, MCID_NODEP);
  27         store_64(_p1, (uintptr_t) MAKE_POINTER(NULL, 0LL));
  28         /* initialize queue */
  29
  30         void * _p2 = &q->head;
  31         MCID _fn2 = MC2_function(1, MC2_PTR_LENGTH, _p2, _mq); MC2_nextOpStore(_fn2, _fn11);
  32         store_64(_p2, (uintptr_t) MAKE_POINTER(newnode, 0LL));
  33
  34
  35         void * _p3 = &q->tail;
  36         MCID _fn3 = MC2_function(1, MC2_PTR_LENGTH, _p3, _mq); MC2_nextOpStore(_fn3, _fn11);
  37         store_64(_p3, (uintptr_t) MAKE_POINTER(newnode, 0LL));
  38 }
  39
  40 void enqueue(MCID _mq, queue_t *q, MCID _mval, unsigned int val) {
  41         MCID _fn13; struct node *tail;
  42         MCID _fn12; struct node * node_ptr = malloc(sizeof(struct node));
  43         _fn12 = MC2_function(0, sizeof (node_ptr), node_ptr);
  44
  45         void * _p4 = &node_ptr->value;
  46         MCID _fn4 = MC2_function(1, MC2_PTR_LENGTH, _p4, _fn12); MC2_nextOpStore(_fn4, _mval);
  47         store_32(_p4, val);
  48
  49
  50         void * _p5 = &node_ptr->next;
  51         MCID _fn5 = MC2_function(1, MC2_PTR_LENGTH, _p5, _fn12); MC2_nextOpStore(_fn5, MCID_NODEP);
  52         store_64(_p5, (uintptr_t) MAKE_POINTER(NULL, GET_COUNT(1)));
  53
  54         MC2_enterLoop();
  55         while (true) {
  56
  57                 void * _p6 = &q->tail;
  58                 MCID _fn6 = MC2_function(1, MC2_PTR_LENGTH, _p6, _mq); _fn13=MC2_nextOpLoad(_fn6), tail = (struct node *) load_64(_p6);
  59                 _fn13 = MC2_function(1, sizeof (tail), tail, _fn13);
  60                 MCID _fn14; struct node ** tail_ptr_next= & GET_PTR(tail)->next;
  61                 _fn14 = MC2_function(1, sizeof (tail_ptr_next), tail_ptr_next, _fn13);
  62
  63                 MCID _mnext; _mnext=MC2_nextOpLoad(_fn14); struct node * next = (struct node *) load_64(tail_ptr_next);
  64
  65                 MCID _mqtail;
  66                 void * _p7 = &q->tail;
  67                 MCID _fn7 = MC2_function(1, MC2_PTR_LENGTH, _p7, _mq); _mqtail=MC2_nextOpLoad(_fn7); struct node * qtail = (struct node *) load_64(_p7);
  68                 MCID _fn15; int tqt = (tail == qtail);
  69                 _fn15 = MC2_function(2, sizeof (tqt), tqt, _fn13, _mqtail);
  70                 MCID _br0;
  71                 if (tqt) {
  72                         MCID _fn16; _br0 = MC2_branchUsesID(_fn15, 1, 2, true);
  73                         struct node *next_ptr=GET_PTR(next);
  74                         _fn16 = MC2_function(1, sizeof (next_ptr), next_ptr, _mnext);
  75
  76                         MCID _fn17; int npn = (next_ptr == NULL);
  77                         _fn17 = MC2_function(1, sizeof (npn), npn, _fn16);
  78                         MCID _br1;
  79                         if (npn) {
  80                                 MCID _fn18; _br1 = MC2_branchUsesID(_fn17, 1, 2, true);
  81                                 struct node * new_node = MAKE_POINTER(node_ptr, GET_COUNT(next) +1);
  82                                 _fn18 = MC2_function(2, sizeof (new_node), new_node, _fn12, _mnext);
  83                                 MCID _rmw0 = MC2_nextRMW(_fn14, _mnext, _fn18);
  84                                 struct node * valread = (struct node *) rmw_64(CAS, tail_ptr_next, (uintptr_t) next, (uintptr_t) new_node);
  85                                 MCID _fn19; int vn = (valread == next);
  86                                 _fn19 = MC2_function(2, sizeof (vn), vn, _mnext, _rmw0);
  87                                 MCID _br2;
  88                                 if (vn) {
  89                                         _br2 = MC2_branchUsesID(_fn19, 1, 2, true);
  90                                         break;
  91                                 } else {
  92                                         _br2 = MC2_branchUsesID(_fn19, 0, 2, true);
  93                                         MC2_yield();
  94                                         MC2_merge(_br2);
  95                                 }
  96                                 MC2_merge(_br1);
  97                         } else {
  98                                 _br1 = MC2_branchUsesID(_fn17, 0, 2, true);
  99                                 MC2_yield();
 100                                 MC2_merge(_br1);
 101                         }
 102                         MCID _mnew_tailptr; _mnew_tailptr=MC2_nextOpLoad(_fn14); struct node * new_tailptr = GET_PTR(load_64( tail_ptr_next));
 103                         MCID _fn20; struct node * newtail = MAKE_POINTER(new_tailptr, GET_COUNT(tail) + 1);
 104                         _fn20 = MC2_function(2, sizeof (newtail), newtail, _fn13, _mnew_tailptr);
 105                         MCID _rmw1 = MC2_nextRMW(MCID_NODEP, _fn13, _fn20);
 106                         rmw_64(CAS, &q->tail, (uintptr_t) tail, (uintptr_t) newtail);
 107                         MC2_yield();
 108                         MC2_merge(_br0);
 109                 } else {
 110                         _br0 = MC2_branchUsesID(_fn15, 0, 2, true);
 111                         MC2_yield();
 112                         MC2_merge(_br0);
 113                 }
 114         }
 115 MC2_exitLoop();
 116
 117         MCID _rmw2 = MC2_nextRMW(MCID_NODEP, _fn13, _fn13);
 118         rmw_64(CAS, &q->tail, (uintptr_t) tail, (uintptr_t)MAKE_POINTER(node_ptr, GET_COUNT(tail) + 1));
 119 }
 120
 121 bool dequeue(MCID _mq, queue_t *q, MCID _mretVal, unsigned int *retVal) {
 122         MC2_enterLoop();
 123         while (true) {
 124                 MCID _mhead;
 125                 void * _p8 = &q->head;
 126                 MCID _fn8 = MC2_function(1, MC2_PTR_LENGTH, _p8, _mq); _mhead=MC2_nextOpLoad(_fn8); struct node * head = (struct node *) load_64(_p8);
 127                 MCID _mtail;
 128                 void * _p9 = &q->tail;
 129                 MCID _fn9 = MC2_function(1, MC2_PTR_LENGTH, _p9, _mq); _mtail=MC2_nextOpLoad(_fn9); struct node * tail = (struct node *) load_64(_p9);
 130                 MCID _mnext; _mnext=MC2_nextOpLoad(_mhead); struct node * next = (struct node *) load_64(&(GET_PTR(head)->next));
 131
 132                 MCID _mt;
 133                 void * _p10 = &q->head;
 134                 MCID _fn10 = MC2_function(1, MC2_PTR_LENGTH, _p10, _mq); _mt=MC2_nextOpLoad(_fn10); int t = ((struct node *) load_64(_p10)) == head;
 135                 MCID _br3;
 136                 if (t) {
 137                         _br3 = MC2_branchUsesID(_mt, 1, 2, true);
 138                         if (GET_PTR(head) == GET_PTR(tail)) {
 139
 140                                 MCID _br4;
 141                                 if (GET_PTR(next) == NULL) {
 142                                         _br4 = MC2_branchUsesID(_mnext, 1, 2, true);
 143                                         MC2_exitLoop();
 144                                         return false; // NULL
 145                                 } else {
 146                                         _br4 = MC2_branchUsesID(_mnext, 0, 2, true);
 147                                         MC2_yield();
 148                                         MC2_merge(_br4);
 149                                 }
 150                                 MCID _rmw3 = MC2_nextRMW(MCID_NODEP, _mtail, _mtail);
 151                                 rmw_64(CAS, &q->tail, (uintptr_t) tail, (uintptr_t) MAKE_POINTER(GET_PTR(next), GET_COUNT(tail) + 1));
 152                                 MC2_yield();
 153                         } else {
 154                                 MCID _mnv; _mnv=MC2_nextOpLoad(_mnext); int nv = load_32(&GET_PTR(next)->value);
 155                                 MC2_nextOpStore(_mretVal, _mnv);
 156                                 store_32(retVal, nv);
 157                                 MCID _fn21; struct node * nh = MAKE_POINTER(GET_PTR(next), GET_COUNT(head)+1);
 158                                 _fn21 = MC2_function(2, sizeof (nh), nh, _mhead, _mnext);
 159                                 MCID _rmw4 = MC2_nextRMW(MCID_NODEP, _mhead, _fn21);
 160                                 struct node *old_head = (struct node *) rmw_64(CAS, &q->head,
 161                                                                                                                                                                                                                          (uintptr_t) head,
 162                                                                                                                                                                                                                          (uintptr_t) nh);
 163                                 if (old_head == head) {
 164                                         MC2_exitLoop();
 165                                         return true;
 166                                 } else {
 167                                         MC2_yield();
 168                                 }
 169                         }
 170                         MC2_merge(_br3);
 171                 } else { _br3 = MC2_branchUsesID(_mt, 0, 2, true);      MC2_merge(_br3);
 172                  }
 173         }
 174 MC2_exitLoop();
 175
 176 }
 177
 178 /* ms-queue-main */
 179 static queue_t queue;
 180 bool succ1, succ2;
 181
 182 static void e(void *p) {
 183         int i;
 184         MC2_enterLoop();
 185         for(i=0;i<2;i++)
 186         enqueue(MCID_NODEP, &queue, MCID_NODEP, 1);
 187 MC2_exitLoop();
 188
 189 }
 190
 191 static void d(void *p) {
 192         unsigned int val;
 193         int i;
 194         MC2_enterLoop();
 195         for(i=0;i<2;i++)
 196                 dequeue(MCID_NODEP, &queue, MCID_NODEP, &val);
 197 MC2_exitLoop();
 198
 199 }
 200
 201 int user_main(int argc, char **argv)
 202 {
 203         init_queue(MCID_NODEP, &queue, MCID_NODEP, 2);
 204
 205         thrd_t t1,t2;
 206         thrd_create(&t1, e, NULL);
 207         thrd_create(&t2, d, NULL);
 208
 209         thrd_join(t1);
 210         thrd_join(t2);
 211
 212         return 0;
 213 }