projects
/
model-checker-benchmarks.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (from parent 1:
19711e1
)
ms-queue: begin relaxing
author
Brian Norris
<banorris@uci.edu>
Thu, 7 Mar 2013 03:32:05 +0000
(19:32 -0800)
committer
Brian Norris
<banorris@uci.edu>
Thu, 7 Mar 2013 03:34:39 +0000
(19:34 -0800)
Not functioning yet.
ms-queue/my_queue.c
patch
|
blob
|
history
diff --git
a/ms-queue/my_queue.c
b/ms-queue/my_queue.c
index 2377d01a4679cad3a4bdcc3175aa01bfed26ccec..7966fb200969d41ceb0d27b17c3dbba1e69237b2 100644
(file)
--- a/
ms-queue/my_queue.c
+++ b/
ms-queue/my_queue.c
@@
-59,18
+59,18
@@
void enqueue(queue_t *q, unsigned int val)
node = new_node();
store_32(&q->nodes[node].value, val);
node = new_node();
store_32(&q->nodes[node].value, val);
- tmp = atomic_load
(&q->nodes[node].next
);
+ tmp = atomic_load
_explicit(&q->nodes[node].next, memory_order_relaxed
);
set_ptr(&tmp, 0); // NULL
set_ptr(&tmp, 0); // NULL
- atomic_store
(&q->nodes[node].next, tmp
);
+ atomic_store
_explicit(&q->nodes[node].next, tmp, memory_order_relaxed
);
while (!success) {
while (!success) {
- tail = atomic_load
(&q->tail
);
- next = atomic_load
(&q->nodes[get_ptr(tail)].next
);
+ tail = atomic_load
_explicit(&q->tail, memory_order_relaxed
);
+ next = atomic_load
_explicit(&q->nodes[get_ptr(tail)].next, memory_order_relaxed
);
if (tail == atomic_load(&q->tail)) {
if (get_ptr(next) == 0) { // == NULL
pointer value = MAKE_POINTER(node, get_count(next) + 1);
if (tail == atomic_load(&q->tail)) {
if (get_ptr(next) == 0) { // == NULL
pointer value = MAKE_POINTER(node, get_count(next) + 1);
- success = atomic_compare_exchange_weak(&q->nodes[get_ptr(tail)].next,
- &next, value);
+ success = atomic_compare_exchange_weak
_explicit
(&q->nodes[get_ptr(tail)].next,
+ &next, value
, memory_order_release, memory_order_release
);
}
if (!success) {
unsigned int ptr = get_ptr(atomic_load(&q->nodes[get_ptr(tail)].next));
}
if (!success) {
unsigned int ptr = get_ptr(atomic_load(&q->nodes[get_ptr(tail)].next));
@@
-82,9
+82,10
@@
void enqueue(queue_t *q, unsigned int val)
}
}
}
}
}
}
- atomic_compare_exchange_strong(&q->tail,
+ atomic_compare_exchange_strong
_explicit
(&q->tail,
&tail,
&tail,
- MAKE_POINTER(node, get_count(tail) + 1));
+ MAKE_POINTER(node, get_count(tail) + 1),
+ memory_order_release, memory_order_release);
}
unsigned int dequeue(queue_t *q)
}
unsigned int dequeue(queue_t *q)
@@
-96,9
+97,9
@@
unsigned int dequeue(queue_t *q)
pointer next;
while (!success) {
pointer next;
while (!success) {
- head = atomic_load
(&q->hea
d);
- tail = atomic_load
(&q->tail
);
- next = atomic_load
(&q->nodes[get_ptr(head)].next
);
+ head = atomic_load
_explicit(&q->head, memory_order_relaxe
d);
+ tail = atomic_load
_explicit(&q->tail, memory_order_relaxed
);
+ next = atomic_load
_explicit(&q->nodes[get_ptr(head)].next, memory_order_relaxed
);
if (atomic_load(&q->head) == head) {
if (get_ptr(head) == get_ptr(tail)) {
if (get_ptr(next) == 0) { // NULL
if (atomic_load(&q->head) == head) {
if (get_ptr(head) == get_ptr(tail)) {
if (get_ptr(next) == 0) { // NULL