8 #include <cdsannotate.h>
9 #include <specannotation.h>
10 #include <model_memory.h>
15 typedef unsigned long long pointer;
16 typedef atomic_ullong pointer_t;
18 #define MAKE_POINTER(ptr, count) ((((pointer)count) << 32) | ptr)
19 #define PTR_MASK 0xffffffffLL
20 #define COUNT_MASK (0xffffffffLL << 32)
22 static inline void set_count(pointer *p, unsigned int val) { *p = (*p & ~COUNT_MASK) | ((pointer)val << 32); }
23 static inline void set_ptr(pointer *p, unsigned int val) { *p = (*p & ~PTR_MASK) | val; }
24 static inline unsigned int get_count(pointer p) { return (p & COUNT_MASK) >> 32; }
25 static inline unsigned int get_ptr(pointer p) { return p & PTR_MASK; }
35 node_t nodes[MAX_NODES + 1];
38 void init_queue(queue_t *q, int num_threads);
46 typedef struct tag_elem {
55 __queue = new_spec_list();
56 tag = new_id_tag(); // Beginning of available id
59 // free_spec_list(__queue);
63 tag_elem_t* new_tag_elem(call_id_t id, unsigned int data) {
64 tag_elem_t *e = (tag_elem_t*) CMODEL_MALLOC(sizeof(tag_elem_t));
70 // void free_tag_elem(tag_elem_t *e) {
74 call_id_t get_id(void *wrapper) {
75 // if (wrapper == NULL)
77 // return ((tag_elem_t*) wrapper)->id;
78 return wrapper == NULL ? 0 : ((tag_elem_t*) wrapper)->id;
81 unsigned int get_data(void *wrapper) {
82 return ((tag_elem_t*) wrapper)->data;
84 @Happens_before: Enqueue -> Dequeue
85 # Only check the happens-before relationship according to the id of the
86 # commit_point_set. For commit_point_set that has same ID, A -> B means
87 # B happens after the previous A.
88 @Commutativity: Enqueue <-> Dequeue: _Method1.__RET__ == NULL
89 @Commutativity: Enqueue <-> Dequeue: _Method1.q != _Method2.q
98 @Commit_point_set: Enqueue_Read_Tail | Enqueue_UpdateNext | Enqueue_Additional_Tail_LoadOrCAS
101 # __ID__ is an internal macro that refers to the id of the current
103 tag_elem_t *elem = new_tag_elem(__ID__, val);
104 push_back(__queue, elem);
105 //model_print("Enqueue: input=%d\n", val);
108 void enqueue(queue_t *q, unsigned int val);
113 @Commit_point_set: Dequeue_Read_Head | Dequeue_Read_Tail | Dequeue_LoadNext
114 @ID: get_id(front(__queue))
116 unsigned int _Old_Val = 0;
117 if (size(__queue) > 0) {
118 _Old_Val = get_data(front(__queue));
121 // model_print("Dequeue: __RET__=%d, retVal=%d, Old_Val=%d\n", __RET__, *retVal, _Old_Val);
122 @Post_check: _Old_Val == 0 ? !__RET__ : _Old_Val == *retVal
125 bool dequeue(queue_t *q, int *retVal);
126 int get_thread_num();