#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[];
atomic_uintptr_t array; /* Atomic(Array *) */
} Deque;
+#define EMPTY 0xffffffff
+#define ABORT 0xfffffffe
+
+/**
+ @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
+
+ @End
+*/
+
+
Deque * create();
-int take(Deque *q);
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);
-#define EMPTY 0xffffffff
-#define ABORT 0xfffffffe
+/**
+ @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