projects
/
model-checker-benchmarks.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
save fixed ms-queue
[model-checker-benchmarks.git]
/
ms-queue
/
my_queue.c
diff --git
a/ms-queue/my_queue.c
b/ms-queue/my_queue.c
index ef3555296b1933cfb0f1b8d34d203de6089ea4d6..6c0ccd4bea4c0f49b2a1fdd4f9b24d992dc0f749 100644
(file)
--- a/
ms-queue/my_queue.c
+++ b/
ms-queue/my_queue.c
@@
-120,9
+120,8
@@
void enqueue(queue_t *q, unsigned int val)
release, release);
}
release, release);
}
-
unsigned int dequeue(queue_t *q
)
+
bool dequeue(queue_t *q, unsigned int *retVal
)
{
{
- unsigned int value;
int success = 0;
pointer head;
pointer tail;
int success = 0;
pointer head;
pointer tail;
@@
-139,7
+138,7
@@
unsigned int dequeue(queue_t *q)
MODEL_ASSERT(get_ptr(next) != POISON_IDX);
if (get_ptr(next) == 0) { // NULL
MODEL_ASSERT(get_ptr(next) != POISON_IDX);
if (get_ptr(next) == 0) { // NULL
- return
0
; // NULL
+ return
false
; // NULL
}
atomic_compare_exchange_strong_explicit(&q->tail,
&tail,
}
atomic_compare_exchange_strong_explicit(&q->tail,
&tail,
@@
-147,7
+146,7
@@
unsigned int dequeue(queue_t *q)
release, release);
thrd_yield();
} else {
release, release);
thrd_yield();
} else {
-
value
= load_32(&q->nodes[get_ptr(next)].value);
+
*retVal
= load_32(&q->nodes[get_ptr(next)].value);
success = atomic_compare_exchange_strong_explicit(&q->head,
&head,
MAKE_POINTER(get_ptr(next), get_count(head) + 1),
success = atomic_compare_exchange_strong_explicit(&q->head,
&head,
MAKE_POINTER(get_ptr(next), get_count(head) + 1),
@@
-158,5
+157,5
@@
unsigned int dequeue(queue_t *q)
}
}
reclaim(get_ptr(head));
}
}
reclaim(get_ptr(head));
- return
val
ue;
+ return
tr
ue;
}
}