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