9 #include "ms-queue-simple.h"
10 #include "libinterface.h"
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);
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);
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);
30 MC2_nextOpStoreOffset(_mq, MC2_OFFSET(queue_t *, tail), _fn0);
31 store_64(&q->tail, (uintptr_t) newnode);
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);
39 MC2_nextOpStoreOffset(_fn1, MC2_OFFSET(struct node *, value), _mval);
40 store_32(&node_ptr->value, val);
43 MC2_nextOpStoreOffset(_fn1, MC2_OFFSET(struct node *, next), MCID_NODEP);
44 store_64(&node_ptr->next, (uintptr_t) NULL);
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;
52 MCID _mnext=MC2_nextOpLoadOffset(_fn2, MC2_OFFSET(struct node *, next));
53 struct node * next = (struct node *) load_64(tail_ptr_next);
56 _mqtail=MC2_nextOpLoadOffset(_mq, MC2_OFFSET(queue_t *,tail)); struct node * qtail = (struct node *) load_64(&q->tail);
59 int tqt = MC2_equals(_fn2, tail, _mqtail, qtail, &_fn16);
63 _br0 = MC2_branchUsesID(_fn16, 1, 2, true);
67 _br1 = MC2_branchUsesID(_mnext, 1, 2, true);
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);
75 int vn = MC2_equals(_mnext, next, _rmw0, valread, &_fn17);
78 _br1 = MC2_branchUsesID(_fn17, 1, 2, true);
80 } else { _br1 = MC2_branchUsesID(_fn17, 0, 2, true); MC2_merge(_br1);
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);
90 _br0 = MC2_branchUsesID(_fn16, 0, 2, true);
97 MCID _rmw2 = MC2_nextRMW(MCID_NODEP, _fn2, _fn1);
98 rmw_64(CAS, &q->tail, (uintptr_t) tail, (uintptr_t) node_ptr);
101 bool dequeue(MCID _mq, queue_t *q, MCID _mretVal, unsigned int *retVal) {
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);
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);
119 int t = MC2_equals(_mhead, head, _mload, headr, &_mt);
123 _br0 = MC2_branchUsesID(_mt, 1, 2, true);
126 int ht = MC2_equals(_mhead, head, _mtail, tail, &_fn18);
131 _br1 = MC2_branchUsesID(_fn18, 1, 2, true);
135 _br2 = MC2_branchUsesID(_mnext, 1, 2, true);
139 _br2 = MC2_branchUsesID(_mnext, 0, 2, true);
141 return false; // NULL
143 MCID _rmw3 = MC2_nextRMW(MCID_NODEP, _mtail, _mnext);
144 rmw_64(CAS, &q->tail, (uintptr_t) tail, (uintptr_t) next);
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,
157 int ohh = MC2_equals(_mhead, head, _rmw4, old_head, &_fn19);
161 _br6 = MC2_branchUsesID(_fn19, 1, 2, true);
165 _br6 = MC2_branchUsesID(_fn19, 0, 2, true);
173 _br0 = MC2_branchUsesID(_mt, 0, 2, true);
184 static void e(void *p) {
187 enqueue(MCID_NODEP, &queue, MCID_NODEP, 1);
190 static void d(void *p) {
193 for(i=0;i<PROBLEMSIZE;i++)
194 dequeue(MCID_NODEP, &queue, MCID_NODEP, &val);
197 int user_main(int argc, char **argv)
199 init_queue(MCID_NODEP, &queue, MCID_NODEP, 2);
202 thrd_create(&t1, e, NULL);
203 thrd_create(&t2, d, NULL);