output/chase-lev-deque-bugfix/deque.h

   1 #ifndef DEQUE_H
   2 #define DEQUE_H
   3
   4 #include <spec_lib.h>
   5 #include <stdlib.h>
   6 #include <cdsannotate.h>
   7 #include <specannotation.h>
   8 #include <model_memory.h>
   9 #include "common.h"
  10
  11 typedef struct {
  12         atomic_size_t size;
  13         atomic_int buffer[];
  14 } Array;
  15
  16 typedef struct {
  17         atomic_size_t top, bottom;
  18         atomic_uintptr_t array;
  19 } Deque;
  20
  21 #define EMPTY 0xffffffff
  22 #define ABORT 0xfffffffe
  23
  24 /* All other user-defined structs */
  25 static IntegerList * __deque;
  26 /* All other user-defined functions */
  27 inline static bool succ ( int res ) {
  28 return res != EMPTY && res != ABORT ;
  29 }
  30
  31 /* Definition of interface info struct: Steal */
  32 typedef struct Steal_info {
  33 int __RET__;
  34 Deque * q;
  35 } Steal_info;
  36 /* End of info struct definition: Steal */
  37
  38 /* ID function of interface: Steal */
  39 inline static call_id_t Steal_id(void *info, thread_id_t __TID__) {
  40         Steal_info* theInfo = (Steal_info*)info;
  41         int __RET__ = theInfo->__RET__;
  42         Deque * q = theInfo->q;
  43
  44         call_id_t __ID__ = succ ( __RET__ ) ? __RET__ : DEFAULT_CALL_ID;
  45         return __ID__;
  46 }
  47 /* End of ID function: Steal */
  48
  49 /* Check action function of interface: Steal */
  50 inline static bool Steal_check_action(void *info, call_id_t __ID__, thread_id_t __TID__) {
  51         bool check_passed;
  52         Steal_info* theInfo = (Steal_info*)info;
  53         int __RET__ = theInfo->__RET__;
  54         Deque * q = theInfo->q;
  55
  56         int elem = 0 ;
  57         if ( succ ( __RET__ ) ) {
  58         elem = front ( __deque ) ;
  59         pop_front ( __deque ) ;
  60         }
  61         check_passed = succ ( __RET__ ) ? __RET__ == elem : true;
  62         if (!check_passed)
  63                 return false;
  64         return true;
  65 }
  66 /* End of check action function: Steal */
  67
  68 /* Definition of interface info struct: Take */
  69 typedef struct Take_info {
  70 int __RET__;
  71 Deque * q;
  72 } Take_info;
  73 /* End of info struct definition: Take */
  74
  75 /* ID function of interface: Take */
  76 inline static call_id_t Take_id(void *info, thread_id_t __TID__) {
  77         Take_info* theInfo = (Take_info*)info;
  78         int __RET__ = theInfo->__RET__;
  79         Deque * q = theInfo->q;
  80
  81         call_id_t __ID__ = succ ( __RET__ ) ? __RET__ : DEFAULT_CALL_ID;
  82         return __ID__;
  83 }
  84 /* End of ID function: Take */
  85
  86 /* Check action function of interface: Take */
  87 inline static bool Take_check_action(void *info, call_id_t __ID__, thread_id_t __TID__) {
  88         bool check_passed;
  89         Take_info* theInfo = (Take_info*)info;
  90         int __RET__ = theInfo->__RET__;
  91         Deque * q = theInfo->q;
  92
  93         int elem = 0 ;
  94         if ( succ ( __RET__ ) ) {
  95         elem = back ( __deque ) ;
  96         pop_back ( __deque ) ;
  97         }
  98         check_passed = succ ( __RET__ ) ? __RET__ == elem : true;
  99         if (!check_passed)
 100                 return false;
 101         return true;
 102 }
 103 /* End of check action function: Take */
 104
 105 /* Definition of interface info struct: Push */
 106 typedef struct Push_info {
 107 Deque * q;
 108 int x;
 109 } Push_info;
 110 /* End of info struct definition: Push */
 111
 112 /* ID function of interface: Push */
 113 inline static call_id_t Push_id(void *info, thread_id_t __TID__) {
 114         Push_info* theInfo = (Push_info*)info;
 115         Deque * q = theInfo->q;
 116         int x = theInfo->x;
 117
 118         call_id_t __ID__ = x;
 119         return __ID__;
 120 }
 121 /* End of ID function: Push */
 122
 123 /* Check action function of interface: Push */
 124 inline static bool Push_check_action(void *info, call_id_t __ID__, thread_id_t __TID__) {
 125         bool check_passed;
 126         Push_info* theInfo = (Push_info*)info;
 127         Deque * q = theInfo->q;
 128         int x = theInfo->x;
 129
 130         push_back ( __deque , x ) ;
 131         return true;
 132 }
 133 /* End of check action function: Push */
 134
 135 #define INTERFACE_SIZE 3
 136 static void** func_ptr_table;
 137 static hb_rule** hb_rule_table;
 138 static commutativity_rule** commutativity_rule_table;
 139 inline static bool CommutativityCondition0(void *info1, void *info2) {
 140         Push_info *_info1 = (Push_info*) info1;
 141         Steal_info *_info2 = (Steal_info*) info2;
 142         return true;
 143 }
 144 inline static bool CommutativityCondition1(void *info1, void *info2) {
 145         Take_info *_info1 = (Take_info*) info1;
 146         Steal_info *_info2 = (Steal_info*) info2;
 147         return true;
 148 }
 149
 150 /* Initialization of sequential varialbes */
 151 static void __SPEC_INIT__() {
 152         __deque = createIntegerList ( ) ;
 153 }
 154
 155 /* Cleanup routine of sequential variables */
 156 static bool __SPEC_CLEANUP__() {
 157         if ( __deque ) destroyIntegerList ( __deque ) ;
 158         return true ;
 159 }
 160
 161 /* Define function for sequential code initialization */
 162 inline static void __sequential_init() {
 163         /* Init func_ptr_table */
 164         func_ptr_table = (void**) malloc(sizeof(void*) * 3 * 2);
 165         func_ptr_table[2 * 2] = (void*) &Steal_id;
 166         func_ptr_table[2 * 2 + 1] = (void*) &Steal_check_action;
 167         func_ptr_table[2 * 0] = (void*) &Take_id;
 168         func_ptr_table[2 * 0 + 1] = (void*) &Take_check_action;
 169         func_ptr_table[2 * 1] = (void*) &Push_id;
 170         func_ptr_table[2 * 1 + 1] = (void*) &Push_check_action;
 171         /* Push(true) -> Steal(true) */
 172         struct hb_rule *hbConditionInit0 = (struct hb_rule*) malloc(sizeof(struct hb_rule));
 173         hbConditionInit0->interface_num_before = 1; // Push
 174         hbConditionInit0->hb_condition_num_before = 0; //
 175         hbConditionInit0->interface_num_after = 2; // Steal
 176         hbConditionInit0->hb_condition_num_after = 0; //
 177         /* Init hb_rule_table */
 178         hb_rule_table = (hb_rule**) malloc(sizeof(hb_rule*) * 1);
 179         #define HB_RULE_TABLE_SIZE 1
 180         hb_rule_table[0] = hbConditionInit0;
 181         /* Init commutativity_rule_table */
 182         commutativity_rule_table = (commutativity_rule**) malloc(sizeof(commutativity_rule*) * 2);
 183         commutativity_rule* rule;
 184         rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
 185         rule->interface_num_before = 1;
 186         rule->interface_num_after = 2;
 187         rule->rule = "true";
 188         rule->condition = CommutativityCondition0;
 189         commutativity_rule_table[0] = rule;
 190         rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
 191         rule->interface_num_before = 0;
 192         rule->interface_num_after = 2;
 193         rule->rule = "true";
 194         rule->condition = CommutativityCondition1;
 195         commutativity_rule_table[1] = rule;
 196         /* Pass init info, including function table info & HB rules & Commutativity Rules */
 197         struct anno_init *anno_init = (struct anno_init*) malloc(sizeof(struct anno_init));
 198         anno_init->init_func = (void_func_t) __SPEC_INIT__;
 199         anno_init->cleanup_func = (cleanup_func_t) __SPEC_CLEANUP__;
 200         anno_init->func_table = func_ptr_table;
 201         anno_init->func_table_size = INTERFACE_SIZE;
 202         anno_init->hb_rule_table = hb_rule_table;
 203         anno_init->hb_rule_table_size = HB_RULE_TABLE_SIZE;
 204         anno_init->commutativity_rule_table = commutativity_rule_table;
 205         anno_init->commutativity_rule_table_size = 2;
 206         struct spec_annotation *init = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 207         init->type = INIT;
 208         init->annotation = anno_init;
 209         cdsannotate(SPEC_ANALYSIS, init);
 210
 211 }
 212
 213 /* End of Global construct generation in class */
 214
 215
 216
 217 Deque * create();
 218 void resize(Deque *q);
 219
 220 int __wrapper__take(Deque * q);
 221
 222 int __wrapper__take(Deque * q) ;
 223
 224 void __wrapper__push(Deque * q, int x);
 225
 226 void __wrapper__push(Deque * q, int x) ;
 227
 228 int __wrapper__steal(Deque * q);
 229
 230 int __wrapper__steal(Deque * q) ;
 231
 232 #endif
 233