From: Peizhao Ou Date: Fri, 16 Jan 2015 03:02:21 +0000 (-0800) Subject: changes X-Git-Url: http://plrg.eecs.uci.edu/git/?a=commitdiff_plain;h=6d0e5824cfcdd3569f05e8d2a11992e7ac9a344f;p=cdsspec-compiler.git changes --- diff --git a/benchmark/chase-lev-deque-bugfix/deque.c b/benchmark/chase-lev-deque-bugfix/deque.c index 4dcb9bb..d174122 100644 --- a/benchmark/chase-lev-deque-bugfix/deque.c +++ b/benchmark/chase-lev-deque-bugfix/deque.c @@ -22,15 +22,27 @@ Deque * create() { */ int take(Deque *q) { size_t b = atomic_load_explicit(&q->bottom, memory_order_relaxed) - 1; + /** + @Begin + @Commit_point_define_check: true + @Label: Take_Read_Bottom + @End + */ Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed); + /** + //@Begin + @Commit_point_define_check: true + @Label: Take_Read_Array + @End + */ atomic_store_explicit(&q->bottom, b, memory_order_relaxed); /**** detected correctness ****/ atomic_thread_fence(memory_order_seq_cst); size_t t = atomic_load_explicit(&q->top, memory_order_relaxed); /** - @Begin - @Commit_point_define_check: t > b - @Label: Take_Point1 + //@Begin + @Commit_point_define_check: t != b + @Label: Take_Read_Top @End */ int x; @@ -39,9 +51,9 @@ int take(Deque *q) { int size = atomic_load_explicit(&a->size,memory_order_relaxed); x = atomic_load_explicit(&a->buffer[b % size], memory_order_relaxed); /** - @Begin + //@Begin @Commit_point_define_check: t != b - @Label: Take_Point2 + @Label: Take_Read_Buffer @End */ if (t == b) { @@ -51,8 +63,15 @@ int take(Deque *q) { 1, memory_order_seq_cst, memory_order_relaxed); /** @Begin - @Commit_point_define_check: true - @Label: Take_Point3 + @Commit_point_define_check: succ + @Label: Take_CAS_Top + @End + */ + + /** + @Begin + @Additional_ordering_point_define_check: !succ + @Label: Take_Additional_Point @End */ if (!succ) { @@ -100,7 +119,7 @@ void push(Deque *q, int x) { //Bug in paper...should have next line... a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed); /** - @Begin + //@Begin @Commit_point_define_check: true @Label: Push_Read_Array @End @@ -110,7 +129,7 @@ void push(Deque *q, int x) { atomic_store_explicit(&a->buffer[b % size], x, memory_order_relaxed); /** - @Begin + //@Begin @Commit_point_define_check: true @Label: Push_Update_Buffer @End @@ -135,14 +154,28 @@ void push(Deque *q, int x) { int steal(Deque *q) { //FIXME: weaken the following acquire causes no spec problem size_t t = atomic_load_explicit(&q->top, memory_order_acquire); + /** + //@Begin + @Potential_commit_point_define: true + @Label: Steal_Potential_Read_Tail + @End + */ //FIXME: remove the fence causes no error and fewer executions.. atomic_thread_fence(memory_order_seq_cst); /**** detected UL ****/ size_t b = atomic_load_explicit(&q->bottom, memory_order_acquire); /** @Begin - @Commit_point_define_check: t >= b - @Label: Steal_Point1 + @Commit_point_define_check: true + @Label: Steal_Read_Bottom + @End + */ + + /** + //@Begin + @Commit_point_define: t >= b + @Potential_commit_point_label: Steal_Potential_Read_Tail + @Label: Steal_Read_Tail @End */ int x = EMPTY; @@ -150,12 +183,18 @@ int steal(Deque *q) { /* Non-empty queue. */ /**** detected UL ****/ Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_acquire); + /** + //@Begin + @Commit_point_define_check: true + @Label: Steal_Read_Array + @End + */ int size = atomic_load_explicit(&a->size, memory_order_relaxed); x = atomic_load_explicit(&a->buffer[t % size], memory_order_relaxed); /** - @Begin + //@Begin @Potential_commit_point_define: true - @Label: Potential_Steal + @Label: Steal_Potential_Read_Buffer @End */ /**** detected correctness failure ****/ @@ -163,16 +202,23 @@ int steal(Deque *q) { memory_order_seq_cst, memory_order_relaxed); /** @Begin - @Commit_point_define_check: !succ - @Label: Steal_Point2 + @Commit_point_define_check: succ + @Label: Steal_CAS_Top @End */ /** @Begin + @Additional_ordering_point_define_check: !succ + @Label: Steal_Additional_Point + @End + */ + + /** + //@Begin @Commit_point_define: succ - @Potential_commit_point_label: Potential_Steal - @Label: Steal_Point3 + @Potential_commit_point_label: Steal_Potential_Read_Buffer + @Label: Steal_Read_Buffer @End */ if (!succ) { diff --git a/benchmark/chase-lev-deque-bugfix/deque.h b/benchmark/chase-lev-deque-bugfix/deque.h index da81cfa..0a87de7 100644 --- a/benchmark/chase-lev-deque-bugfix/deque.h +++ b/benchmark/chase-lev-deque-bugfix/deque.h @@ -72,7 +72,7 @@ void resize(Deque *q); /** @Begin @Interface: Take - @Commit_point_set: Take_Point1 | Take_Point2 | Take_Point3 + @Commit_point_set: Take_Read_Bottom | Take_CAS_Top |Take_Additional_Point @ID: __RET__ == EMPTY ? DEFAULT_CALL_ID : get_id(back(__deque)) @Action: int _Old_Val = EMPTY; @@ -91,7 +91,7 @@ int take(Deque *q); /** @Begin @Interface: Push - @Commit_point_set: Push_Read_Array | Push_Update_Buffer | Push_Update_Bottom + @Commit_point_set: Push_Update_Bottom @ID: get_and_inc(tag); @Action: tag_elem_t *elem = new_tag_elem(__ID__, x); @@ -103,7 +103,7 @@ void push(Deque *q, int x); /** @Begin @Interface: Steal - @Commit_point_set: Steal_Point1 | Steal_Point2 | Steal_Point3 + @Commit_point_set: Steal_Read_Bottom | Steal_CAS_Top | Steal_Additional_Point @ID: (__RET__ == EMPTY || __RET__ == ABORT) ? DEFAULT_CALL_ID : get_id(front(__deque)) @Action: int _Old_Val = EMPTY; diff --git a/benchmark/chase-lev-deque-bugfix/main.c b/benchmark/chase-lev-deque-bugfix/main.c index 786aa3c..6be90a5 100644 --- a/benchmark/chase-lev-deque-bugfix/main.c +++ b/benchmark/chase-lev-deque-bugfix/main.c @@ -16,6 +16,11 @@ int c; static void task(void * param) { //a=steal(q); a=steal(q); + if (a == ABORT) { + printf("Steal NULL\n"); + } else { + printf("Steal %d\n", a); + } } int user_main(int argc, char **argv) @@ -29,10 +34,23 @@ int user_main(int argc, char **argv) q=create(); thrd_create(&t, task, 0); push(q, 1); + printf("Push 1\n"); push(q, 2); + printf("Push 2\n"); push(q, 4); + printf("Push 4\n"); b=take(q); + if (b == EMPTY) { + printf("Take NULL\n"); + } else { + printf("Take %d\n", b); + } c=take(q); + if (c == EMPTY) { + printf("Take NULL\n"); + } else { + printf("Take %d\n", c); + } thrd_join(t); /* bool correct=true; diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java index 4acbfb6..89bc6a6 100644 --- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java +++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java @@ -327,7 +327,7 @@ public class CodeGenerator { // File[][] sources = { srcLinuxRWLocks, srcMSQueue, srcRCU, // srcDeque, srcMCSLock, srcSPSCQueue, srcMPMCQueue, srcHashtable }; - File[][] sources = {srcMSQueue, srcMPMCQueue }; + File[][] sources = {srcDeque }; // Compile all the benchmarks for (int i = 0; i < sources.length; i++) { CodeGenerator gen = new CodeGenerator(sources[i]);