clang/test/ms-queue-simple-offset.c

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