8 #include "ms-queue-simple.h"
9 #include "libinterface.h"
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);
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));
20 void * _p0 = &newnode->value;
21 MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
25 void * _p1 = &newnode->next;
26 MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
27 store_64(_p1, (uintptr_t) NULL);
28 /* initialize queue */
30 void * _p2 = &q->head;
31 MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
32 store_64(_p2, (uintptr_t) newnode);
35 void * _p3 = &q->tail;
36 MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
37 store_64(_p3, (uintptr_t) newnode);
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);
45 void * _p4 = &node_ptr->value;
46 MCID _fn4 = MC2_function(1, MC2_PTR_LENGTH, _p4, _fn7);
47 MC2_nextOpStore(_fn4, _mval);
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);
58 _fn8=MC2_nextOpLoad(MCID_NODEP), tail = (struct node *) load_64(&q->tail);
60 MCID _fn9; struct node ** tail_ptr_next= & tail->next;
61 _fn9 = MC2_function(1, sizeof (tail_ptr_next), tail_ptr_next, _fn8);
63 MCID _mnext; _mnext=MC2_nextOpLoad(_fn9); struct node * next = (struct node *) load_64(tail_ptr_next);
65 MCID _mqtail; _mqtail=MC2_nextOpLoad(MCID_NODEP); struct node * qtail = (struct node *) load_64(&q->tail);
67 bool comp = (tail==qtail);
68 MCID _comp = MC2_function(2, 4, comp, _fn8, _mqtail);
71 _br0 = MC2_branchUsesID(_comp, 1, 2, true);
75 _br1 = MC2_branchUsesID(_mnext, 1, 2, true);
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);
85 _br2 = MC2_branchUsesID(_comp2, 1, 2, true);
88 _br2 = MC2_branchUsesID(_comp2, 0, 2, true);
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);
99 _br0 = MC2_branchUsesID(_comp, 0, 2, true);
106 MCID _rmw2 = MC2_nextRMW(MCID_NODEP, _fn8, _fn7);
107 rmw_64(CAS, &q->tail, (uintptr_t) tail, (uintptr_t) node_ptr);
110 bool dequeue(MCID _mq, queue_t *q, MCID _mretVal, unsigned int *retVal) {
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);
117 MCID _mt; _mt=MC2_nextOpLoad(MCID_NODEP); int t = ((struct node *) load_64(&q->head)) == head;
121 _br0 = MC2_branchUsesID(_mt, 1, 2, true);
123 bool comp = head == tail;
124 MCID _mcomp = MC2_function(2, 4, comp, _mhead, _mtail);
128 _br1 = MC2_branchUsesID(_mcomp, 1, 2, true);
131 _br2 = MC2_branchUsesID(_mnext, 1, 2, true);
134 _br2 = MC2_branchUsesID(_mnext, 0, 2, true);
136 return false; // NULL
138 MCID _rmw3 = MC2_nextRMW(MCID_NODEP, _mtail, _mnext);
139 rmw_64(CAS, &q->tail, (uintptr_t) tail, (uintptr_t) next);
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,
152 bool comp1 = old_head == head;
153 MCID _mcomp1 = MC2_function(2, 4, comp1, _rmw4, _mhead);
157 _br2 = MC2_branchUsesID(_mcomp1, 1, 2, true);
161 _br2 = MC2_branchUsesID(_mcomp1, 0, 2, true);
169 _br0 = MC2_branchUsesID(_mt, 0, 2, true);
180 static void e(void *p) {
181 enqueue(MCID_NODEP, &queue, MCID_NODEP, 1);
184 static void d(void *p) {
186 dequeue(MCID_NODEP, &queue, MCID_NODEP, &val);
189 int user_main(int argc, char **argv)
191 init_queue(MCID_NODEP, &queue, MCID_NODEP, 2);
194 thrd_create(&t1, e, NULL);
195 thrd_create(&t2, d, NULL);