atomic_uintptr_t array; /* Atomic(Array *) */
} Deque;
+#define EMPTY 0xffffffff
+#define ABORT 0xfffffffe
+
+/**
+ @Begin
+ @Options:
+ LANG = C;
+ @Global_define:
+ @DeclareStruct:
+ typedef struct tag_elem {
+ call_id_t id;
+ int data;
+ } tag_elem_t;
+
+ @DeclareVar:
+ spec_list *__deque;
+ id_tag_t *tag;
+ @InitVar:
+ __deque= new_spec_list();
+ tag = new_id_tag(); // Beginning of available id
+ @DefineFunc:
+ tag_elem_t* new_tag_elem(call_id_t id, int data) {
+ tag_elem_t *e = (tag_elem_t*) CMODEL_MALLOC(sizeof(tag_elem_t));
+ e->id = id;
+ e->data = data;
+ return e;
+ }
+ @DefineFunc:
+ call_id_t get_id(void *wrapper) {
+ return ((tag_elem_t*) wrapper)->id;
+ }
+ @DefineFunc:
+ int get_data(void *wrapper) {
+ return ((tag_elem_t*) wrapper)->data;
+ }
+ @Happens_before:
+ Push -> Steal
+ Push -> Take
+ @End
+*/
+
+
Deque * create();
-int take(Deque *q);
void resize(Deque *q);
+
+/**
+ @Begin
+ @Interface: Take
+ @Commit_point_set: Take_Point1 | Take_Point2 | Take_Point3 | Take_Point4
+ @ID: size(__deque) == 0 ? DEFAULT_CALL_ID : get_id(back(__deque))
+ @Action:
+ int _Old_Val = EMPTY;
+ if (size(__deque) > 0) {
+ _Old_Val = get_data(back(__deque));
+ pop_back(__deque);
+ }
+ @Post_check:
+ _Old_Val == __RET__
+ @End
+*/
+int take(Deque *q);
+
+/**
+ @Begin
+ @Interface: Push
+ @Commit_point_set: Push_Point
+ @ID: get_and_inc(tag);
+ @Action:
+ tag_elem_t *elem = new_tag_elem(__ID__, x);
+ push_back(__deque, elem);
+ @End
+*/
void push(Deque *q, int x);
-#define EMPTY 0xffffffff
-#define ABORT 0xfffffffe
+/**
+ @Begin
+ @Interface: Steal
+ @Commit_point_set: Steal_Point1 | Steal_Point2 | Steal_Point3
+ @ID: size(__deque) == 0 ? DEFAULT_CALL_ID : get_id(front(__deque))
+ @Action:
+ int _Old_Val = EMPTY;
+ if (size(__deque) > 0) {
+ _Old_Val = get_data(front(__deque));
+ pop_front(__deque);
+ }
+ @Post_check:
+ _Old_Val == __RET__
+ @End
+*/
+int steal(Deque *q);
#endif