changes

[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 c9fc8a9327f5d2a20fe623ba796527fe6cd52f81..4dcb9bbd156fe3581452fbec1dd6ff3291ef8463 100644 (file)
--- a/benchmark/chase-lev-deque-bugfix/deque.c
+++ b/benchmark/chase-lev-deque-bugfix/deque.c
@@ -99,20 +99,32 @@ void push(Deque *q, int x) {
                resize(q);
                //Bug in paper...should have next line...
                a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
+               /**
+                       @Begin
+                       @Commit_point_define_check: true
+                       @Label: Push_Read_Array
+                       @End
+               */
        }
        int size = atomic_load_explicit(&a->size, memory_order_relaxed);
+
        atomic_store_explicit(&a->buffer[b % size], x, memory_order_relaxed);
        /**
                @Begin
                @Commit_point_define_check: true
-               @Label: Push_Point
+               @Label: Push_Update_Buffer
                @End
        */
        /**** correctness error ****/
        atomic_thread_fence(memory_order_release);
        
        atomic_store_explicit(&q->bottom, b + 1, memory_order_relaxed);
-       
+       /**
+               @Begin
+               @Commit_point_define_check: true
+               @Label: Push_Update_Bottom
+               @End
+       */
 }
 
 /**