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 return ((tag_elem_t*) wrapper)->id;
53 int get_data(void *wrapper) {
54 return ((tag_elem_t*) wrapper)->data;
64 void resize(Deque *q);
69 @Commit_point_set: Take_Point1 | Take_Point2 | Take_Point3
70 @ID: __RET__ == EMPTY ? DEFAULT_CALL_ID : get_id(back(__deque))
73 if (__RET__ != EMPTY) {
74 if (size(__deque) > 0) {
75 _Old_Val = get_data(back(__deque));
88 @Commit_point_set: Push_Point
89 @ID: get_and_inc(tag);
91 tag_elem_t *elem = new_tag_elem(__ID__, x);
92 push_back(__deque, elem);
95 void push(Deque *q, int x);
100 @Commit_point_set: Steal_Point1 | Steal_Point2 | Steal_Point3
101 @ID: (__RET__ == EMPTY || __RET__ == ABORT) ? DEFAULT_CALL_ID : get_id(front(__deque))
103 int _Old_Val = EMPTY;
104 if (__RET__ != EMPTY && __RET__ != ABORT) {
105 if (size(__deque) > 0) {
106 _Old_Val = get_data(front(__deque));
111 _Old_Val == __RET__ || __RET__ == EMPTY || __RET__ == ABORT