benchmarks/satcheck-precompiled/msqueueoffset/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, MCID * retval);
  14
  15 queue_t queue;
  16
  17 void init_queue(MCID _mq, queue_t *q, MCID _mnum_threads, int num_threads) {
  18         MCID _fn0; struct node *newnode=(struct node *)malloc(sizeof (struct node));
  19         _fn0 = MC2_function_id(0, 0, sizeof (newnode), (uint64_t)newnode);
  20
  21         MC2_nextOpStoreOffset(_fn0, MC2_OFFSET(struct node *, value), MCID_NODEP);
  22         store_32(&newnode->value, 0);
  23
  24
  25         MC2_nextOpStoreOffset(_fn0, MC2_OFFSET(struct node *, next), MCID_NODEP);
  26         store_64(&newnode->next, (uintptr_t) NULL);
  27                 /* initialize queue */
  28
  29         MC2_nextOpStoreOffset(_mq, MC2_OFFSET(queue_t *, head), _fn0);
  30         store_64(&q->head, (uintptr_t) newnode);
  31
  32
  33         MC2_nextOpStoreOffset(_mq, MC2_OFFSET(queue_t *, tail), _fn0);
  34         store_64(&q->tail, (uintptr_t) newnode);
  35 }
  36
  37 void enqueue(MCID _mq, queue_t *q, MCID _mval, unsigned int val) {
  38         MCID _mtail; struct node *tail;
  39         MCID _fn1; struct node * node_ptr; node_ptr = (struct node *)malloc(sizeof(struct node));
  40         _fn1 = MC2_function_id(0, 1, sizeof (node_ptr), (uint64_t)node_ptr, _fn1);
  41
  42         MC2_nextOpStoreOffset(_fn1, MC2_OFFSET(struct node *, value), _mval);
  43         store_32(&node_ptr->value, val);
  44
  45
  46         MC2_nextOpStoreOffset(_fn1, MC2_OFFSET(struct node *, next), MCID_NODEP);
  47         store_64(&node_ptr->next, (uintptr_t) NULL);
  48
  49         MC2_enterLoop();
  50         while (true) {
  51
  52                 _mtail=MC2_nextOpLoadOffset(_mq, MC2_OFFSET(queue_t *, tail)), tail = (struct node *) load_64(&q->tail);
  53
  54                 MCID _mnext; _mnext=MC2_nextOpLoadOffset(_mtail, MC2_OFFSET(struct node *, next)); struct node * next = (struct node *) load_64(&tail->next);
  55
  56                 MCID _mqtail; _mqtail=MC2_nextOpLoadOffset(_mq, MC2_OFFSET(queue_t *, tail)); struct node * qtail = (struct node *) load_64(&q->tail);
  57
  58                 MCID _br0;
  59
  60                 MCID _cond0_m;
  61
  62                 int _cond0 = MC2_equals(_mtail, (uint64_t)tail, _mqtail, (uint64_t)qtail, &_cond0_m);
  63                 if (_cond0) {
  64                         MCID _br1;
  65                         _br0 = MC2_branchUsesID(_cond0_m, 1, 2, true);
  66
  67                         int _cond1 = next;
  68                         MCID _cond1_m = MC2_function_id(1, 1, sizeof(_cond1), _cond1, _mnext);
  69                         if (_cond1) {
  70                                 _br1 = MC2_branchUsesID(_mnext, 1, 2, true);
  71                                 MC2_yield();
  72                                 MC2_merge(_br1);
  73                         } else {
  74                                 _br1 = MC2_branchUsesID(_mnext, 0, 2, true);
  75                                 MCID _rmw0 = MC2_nextRMWOffset(_mtail, MC2_OFFSET(struct node *, next), _mnext, _fn1);
  76                                 struct node * valread = (struct node *) rmw_64(CAS, &tail->next, (uintptr_t) next, (uintptr_t) node_ptr);
  77
  78                                 MCID _br2;
  79
  80                                 MCID _cond2_m;
  81
  82                                 int _cond2 = MC2_equals(_mnext, (uint64_t)next, _rmw0, (uint64_t)valread, &_cond2_m);
  83                                 if (_cond2) {
  84                                         _br2 = MC2_branchUsesID(_cond2_m, 1, 2, true);
  85                                         break;
  86                                 } else {_br2 = MC2_branchUsesID(_cond2_m, 0, 2, true);
  87
  88                                         MC2_merge(_br2);
  89                                 }
  90                                 MC2_merge(_br1);
  91                         }
  92                         MCID _mnew_tailptr; _mnew_tailptr=MC2_nextOpLoadOffset(_mtail, MC2_OFFSET(struct node *, next)); struct node * new_tailptr = (struct node *)load_64(&tail->next);
  93                         MCID _rmw1 = MC2_nextRMWOffset(_mq, MC2_OFFSET(queue_t *, tail), _mtail, _mnew_tailptr);
  94                         rmw_64(CAS, &q->tail, (uintptr_t) tail, (uintptr_t) new_tailptr);
  95                         MC2_yield();
  96                         MC2_merge(_br0);
  97                 } else {
  98                         _br0 = MC2_branchUsesID(_cond0_m, 0, 2, true);
  99                         MC2_yield();
 100                         MC2_merge(_br0);
 101                 }
 102         }
 103 MC2_exitLoop();
 104
 105
 106         MCID _rmw2 = MC2_nextRMWOffset(_mq, MC2_OFFSET(queue_t *, tail), _mtail, _fn1);
 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, MCID * retval) {
 111         MC2_enterLoop();
 112         while (true) {
 113                 MCID _mhead; _mhead=MC2_nextOpLoadOffset(_mq, MC2_OFFSET(queue_t *, head)); struct node * head = (struct node *) load_64(&q->head);
 114                 MCID _mtail; _mtail=MC2_nextOpLoadOffset(_mq, MC2_OFFSET(queue_t *, tail)); struct node * tail = (struct node *) load_64(&q->tail);
 115                 MCID _mnext; _mnext=MC2_nextOpLoadOffset(_mhead, MC2_OFFSET(struct node *, next)); struct node * next = (struct node *) load_64(&head->next);
 116
 117                 MCID _mheadr; _mheadr=MC2_nextOpLoadOffset(_mq, MC2_OFFSET(queue_t *, head)); struct node * headr = (struct node *) load_64(&q->head);
 118
 119                 MCID _br3;
 120
 121                 MCID _cond3_m;
 122
 123                 int _cond3 = MC2_equals(_mhead, (uint64_t)head, _mheadr, (uint64_t)headr, &_cond3_m);
 124                 if (_cond3) {
 125                         MCID _br4;
 126                         _br3 = MC2_branchUsesID(_cond3_m, 1, 2, true);
 127
 128                         MCID _cond4_m;
 129
 130                         int _cond4 = MC2_equals(_mhead, (uint64_t)head, _mtail, (uint64_t)tail, &_cond4_m);
 131                         if (_cond4) {
 132                                 MCID _br5;
 133                                 _br4 = MC2_branchUsesID(_cond4_m, 1, 2, true);
 134
 135                                 int _cond5 = next;
 136                                 MCID _cond5_m = MC2_function_id(2, 1, sizeof(_cond5), _cond5, _mnext);
 137                                 if (_cond5) {
 138                                         _br5 = MC2_branchUsesID(_mnext, 1, 2, true);
 139                                         MC2_yield();
 140                                         MC2_merge(_br5);
 141                                 } else {
 142                                         *retval = MCID_NODEP;
 143                                         _br5 = MC2_branchUsesID(_mnext, 0, 2, true);
 144                                         MC2_exitLoop();
 145                                         return false; // NULL
 146                                 }
 147                                 MCID _rmw3 = MC2_nextRMWOffset(_mq, MC2_OFFSET(queue_t *, tail), _mtail, _mnext);
 148                                 rmw_64(CAS, &q->tail, (uintptr_t) tail, (uintptr_t) next);
 149                                 MC2_yield();
 150                                 MC2_merge(_br4);
 151                         } else {
 152                                 _br4 = MC2_branchUsesID(_cond4_m, 0, 2, true);
 153                                 _mretVal=MC2_nextOpLoadOffset(_mnext, MC2_OFFSET(struct node *, value)), *retVal = load_32(&next->value);
 154                                 MCID _rmw4 = MC2_nextRMWOffset(_mq, MC2_OFFSET(queue_t *, head), _mhead, _mnext);
 155                                 struct node *old_head = (struct node *) rmw_64(CAS, &q->head,
 156                                                                                                                                                                                                                          (uintptr_t) head,
 157                                                                                                                                                                                                                          (uintptr_t) next);
 158
 159                                 MCID _br6;
 160
 161                                 MCID _cond6_m;
 162
 163                                 int _cond6 = MC2_equals(_mhead, (uint64_t)head, _rmw4, (uint64_t)old_head, &_cond6_m);
 164                                 if (_cond6) {
 165                                         *retval = MCID_NODEP;
 166                                         _br6 = MC2_branchUsesID(_cond6_m, 1, 2, true);
 167                                         MC2_exitLoop();
 168                                         return true;
 169                                 } else {
 170                                         _br6 = MC2_branchUsesID(_cond6_m, 0, 2, true);
 171                                         MC2_yield();
 172                                         MC2_merge(_br6);
 173                                 }
 174                                 MC2_merge(_br4);
 175                         }
 176                         MC2_merge(_br3);
 177                 } else {
 178                         _br3 = MC2_branchUsesID(_cond3_m, 0, 2, true);
 179                         MC2_yield();
 180                         MC2_merge(_br3);
 181                 }
 182         }
 183 MC2_exitLoop();
 184
 185 }
 186
 187 /* ms-queue-main */
 188 bool succ1, succ2;
 189
 190 static void e(void *p) {
 191         int i;
 192         MC2_enterLoop();
 193         for(i=0;i<PROBLEMSIZE;i++) {
 194                 enqueue(MCID_NODEP, &queue, MCID_NODEP, 1);
 195         }
 196 MC2_exitLoop();
 197
 198 }
 199
 200 static void d(void *p) {
 201         unsigned int val;
 202         int i;
 203         MC2_enterLoop();
 204         for(i=0;i<PROBLEMSIZE;i++) {
 205                 int r;
 206                 MCID _rv0;
 207                 r = dequeue(MCID_NODEP, &queue, MCID_NODEP, &val, &_rv0);
 208         }
 209 MC2_exitLoop();
 210
 211 }
 212
 213 int user_main(int argc, char **argv)
 214 {
 215         init_queue(MCID_NODEP, &queue, MCID_NODEP, 2);
 216
 217         thrd_t t1,t2;
 218         thrd_create(&t1, e, NULL);
 219         thrd_create(&t2, d, NULL);
 220
 221         thrd_join(t1);
 222         thrd_join(t2);
 223
 224         return 0;
 225 }