fixed command line

[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
deleted file mode 100644 (file)
index 4d1f34e..0000000
--- a/benchmark/chase-lev-deque-bugfix/deque.h
+++ /dev/null
@@ -1,101 +0,0 @@
-#ifndef DEQUE_H
-#define DEQUE_H
-
-#include <spec_lib.h>
-#include <stdlib.h>
-#include <cdsannotate.h>
-#include <specannotation.h>
-#include <model_memory.h>
-#include "common.h"
-
-typedef struct {
-       atomic_size_t size;
-       atomic_int buffer[];
-} Array;
-
-typedef struct {
-       atomic_size_t top, bottom;
-       atomic_uintptr_t array; /* Atomic(Array *) */
-} Deque;
-
-#define EMPTY 0xffffffff
-#define ABORT 0xfffffffe
-
-inline bool fail(int ret);
-/**
-    @Begin
-    @Options:
-        LANG = C;
-    @Global_define:
-        @DeclareVar:
-                       IntegerList *__deque;
-        @InitVar:
-                       __deque = createIntegerList();
-               @Finalize:
-                       if (__deque)
-                               destroyIntegerList(__deque);
-                       return true;
-               @DefineFunc:
-                       bool succ(int res) {
-                               return res != EMPTY && res != ABORT;
-                       }
-    @Happens_before:
-        Push -> Steal
-       @Commutativity: Push <-> Steal: true
-       @Commutativity: Take <-> Steal: true
-       @Commutativity: Steal <-> Steal: fail(_Method1.__RET__) || fail(_Method2.__RET__)
-
-    @End
-*/
-
-
-Deque * create();
-void resize(Deque *q);
-
-/**
-    @Begin
-    @Interface: Take 
-    @Commit_point_set: TakeReadBottom | TakeReadBuffer | TakeReadTop
-    @ID: succ(__RET__) ? __RET__ : DEFAULT_CALL_ID
-    @Action:
-               int elem = 0;
-       if (succ(__RET__)) {
-                       elem = back(__deque);
-                       pop_back(__deque);
-                       //model_print("take: elem=%d, __RET__=%d\n", elem, __RET__);
-               }
-    @Post_check: succ(__RET__) ? __RET__ == elem : true
-    @End
-*/
-int take(Deque *q);
-
-/**
-    @Begin
-    @Interface: Push 
-    @Commit_point_set: PushUpdateBuffer
-    @ID: x 
-    @Action:
-               push_back(__deque, x);
-               //model_print("push: elem=%d\n", x);
-    @End
-*/
-void push(Deque *q, int x);
-
-/**
-    @Begin
-    @Interface: Steal 
-    @Commit_point_set: StealReadTop1 | StealReadTop2 | StealReadBuffer
-    @ID: succ(__RET__) ? __RET__ : DEFAULT_CALL_ID
-    @Action:
-       int elem = 0;
-       if (succ(__RET__)) {
-                       elem = front(__deque);
-                       pop_front(__deque);
-                       //model_print("steal: elem=%d, __RET__=%d\n", elem, __RET__);
-               }
-    @Post_check: succ(__RET__) ? __RET__ == elem : true
-    @End
-*/
-int steal(Deque *q);
-
-#endif