edits

[cdsspec-compiler.git] / benchmark / chase-lev-deque-bugfix / deque.c

diff --git a/benchmark/chase-lev-deque-bugfix/deque.c b/benchmark/chase-lev-deque-bugfix/deque.c
index 854091ff41d9845ebbace331b04eaf0d85f70a79..b4f63171fde4fda413384f3f7eeae90f816fcdab 100644 (file)
--- a/benchmark/chase-lev-deque-bugfix/deque.c
+++ b/benchmark/chase-lev-deque-bugfix/deque.c
@@ -36,7 +36,7 @@ int take(Deque *q) {
                @End
        */
        atomic_store_explicit(&q->bottom, b, memory_order_relaxed);
-       /**** detected correctness ****/
+       /**** SPEC (sequential) (testcase1.c) ****/
        atomic_thread_fence(memory_order_seq_cst);
        size_t t = atomic_load_explicit(&q->top, memory_order_relaxed);
        /**
@@ -111,11 +111,12 @@ void resize(Deque *q) {
 */
 void push(Deque *q, int x) {
        size_t b = atomic_load_explicit(&q->bottom, memory_order_relaxed);
-       /**** detected correctness ****/
+       /**** SPEC (sequential) ****/
        size_t t = atomic_load_explicit(&q->top, memory_order_acquire);
        Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
        if (b - t > atomic_load_explicit(&a->size, memory_order_relaxed) - 1) /* Full queue. */ {
                resize(q);
+               // CDSSpec can actually detect the same bug if we avoid the UL error
                //Bug in paper...should have next line...
                a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
                /**
@@ -134,16 +135,18 @@ void push(Deque *q, int x) {
                @Label: Push_Update_Buffer
                @End
        */
-       /**** detected HB error (run with -u100 to avoid the uninitialized bug) ****/
+       /**** SPEC (Sync) (run with -u100 to avoid the uninitialized bug) ****/
        atomic_thread_fence(memory_order_release);
-       
-       atomic_store_explicit(&q->bottom, b + 1, memory_order_relaxed);
+       // Watch out!!! We need to specifiy the fence as the commit point because
+       // the synchronization in C11 actually is established at the fence.
        /**
                @Begin
                @Commit_point_define_check: true
                @Label: Push_Update_Bottom
                @End
        */
+       atomic_store_explicit(&q->bottom, b + 1, memory_order_relaxed);
+       
 }
 
 /**
@@ -152,7 +155,8 @@ void push(Deque *q, int x) {
        @End
 */
 int steal(Deque *q) {
-       //FIXME: weaken the following acquire causes no spec problem
+       //Watch out: actually on need to be an acquire (don't count it)
+       // An old bug
        size_t t = atomic_load_explicit(&q->top, memory_order_acquire);
        /**
                //@Begin
@@ -162,7 +166,7 @@ int steal(Deque *q) {
        */
        //FIXME: remove the fence causes no error and fewer executions..
        atomic_thread_fence(memory_order_seq_cst);
-       /**** detected HB error (run with -u100 to avoid the uninitialized bug) ****/
+       /**** SPEC & UL ****/
        size_t b = atomic_load_explicit(&q->bottom, memory_order_acquire);
        /**
                @Begin
@@ -197,7 +201,7 @@ int steal(Deque *q) {
                        @Label: Steal_Potential_Read_Buffer
                        @End
                */
-               /**** detected correctness failure ****/ 
+               /**** SPEC (sequential) ****/ 
                bool succ = atomic_compare_exchange_strong_explicit(&q->top, &t, t + 1,
                        memory_order_seq_cst, memory_order_relaxed);
                /**