From: Peizhao Ou Date: Sat, 14 Feb 2015 02:48:45 +0000 (-0800) Subject: changes X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=241ce6c4685d235cdae32e721505ec5024b8b5b3;p=model-checker-benchmarks.git changes --- diff --git a/ms-queue/Makefile b/ms-queue/Makefile index 46554a1..55a4edb 100644 --- a/ms-queue/Makefile +++ b/ms-queue/Makefile @@ -2,7 +2,7 @@ include ../benchmarks.mk BENCH := queue -NORMAL_TESTS := testcase1 testcase2 +NORMAL_TESTS := testcase1 testcase2 testcase3 WILDCARD_TESTS := $(patsubst %, %_wildcard, $(NORMAL_TESTS)) diff --git a/ms-queue/queue.c b/ms-queue/queue.c index 0a5f3bd..c7b5de5 100644 --- a/ms-queue/queue.c +++ b/ms-queue/queue.c @@ -33,6 +33,13 @@ static unsigned int new_node() return 0; } +/* Simulate the fact that when a node got recycled, it will get assigned to the + * same queue or for other usage */ +void simulateRecycledNodeUpdate(queue_t *q, unsigned int node) { + atomic_store_explicit(&q->nodes[node].next, -1, memory_order_release); +} + + /* Place this node index back on this thread's free list */ static void reclaim(unsigned int node) { @@ -76,7 +83,7 @@ void init_queue(queue_t *q, int num_threads) atomic_init(&q->nodes[1].next, MAKE_POINTER(0, 0)); } -void enqueue(queue_t *q, unsigned int val) +void enqueue(queue_t *q, unsigned int val, bool yield) { int success = 0; unsigned int node; @@ -120,7 +127,7 @@ void enqueue(queue_t *q, unsigned int val) release, release); } -bool dequeue(queue_t *q, unsigned int *retVal) +bool dequeue(queue_t *q, unsigned int *retVal, unsigned int *reclaimNode) { int success = 0; pointer head; @@ -156,6 +163,7 @@ bool dequeue(queue_t *q, unsigned int *retVal) } } } + reclaimNode = get_ptr(head); reclaim(get_ptr(head)); return true; } diff --git a/ms-queue/queue.h b/ms-queue/queue.h index edaf3dd..76e217b 100644 --- a/ms-queue/queue.h +++ b/ms-queue/queue.h @@ -22,10 +22,13 @@ typedef struct node { typedef struct { pointer_t head; pointer_t tail; - node_t nodes[MAX_NODES + 1]; + node_t nodes[MAX_NODES + 2]; } queue_t; void init_queue(queue_t *q, int num_threads); -void enqueue(queue_t *q, unsigned int val); -bool dequeue(queue_t *q, unsigned int *retVal); +void enqueue(queue_t *q, unsigned int val, bool yield); +bool dequeue(queue_t *q, unsigned int *retVal, unsigned int *reclaimedNode); + +void simulateRecycledNodeUpdate(queue_t *q, unsigned int node); + int get_thread_num(); diff --git a/ms-queue/queue_wildcard.c b/ms-queue/queue_wildcard.c index 73289a7..802e6f6 100644 --- a/ms-queue/queue_wildcard.c +++ b/ms-queue/queue_wildcard.c @@ -32,6 +32,12 @@ static unsigned int new_node() return 0; } +/* Simulate the fact that when a node got recycled, it will get assigned to the + * same queue or for other usage */ +void simulateRecycledNodeUpdate(queue_t *q, unsigned int node) { + atomic_store_explicit(&q->nodes[node].next, -1, memory_order_release); +} + /* Place this node index back on this thread's free list */ static void reclaim(unsigned int node) { @@ -77,7 +83,7 @@ void init_queue(queue_t *q, int num_threads) atomic_init(&q->nodes[1].next, MAKE_POINTER(0, 0)); } -void enqueue(queue_t *q, unsigned int val) +void enqueue(queue_t *q, unsigned int val, bool yield) { int success = 0; unsigned int node; @@ -94,7 +100,9 @@ void enqueue(queue_t *q, unsigned int val) while (!success) { tail = atomic_load_explicit(&q->tail, wildcard(3)); // acquire - // FIXME: SCFence makes this relaxed + // FIXME: SCFence makes this relaxed + if (yield) + thrd_yield(); next = atomic_load_explicit(&q->nodes[get_ptr(tail)].next, wildcard(4)); //acquire if (tail == atomic_load_explicit(&q->tail, wildcard(5))) { // relaxed @@ -103,13 +111,6 @@ void enqueue(queue_t *q, unsigned int val) if (get_ptr(next) == 0) { // == NULL pointer value = MAKE_POINTER(node, get_count(next) + 1); - - // *********************************** - // Inference analysis results have two choices here, it either - // makes wildcard(6) acq_rel and wildcard(8) relaxed or - // wildcard(6) release and wildcard(8) acquire. The - // synchronization here is for enqueue() to dequeue(), and - // actually either synchronization options will work!!! success = atomic_compare_exchange_strong_explicit(&q->nodes[get_ptr(tail)].next, &next, value, wildcard(6), wildcard(7)); // release & relaxed } @@ -131,7 +132,7 @@ void enqueue(queue_t *q, unsigned int val) wildcard(11), wildcard(12)); // release & relaxed } -bool dequeue(queue_t *q, unsigned int *retVal) +bool dequeue(queue_t *q, unsigned int *retVal, unsigned int *reclaimNode) { unsigned int value; int success = 0; @@ -169,6 +170,8 @@ bool dequeue(queue_t *q, unsigned int *retVal) } } } + + reclaimNode = get_ptr(head); reclaim(get_ptr(head)); *retVal = value; return true; diff --git a/ms-queue/result2.txt b/ms-queue/result2.txt new file mode 100644 index 0000000..eae4d2b --- /dev/null +++ b/ms-queue/result2.txt @@ -0,0 +1,17 @@ + +Result 1: +wildcard 1 -> memory_order_relaxed +wildcard 2 -> memory_order_relaxed +wildcard 3 -> memory_order_acquire +wildcard 4 -> memory_order_relaxed +wildcard 5 -> memory_order_relaxed +wildcard 6 -> memory_order_acq_rel +wildcard 8 -> memory_order_relaxed +wildcard 9 -> memory_order_release +wildcard 11 -> memory_order_release +wildcard 13 -> memory_order_acquire +wildcard 14 -> memory_order_acquire +wildcard 15 -> memory_order_acquire +wildcard 16 -> memory_order_relaxed +wildcard 17 -> memory_order_release +wildcard 19 -> memory_order_release diff --git a/ms-queue/result3.txt b/ms-queue/result3.txt new file mode 100644 index 0000000..de42103 --- /dev/null +++ b/ms-queue/result3.txt @@ -0,0 +1,16 @@ +Result 0: +wildcard 1 -> memory_order_relaxed +wildcard 2 -> memory_order_relaxed +wildcard 3 -> memory_order_acquire +wildcard 4 -> memory_order_relaxed +wildcard 5 -> memory_order_relaxed +wildcard 6 -> memory_order_acq_rel +wildcard 8 -> memory_order_acquire +wildcard 9 -> memory_order_release +wildcard 11 -> memory_order_release +wildcard 13 -> memory_order_acquire +wildcard 14 -> memory_order_acquire +wildcard 15 -> memory_order_acquire +wildcard 16 -> memory_order_relaxed +wildcard 17 -> memory_order_release +wildcard 19 -> memory_order_release diff --git a/ms-queue/testcase1.c b/ms-queue/testcase1.c index 78feaa4..b416c7d 100644 --- a/ms-queue/testcase1.c +++ b/ms-queue/testcase1.c @@ -25,6 +25,7 @@ int get_thread_num() bool succ1, succ2; atomic_int x[3]; int idx1, idx2; +unsigned int reclaimNode; static int procs = 4; static void main_task(void *param) @@ -33,18 +34,18 @@ static void main_task(void *param) int pid = *((int *)param); if (pid % 4 == 0) { atomic_store_explicit(&x[0], 1, memory_order_relaxed); - enqueue(queue, 0); + enqueue(queue, 0, false); } else if (pid % 4 == 1) { atomic_store_explicit(&x[1], 1, memory_order_relaxed); - enqueue(queue, 1); + enqueue(queue, 1, false); } else if (pid % 4 == 2) { - succ1 = dequeue(queue, &idx1); + succ1 = dequeue(queue, &idx1, &reclaimNode); if (succ1) { atomic_load_explicit(&x[idx1], memory_order_relaxed); } } else if (pid % 4 == 3) { /* - succ2 = dequeue(queue, &idx2); + succ2 = dequeue(queue, &idx2, &reclaimNode); if (succ2) { atomic_load_explicit(&x[idx2], memory_order_relaxed); } diff --git a/ms-queue/testcase2.c b/ms-queue/testcase2.c index 3431b26..e862239 100644 --- a/ms-queue/testcase2.c +++ b/ms-queue/testcase2.c @@ -25,6 +25,7 @@ int get_thread_num() bool succ1, succ2; atomic_int x[3]; int idx1, idx2; +unsigned int reclaimNode; static int procs = 4; static void main_task(void *param) @@ -38,14 +39,14 @@ static void main_task(void *param) */ } else if (pid % 4 == 1) { atomic_store_explicit(&x[1], 1, memory_order_relaxed); - enqueue(queue, 1); + enqueue(queue, 1, false); } else if (pid % 4 == 2) { - succ1 = dequeue(queue, &idx1); + succ1 = dequeue(queue, &idx1, &reclaimNode); if (succ1) { atomic_load_explicit(&x[idx1], memory_order_relaxed); } } else if (pid % 4 == 3) { - succ2 = dequeue(queue, &idx2); + succ2 = dequeue(queue, &idx2, &reclaimNode); if (succ2) { atomic_load_explicit(&x[idx2], memory_order_relaxed); } diff --git a/ms-queue/testcase3.c b/ms-queue/testcase3.c index f6243f9..cd2bf44 100644 --- a/ms-queue/testcase3.c +++ b/ms-queue/testcase3.c @@ -25,28 +25,36 @@ int get_thread_num() bool succ1, succ2; atomic_int x[3]; int idx1, idx2; +unsigned int reclaimNode1, reclaimNode2; -static int procs = 4; +static int procs = 2; static void main_task(void *param) { unsigned int val; int pid = *((int *)param); if (pid % 4 == 0) { - atomic_store_explicit(&x[0], 1, memory_order_relaxed); - enqueue(queue, 0); + //atomic_store_explicit(&x[0], 1, memory_order_relaxed); + enqueue(queue, 0, true); - succ1 = dequeue(queue, &idx1); + + } else if (pid % 4 == 1) { + //atomic_store_explicit(&x[1], 1, memory_order_relaxed); + enqueue(queue, 1, false); + enqueue(queue, 1, false); + + succ1 = dequeue(queue, &idx1, &reclaimNode1); if (succ1) { - atomic_load_explicit(&x[idx1], memory_order_relaxed); + //atomic_load_explicit(&x[idx1], memory_order_relaxed); } - } else if (pid % 4 == 1) { - atomic_store_explicit(&x[1], 1, memory_order_relaxed); - enqueue(queue, 1); - succ2 = dequeue(queue, &idx2); + succ2 = dequeue(queue, &idx2, &reclaimNode2); if (succ2) { - atomic_load_explicit(&x[idx2], memory_order_relaxed); + //atomic_load_explicit(&x[idx2], memory_order_relaxed); } + simulateRecycledNodeUpdate(queue, reclaimNode1); + + + } else if (pid % 4 == 2) { } else if (pid % 4 == 3) {