clang/test/ms-queue-simple_manual.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 _fn6; struct node *newnode=malloc(sizeof (struct node));
  19
  20         void * _p0 = &newnode->value;
  21         MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
  22         store_32(_p0, 0);
  23
  24
  25         void * _p1 = &newnode->next;
  26         MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
  27         store_64(_p1, (uintptr_t) NULL);
  28                 /* initialize queue */
  29
  30         void * _p2 = &q->head;
  31         MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
  32         store_64(_p2, (uintptr_t) newnode);
  33
  34
  35         void * _p3 = &q->tail;
  36         MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
  37         store_64(_p3, (uintptr_t) newnode);
  38 }
  39
  40 void enqueue(MCID _mq, queue_t *q, MCID _mval, unsigned int val) {
  41         MCID _fn8; struct node *tail;
  42         MCID _fn7; struct node * node_ptr = malloc(sizeof(struct node));
  43         _fn7 = 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, _fn7);
  47         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, _fn7);
  53         MC2_nextOpStore(_fn5, MCID_NODEP);
  54         store_64(_p5, (uintptr_t) NULL);
  55
  56         MC2_enterLoop();
  57         while (true) {
  58                 _fn8=MC2_nextOpLoad(MCID_NODEP), tail = (struct node *) load_64(&q->tail);
  59
  60                 MCID _fn9; struct node ** tail_ptr_next= & tail->next;
  61                 _fn9 = MC2_function(1, sizeof (tail_ptr_next), tail_ptr_next, _fn8);
  62
  63                 MCID _mnext; _mnext=MC2_nextOpLoad(_fn9); struct node * next = (struct node *) load_64(tail_ptr_next);
  64
  65                 MCID _mqtail; _mqtail=MC2_nextOpLoad(MCID_NODEP); struct node * qtail = (struct node *) load_64(&q->tail);
  66
  67                 bool comp = (tail==qtail);
  68                 MCID _comp = MC2_function(2, 4, comp, _fn8, _mqtail);
  69                 MCID _br0;
  70                 if (comp) {
  71                         _br0 = MC2_branchUsesID(_comp, 1, 2, true);
  72
  73                         MCID _br1;
  74                         if (next) {
  75                                 _br1 = MC2_branchUsesID(_mnext, 1, 2, true);
  76                                 MC2_merge(_br1);
  77                         } else {
  78                                 _br1 = MC2_branchUsesID(_mnext, 0, 2, true);
  79                                 MCID _rmw0 = MC2_nextRMW(_fn9, _mnext, _fn7);
  80                                 struct node * valread = (struct node *) rmw_64(CAS, tail_ptr_next, (uintptr_t) next, (uintptr_t) node_ptr);
  81                                 bool comp2=(valread == next);
  82                                 MCID _comp2 = MC2_function(2, 4, comp2, _rmw0, _mnext);
  83                                 MCID _br2;
  84                                 if (comp2) {
  85                                         _br2 = MC2_branchUsesID(_comp2, 1, 2, true);
  86                                         break;
  87                                 } else {
  88                                         _br2 = MC2_branchUsesID(_comp2, 0, 2, true);
  89                                         MC2_merge(_br2);
  90                                 }
  91                                 MC2_merge(_br1);
  92                         }
  93                         MCID _mnew_tailptr; _mnew_tailptr=MC2_nextOpLoad(_fn9); struct node * new_tailptr = (struct node *)load_64( tail_ptr_next);
  94                         MCID _rmw1 = MC2_nextRMW(MCID_NODEP, _fn8, _mnew_tailptr);
  95                         rmw_64(CAS, &q->tail, (uintptr_t) tail, (uintptr_t) new_tailptr);
  96                         MC2_yield();
  97                         MC2_merge(_br0);
  98                 } else {
  99                         _br0 = MC2_branchUsesID(_comp, 0, 2, true);
 100                         MC2_yield();
 101                         MC2_merge(_br0);
 102                 }
 103         }
 104         MC2_exitLoop();
 105
 106         MCID _rmw2 = MC2_nextRMW(MCID_NODEP, _fn8, _fn7);
 107         rmw_64(CAS, &q->tail, (uintptr_t) tail, (uintptr_t) node_ptr);
 108 }
 109
 110 bool dequeue(MCID _mq, queue_t *q, MCID _mretVal, unsigned int *retVal) {
 111         MC2_enterLoop();
 112         while (true) {
 113                 MCID _mhead; _mhead=MC2_nextOpLoad(MCID_NODEP); struct node * head = (struct node *) load_64(&q->head);
 114                 MCID _mtail; _mtail=MC2_nextOpLoad(MCID_NODEP); struct node * tail = (struct node *) load_64(&q->tail);
 115                 MCID _mnext; _mnext=MC2_nextOpLoad(MCID_NODEP); struct node * next = (struct node *) load_64(&head->next);
 116
 117                 MCID _mt; _mt=MC2_nextOpLoad(MCID_NODEP); int t = ((struct node *) load_64(&q->head)) == head;
 118                 MCID _br0;
 119
 120                 if (t) {
 121                         _br0 = MC2_branchUsesID(_mt, 1, 2, true);
 122
 123                         bool comp = head == tail;
 124                         MCID _mcomp = MC2_function(2, 4, comp, _mhead, _mtail);
 125                         MCID _br1;
 126
 127                         if (comp) {
 128                                 _br1 = MC2_branchUsesID(_mcomp, 1, 2, true);
 129                                 MCID _br2;
 130                                 if (next) {
 131                                         _br2 = MC2_branchUsesID(_mnext, 1, 2, true);
 132                                         MC2_merge(_br2);
 133                                 } else {
 134                                         _br2 = MC2_branchUsesID(_mnext, 0, 2, true);
 135                                         MC2_exitLoop();
 136                                         return false; // NULL
 137                                 }
 138                                 MCID _rmw3 = MC2_nextRMW(MCID_NODEP, _mtail, _mnext);
 139                                 rmw_64(CAS, &q->tail, (uintptr_t) tail, (uintptr_t) next);
 140                                 MC2_yield();
 141                                 MC2_merge(_br1);
 142                         } else {
 143                                 _br1 = MC2_branchUsesID(_mcomp, 0, 2, true);
 144                                 void * nextval= &(next->value);
 145                                 MCID _mnextval = MC2_function(1, MC2_PTR_LENGTH, nextval, _mnext);
 146                                 MCID _rVal = MC2_nextOpLoad(_mnextval);
 147                                 *retVal = load_32(&next->value);
 148                                 MCID _rmw4 = MC2_nextRMW(MCID_NODEP, _mhead, _mnext);
 149                                 struct node *old_head = (struct node *) rmw_64(CAS, &q->head,
 150                                                                                                                                                                                                                          (uintptr_t) head,
 151                                                                                                                                                                                                                          (uintptr_t) next);
 152                                 bool comp1 = old_head == head;
 153                                 MCID _mcomp1 = MC2_function(2, 4, comp1, _rmw4, _mhead);
 154                                 MCID _br2;
 155
 156                                 if (comp1) {
 157                                         _br2 = MC2_branchUsesID(_mcomp1, 1, 2, true);
 158                                         MC2_exitLoop();
 159                                         return true;
 160                                 } else {
 161                                         _br2 = MC2_branchUsesID(_mcomp1, 0, 2, true);
 162                                         MC2_yield();
 163                                         MC2_merge(_br2);
 164                                 }
 165                                 MC2_merge(_br1);
 166                         }
 167                         MC2_merge(_br0);
 168                 } else {
 169                         _br0 = MC2_branchUsesID(_mt, 0, 2, true);
 170                         MC2_merge(_br0);
 171                 }
 172         }
 173         MC2_exitLoop();
 174
 175 }
 176
 177 /* ms-queue-main */
 178 bool succ1, succ2;
 179
 180 static void e(void *p) {
 181         enqueue(MCID_NODEP, &queue, MCID_NODEP, 1);
 182 }
 183
 184 static void d(void *p) {
 185         unsigned int val;
 186         dequeue(MCID_NODEP, &queue, MCID_NODEP, &val);
 187 }
 188
 189 int user_main(int argc, char **argv)
 190 {
 191         init_queue(MCID_NODEP, &queue, MCID_NODEP, 2);
 192
 193         thrd_t t1,t2;
 194         thrd_create(&t1, e, NULL);
 195         thrd_create(&t2, d, NULL);
 196
 197         thrd_join(t1);
 198         thrd_join(t2);
 199
 200         return 0;
 201 }