edits

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

diff --git a/benchmark/chase-lev-deque-bugfix/deque.h b/benchmark/chase-lev-deque-bugfix/deque.h
index 82560f18947d28024928e04af8df6cecef11a240..9292e16c997dc8d539f9142d82e721ac8a4b8f23 100644 (file)
--- a/benchmark/chase-lev-deque-bugfix/deque.h
+++ b/benchmark/chase-lev-deque-bugfix/deque.h
@@ -42,6 +42,7 @@ typedef struct {
         Push -> Steal
        @Commutativity: Push <-> Steal: true
        @Commutativity: Take <-> Steal: true
+       @Commutativity: Steal <-> Steal: _Method1.__RET__ == ABORT || _Method2.__RET__ == ABORT
 
     @End
 */
@@ -53,7 +54,7 @@ void resize(Deque *q);
 /**
     @Begin
     @Interface: Take 
-    @Commit_point_set: Take_Read_Bottom | Take_Additional_Point
+    @Commit_point_set: TakeReadBottom | TakeReadBuffer | TakeReadTop
     @ID: succ(__RET__) ? __RET__ : DEFAULT_CALL_ID
     @Action:
                int elem = 0;
@@ -70,7 +71,7 @@ int take(Deque *q);
 /**
     @Begin
     @Interface: Push 
-    @Commit_point_set: Push_Update_Bottom 
+    @Commit_point_set: PushUpdateBuffer
     @ID: x 
     @Action:
                push_back(__deque, x);
@@ -82,7 +83,7 @@ void push(Deque *q, int x);
 /**
     @Begin
     @Interface: Steal 
-    @Commit_point_set: Steal_Read_Bottom | Steal_Additional_Point
+    @Commit_point_set: StealReadTop1 | StealReadTop2 | StealReadBuffer
     @ID: succ(__RET__) ? __RET__ : DEFAULT_CALL_ID
     @Action:
        int elem = 0;