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);
40 /* All other user-defined structs */
41 static IntegerList * __queue;
42 /* All other user-defined functions */
43 /* Definition of interface info struct: Dequeue */
44 typedef struct Dequeue_info {
49 /* End of info struct definition: Dequeue */
51 /* ID function of interface: Dequeue */
52 inline static call_id_t Dequeue_id(void *info, thread_id_t __TID__) {
53 Dequeue_info* theInfo = (Dequeue_info*)info;
54 bool __RET__ = theInfo->__RET__;
55 queue_t * q = theInfo->q;
56 int * retVal = theInfo->retVal;
58 call_id_t __ID__ = __RET__ ? * retVal : 0;
61 /* End of ID function: Dequeue */
63 /* Check action function of interface: Dequeue */
64 inline static bool Dequeue_check_action(void *info, call_id_t __ID__, thread_id_t __TID__) {
66 Dequeue_info* theInfo = (Dequeue_info*)info;
67 bool __RET__ = theInfo->__RET__;
68 queue_t * q = theInfo->q;
69 int * retVal = theInfo->retVal;
73 elem = front ( __queue ) ;
74 pop_front ( __queue ) ;
76 check_passed = __RET__ ? * retVal == elem : true;
81 /* End of check action function: Dequeue */
83 /* Definition of interface info struct: Enqueue */
84 typedef struct Enqueue_info {
88 /* End of info struct definition: Enqueue */
90 /* ID function of interface: Enqueue */
91 inline static call_id_t Enqueue_id(void *info, thread_id_t __TID__) {
92 Enqueue_info* theInfo = (Enqueue_info*)info;
93 queue_t * q = theInfo->q;
94 unsigned int val = theInfo->val;
96 call_id_t __ID__ = val;
99 /* End of ID function: Enqueue */
101 /* Check action function of interface: Enqueue */
102 inline static bool Enqueue_check_action(void *info, call_id_t __ID__, thread_id_t __TID__) {
104 Enqueue_info* theInfo = (Enqueue_info*)info;
105 queue_t * q = theInfo->q;
106 unsigned int val = theInfo->val;
108 push_back ( __queue , val ) ;
111 /* End of check action function: Enqueue */
113 #define INTERFACE_SIZE 2
114 static void** func_ptr_table;
115 static hb_rule** hb_rule_table;
116 static commutativity_rule** commutativity_rule_table;
117 inline static bool CommutativityCondition0(void *info1, void *info2) {
118 Enqueue_info *_info1 = (Enqueue_info*) info1;
119 Dequeue_info *_info2 = (Dequeue_info*) info2;
122 inline static bool CommutativityCondition1(void *info1, void *info2) {
123 Dequeue_info *_info1 = (Dequeue_info*) info1;
124 Dequeue_info *_info2 = (Dequeue_info*) info2;
125 return ! _info1-> __RET__ || ! _info2-> __RET__;
128 /* Initialization of sequential varialbes */
129 static void __SPEC_INIT__() {
130 __queue = createIntegerList ( ) ;
133 /* Cleanup routine of sequential variables */
134 static bool __SPEC_CLEANUP__() {
135 if ( __queue ) destroyIntegerList ( __queue ) ;
139 /* Define function for sequential code initialization */
140 inline static void __sequential_init() {
141 /* Init func_ptr_table */
142 func_ptr_table = (void**) malloc(sizeof(void*) * 2 * 2);
143 func_ptr_table[2 * 1] = (void*) &Dequeue_id;
144 func_ptr_table[2 * 1 + 1] = (void*) &Dequeue_check_action;
145 func_ptr_table[2 * 0] = (void*) &Enqueue_id;
146 func_ptr_table[2 * 0 + 1] = (void*) &Enqueue_check_action;
147 /* Enqueue(true) -> Dequeue(true) */
148 struct hb_rule *hbConditionInit0 = (struct hb_rule*) malloc(sizeof(struct hb_rule));
149 hbConditionInit0->interface_num_before = 0; // Enqueue
150 hbConditionInit0->hb_condition_num_before = 0; //
151 hbConditionInit0->interface_num_after = 1; // Dequeue
152 hbConditionInit0->hb_condition_num_after = 0; //
153 /* Init hb_rule_table */
154 hb_rule_table = (hb_rule**) malloc(sizeof(hb_rule*) * 1);
155 #define HB_RULE_TABLE_SIZE 1
156 hb_rule_table[0] = hbConditionInit0;
157 /* Init commutativity_rule_table */
158 commutativity_rule_table = (commutativity_rule**) malloc(sizeof(commutativity_rule*) * 2);
159 commutativity_rule* rule;
160 rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
161 rule->interface_num_before = 0;
162 rule->interface_num_after = 1;
164 rule->condition = CommutativityCondition0;
165 commutativity_rule_table[0] = rule;
166 rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
167 rule->interface_num_before = 1;
168 rule->interface_num_after = 1;
169 rule->rule = "! _Method1 . __RET__ || ! _Method2 . __RET__";
170 rule->condition = CommutativityCondition1;
171 commutativity_rule_table[1] = rule;
172 /* Pass init info, including function table info & HB rules & Commutativity Rules */
173 struct anno_init *anno_init = (struct anno_init*) malloc(sizeof(struct anno_init));
174 anno_init->init_func = (void_func_t) __SPEC_INIT__;
175 anno_init->cleanup_func = (cleanup_func_t) __SPEC_CLEANUP__;
176 anno_init->func_table = func_ptr_table;
177 anno_init->func_table_size = INTERFACE_SIZE;
178 anno_init->hb_rule_table = hb_rule_table;
179 anno_init->hb_rule_table_size = HB_RULE_TABLE_SIZE;
180 anno_init->commutativity_rule_table = commutativity_rule_table;
181 anno_init->commutativity_rule_table_size = 2;
182 struct spec_annotation *init = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
184 init->annotation = anno_init;
185 cdsannotate(SPEC_ANALYSIS, init);
189 /* End of Global construct generation in class */
194 void __wrapper__enqueue(queue_t * q, unsigned int val);
196 void __wrapper__enqueue(queue_t * q, unsigned int val) ;
198 bool __wrapper__dequeue(queue_t * q, int * retVal);
200 bool __wrapper__dequeue(queue_t * q, int * retVal) ;
201 int get_thread_num();