benchmarks/satcheck/msqueueoffset/ms-queue-simple_unannotated.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(queue_t *q, int num_threads);
  12 void enqueue(queue_t *q, unsigned int val);
  13 bool dequeue(queue_t *q, unsigned int *retVal);
  14
  15 queue_t queue;
  16
  17 void init_queue(queue_t *q, int num_threads) {
  18         struct node *newnode=(struct node *)malloc(sizeof (struct node));
  19
  20         store_32(&newnode->value, 0);
  21
  22
  23         store_64(&newnode->next, (uintptr_t) NULL);
  24                 /* initialize queue */
  25
  26         store_64(&q->head, (uintptr_t) newnode);
  27
  28
  29         store_64(&q->tail, (uintptr_t) newnode);
  30 }
  31
  32 void enqueue(queue_t *q, unsigned int val) {
  33         struct node *tail;
  34         struct node * node_ptr; node_ptr = (struct node *)malloc(sizeof(struct node));
  35
  36         store_32(&node_ptr->value, val);
  37
  38
  39         store_64(&node_ptr->next, (uintptr_t) NULL);
  40
  41         while (true) {
  42
  43                 tail = (struct node *) load_64(&q->tail);
  44
  45                 struct node * next = (struct node *) load_64(&tail->next);
  46
  47                 struct node * qtail = (struct node *) load_64(&q->tail);
  48
  49                 if (tail == qtail) {
  50                         if (next) {
  51                                 MC2_yield();
  52                         } else {
  53                                 struct node * valread = (struct node *) rmw_64(CAS, &tail->next, (uintptr_t) next, (uintptr_t) node_ptr);
  54
  55                                 if (next == valread) {
  56                                         break;
  57                                 } else {
  58                                 }
  59                         }
  60                         struct node * new_tailptr = (struct node *)load_64(&tail->next);
  61                         rmw_64(CAS, &q->tail, (uintptr_t) tail, (uintptr_t) new_tailptr);
  62                         MC2_yield();
  63                 } else {
  64                         MC2_yield();
  65                 }
  66         }
  67
  68         rmw_64(CAS, &q->tail, (uintptr_t) tail, (uintptr_t) node_ptr);
  69 }
  70
  71 bool dequeue(queue_t *q, unsigned int *retVal) {
  72         while (true) {
  73                 struct node * head = (struct node *) load_64(&q->head);
  74                 struct node * tail = (struct node *) load_64(&q->tail);
  75                 struct node * next = (struct node *) load_64(&head->next);
  76
  77                 struct node * headr = (struct node *) load_64(&q->head);
  78
  79                 if (head == headr) {
  80                         if (head == tail) {
  81                                 if (next) {
  82                                         MC2_yield();
  83                                 } else {
  84                                         return false; // NULL
  85                                 }
  86                                 rmw_64(CAS, &q->tail, (uintptr_t) tail, (uintptr_t) next);
  87                                 MC2_yield();
  88                         } else {
  89                                 *retVal = load_32(&next->value);
  90                                 struct node *old_head = (struct node *) rmw_64(CAS, &q->head,
  91                                                                                                                                                                                                                          (uintptr_t) head,
  92                                                                                                                                                                                                                          (uintptr_t) next);
  93
  94                                 if (head == old_head) {
  95                                         return true;
  96                                 } else {
  97                                         MC2_yield();
  98                                 }
  99                         }
 100                 } else {
 101                         MC2_yield();
 102                 }
 103         }
 104 }
 105
 106 /* ms-queue-main */
 107 bool succ1, succ2;
 108
 109 static void e(void *p) {
 110         int i;
 111         for(i=0;i<PROBLEMSIZE;i++) {
 112                 enqueue(&queue, 1);
 113         }
 114 }
 115
 116 static void d(void *p) {
 117         unsigned int val;
 118         int i;
 119         for(i=0;i<PROBLEMSIZE;i++) {
 120                 int r;
 121                 r = dequeue(&queue, &val);
 122         }
 123 }
 124
 125 int user_main(int argc, char **argv)
 126 {
 127         init_queue(&queue, 2);
 128
 129         thrd_t t1,t2;
 130         thrd_create(&t1, e, NULL);
 131         thrd_create(&t2, d, NULL);
 132
 133         thrd_join(t1);
 134         thrd_join(t2);
 135
 136         return 0;
 137 }