6 #include <cdsannotate.h>
7 #include <specannotation.h>
8 #include <model_memory.h>
17 atomic_size_t top, bottom;
18 atomic_uintptr_t array; /* Atomic(Array *) */
21 #define EMPTY 0xffffffff
22 #define ABORT 0xfffffffe
30 typedef struct tag_elem {
39 __deque = new_spec_list();
40 //model_print("init_list\n");
41 tag = new_id_tag(); // Beginning of available id
44 //free_spec_list(__deque);
45 //model_print("free_list\n");
50 tag_elem_t* new_tag_elem(call_id_t id, int data) {
51 tag_elem_t *e = (tag_elem_t*) CMODEL_MALLOC(sizeof(tag_elem_t));
57 call_id_t get_id(void *wrapper) {
58 //tag_elem_t *res = (tag_elem_t*) wrapper;
59 return res == NULL ? 0 : ((tag_elem_t*) wrapper)->id;
61 //model_print("wrong id here\n");
67 int get_data(void *wrapper) {
68 //tag_elem_t *res = (tag_elem_t*) wrapper;
70 return ((tag_elem_t*) wrapper)->data;
80 void resize(Deque *q);
85 //@Commit_point_set: Take_Read_Bottom | Take_CAS_Top | Take_Additional_Point
86 @Commit_point_set: Take_Read_Bottom | Take_Additional_Point
87 @ID: __RET__ == EMPTY ? DEFAULT_CALL_ID : get_id(back(__deque))
90 if (__RET__ != EMPTY && size(__deque) > 0) {
91 _Old_Val = get_data(back(__deque));
94 @Post_check: _Old_Val == __RET__
102 @Commit_point_set: Push_Update_Bottom
103 @ID: get_and_inc(tag);
104 @Action: push_back(__deque, new_tag_elem(__ID__, x));
107 void push(Deque *q, int x);
112 //@Commit_point_set: Steal_Read_Bottom | Steal_CAS_Top | Steal_Additional_Point
113 @Commit_point_set: Steal_Read_Bottom | Steal_Additional_Point
114 @ID: (__RET__ == EMPTY || __RET__ == ABORT) ? DEFAULT_CALL_ID : get_id(front(__deque))
116 int _Old_Val = EMPTY;
117 if (__RET__ != EMPTY && __RET__ != ABORT && size(__deque) > 0) {
118 _Old_Val = get_data(front(__deque));
122 _Old_Val == __RET__ || __RET__ == EMPTY || __RET__ == ABORT