changes to the spec of deque

diff --git a/benchmark/chase-lev-deque-bugfix/deque.c b/benchmark/chase-lev-deque-bugfix/deque.c
index d1741225f2963ec0c7d1d4fbe9f66591be37bffc..fbd723bc6d5f0b2a3b33ff71dcb1e8a4c22b59c6 100644 (file)
--- a/benchmark/chase-lev-deque-bugfix/deque.c
+++ b/benchmark/chase-lev-deque-bugfix/deque.c
@@ -62,7 +62,7 @@ int take(Deque *q) {
                        bool succ = atomic_compare_exchange_strong_explicit(&q->top, &t, t +
                                1, memory_order_seq_cst, memory_order_relaxed);
                        /**
                        bool succ = atomic_compare_exchange_strong_explicit(&q->top, &t, t +
                                1, memory_order_seq_cst, memory_order_relaxed);
                        /**

-                               @Begin
+                               //@Begin

                                @Commit_point_define_check: succ 
                                @Label: Take_CAS_Top
                                @End
                                @Commit_point_define_check: succ 
                                @Label: Take_CAS_Top
                                @End


@@ -70,7 +70,7 @@ int take(Deque *q) {
 
                        /**
                                @Begin
 
                        /**
                                @Begin

-                               @Additional_ordering_point_define_check: !succ
+                               @Additional_ordering_point_define_check: true

                                @Label: Take_Additional_Point
                                @End
                        */
                                @Label: Take_Additional_Point
                                @End
                        */


@@ -201,7 +201,7 @@ int steal(Deque *q) {
                bool succ = atomic_compare_exchange_strong_explicit(&q->top, &t, t + 1,
                        memory_order_seq_cst, memory_order_relaxed);
                /**
                bool succ = atomic_compare_exchange_strong_explicit(&q->top, &t, t + 1,
                        memory_order_seq_cst, memory_order_relaxed);
                /**

-                       @Begin
+                       //@Begin

                        @Commit_point_define_check: succ
                        @Label: Steal_CAS_Top
                        @End
                        @Commit_point_define_check: succ
                        @Label: Steal_CAS_Top
                        @End


@@ -209,7 +209,7 @@ int steal(Deque *q) {
 
                /**
                        @Begin
 
                /**
                        @Begin

-                       @Additional_ordering_point_define_check: !succ
+                       @Additional_ordering_point_define_check: true 

                        @Label: Steal_Additional_Point
                        @End
                */
                        @Label: Steal_Additional_Point
                        @End
                */

diff --git a/benchmark/chase-lev-deque-bugfix/deque.h b/benchmark/chase-lev-deque-bugfix/deque.h
index 0a87de7700c49bb57601de3dff7b8dbe149e2064..7d2df9f18e1732d7e2909cf5ec89faaa7b9afd0b 100644 (file)
--- a/benchmark/chase-lev-deque-bugfix/deque.h
+++ b/benchmark/chase-lev-deque-bugfix/deque.h
@@ -72,7 +72,8 @@ void resize(Deque *q);
 /**
     @Begin
     @Interface: Take 
 /**
     @Begin
     @Interface: Take 

-    @Commit_point_set: Take_Read_Bottom | Take_CAS_Top |Take_Additional_Point
+    //@Commit_point_set: Take_Read_Bottom | Take_CAS_Top | Take_Additional_Point
+    @Commit_point_set: Take_Read_Bottom | 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;


@@ -103,7 +104,8 @@ void push(Deque *q, int x);
 /**
     @Begin
     @Interface: Steal 
 /**
     @Begin
     @Interface: Steal 

-    @Commit_point_set: Steal_Read_Bottom | Steal_CAS_Top | Steal_Additional_Point
+    //@Commit_point_set: Steal_Read_Bottom | Steal_CAS_Top | Steal_Additional_Point
+    @Commit_point_set: Steal_Read_Bottom | 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 6be90a5f7ffe73fc49f731ba6fd80cdf9f48e1f8..fd67b60ec7a02ebf39244821030f541699260737 100644 (file)
--- a/benchmark/chase-lev-deque-bugfix/main.c
+++ b/benchmark/chase-lev-deque-bugfix/main.c
@@ -14,13 +14,18 @@ int b;
 int c;
 
 static void task(void * param) {
 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);
        }
        a=steal(q);
        if (a == ABORT) {
                printf("Steal NULL\n");
        } else {
                printf("Steal %d\n", a);
        }

+       int x=steal(q);
+       if (x == ABORT) {
+               printf("Steal NULL\n");
+       } else {
+               printf("Steal %d\n", x);
+       }

 }
 
 int user_main(int argc, char **argv)
 }
 
 int user_main(int argc, char **argv)