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 tag = new_id_tag(); // Beginning of available id
42 tag_elem_t* new_tag_elem(call_id_t id, int data) {
43 tag_elem_t *e = (tag_elem_t*) CMODEL_MALLOC(sizeof(tag_elem_t));
49 call_id_t get_id(void *wrapper) {
50 tag_elem_t *res = (tag_elem_t*) wrapper;
52 //model_print("wrong id here\n");
58 int get_data(void *wrapper) {
59 tag_elem_t *res = (tag_elem_t*) wrapper;
70 void resize(Deque *q);
75 @Commit_point_set: Take_Read_Bottom | Take_CAS_Top |Take_Additional_Point
76 @ID: __RET__ == EMPTY ? DEFAULT_CALL_ID : get_id(back(__deque))
79 if (__RET__ != EMPTY) {
80 if (size(__deque) > 0) {
81 _Old_Val = get_data(back(__deque));
94 @Commit_point_set: Push_Update_Bottom
95 @ID: get_and_inc(tag);
97 tag_elem_t *elem = new_tag_elem(__ID__, x);
98 push_back(__deque, elem);
101 void push(Deque *q, int x);
106 @Commit_point_set: Steal_Read_Bottom | Steal_CAS_Top | Steal_Additional_Point
107 @ID: (__RET__ == EMPTY || __RET__ == ABORT) ? DEFAULT_CALL_ID : get_id(front(__deque))
109 int _Old_Val = EMPTY;
110 if (__RET__ != EMPTY && __RET__ != ABORT) {
111 if (size(__deque) > 0) {
112 _Old_Val = get_data(front(__deque));
117 _Old_Val == __RET__ || __RET__ == EMPTY || __RET__ == ABORT