changes

diff --git a/benchmark/chase-lev-deque-bugfix/deque.c b/benchmark/chase-lev-deque-bugfix/deque.c
index 4dcb9bbd156fe3581452fbec1dd6ff3291ef8463..d1741225f2963ec0c7d1d4fbe9f66591be37bffc 100644 (file)
--- 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;
 */
 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);
        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);
        /**
        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;
                @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);
                /**
                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
                        @Commit_point_define_check: t != b

-                       @Label: Take_Point2
+                       @Label: Take_Read_Buffer

                        @End
                */
                if (t == b) {
                        @End
                */
                if (t == b) {


@@ -51,8 +63,15 @@ int take(Deque *q) {
                                1, memory_order_seq_cst, memory_order_relaxed);
                        /**
                                @Begin
                                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) {
                                @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);
                /**
                //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
                        @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);
        /**
 
        atomic_store_explicit(&a->buffer[b % size], x, memory_order_relaxed);
        /**

-               @Begin
+               //@Begin

                @Commit_point_define_check: true
                @Label: Push_Update_Buffer
                @End
                @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);
 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
        //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;
                @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);
                /* 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);
                /**
                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
                        @Potential_commit_point_define: true

-                       @Label: Potential_Steal
+                       @Label: Steal_Potential_Read_Buffer

                        @End
                */
                /**** detected correctness failure ****/ 
                        @End
                */
                /**** detected correctness failure ****/ 


@@ -163,16 +202,23 @@ int steal(Deque *q) {
                        memory_order_seq_cst, memory_order_relaxed);
                /**
                        @Begin
                        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
                        @End
                */
 
                /**
                        @Begin

+                       @Additional_ordering_point_define_check: !succ
+                       @Label: Steal_Additional_Point
+                       @End
+               */
+
+               /**
+                       //@Begin

                        @Commit_point_define: succ
                        @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) {
                        @End
                */
                if (!succ) {

diff --git a/benchmark/chase-lev-deque-bugfix/deque.h b/benchmark/chase-lev-deque-bugfix/deque.h
index da81cfa13cf76d998a508b3e7bbc01b0b3dff899..0a87de7700c49bb57601de3dff7b8dbe149e2064 100644 (file)
--- 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 
 /**
     @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;
     @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 
 /**
     @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);
     @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 
 /**
     @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;
     @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 786aa3c9e975a6b013886887b3d375a98ba68560..6be90a5f7ffe73fc49f731ba6fd80cdf9f48e1f8 100644 (file)
--- 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);
 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)
 }
 
 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);
        q=create();
        thrd_create(&t, task, 0);
        push(q, 1);

+       printf("Push 1\n");

        push(q, 2);
        push(q, 2);

+       printf("Push 2\n");

        push(q, 4);
        push(q, 4);

+       printf("Push 4\n");

        b=take(q);
        b=take(q);

+       if (b == EMPTY) {
+               printf("Take NULL\n");
+       } else {
+               printf("Take %d\n", b);
+       }

        c=take(q);
        c=take(q);

+       if (c == EMPTY) {
+               printf("Take NULL\n");
+       } else {
+               printf("Take %d\n", c);
+       }

        thrd_join(t);
 /*
        bool correct=true;
        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 4acbfb623e57735f0eb8dd66cf9bde72d48c03fc..89bc6a61e873550003362c87736b47628be9efb9 100644 (file)
--- 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 = { 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]);
                // Compile all the benchmarks
                for (int i = 0; i < sources.length; i++) {
                        CodeGenerator gen = new CodeGenerator(sources[i]);