output/ms-queue/my_queue.h

   1 #ifndef _MY_QUEUE_H
   2 #define _MY_QUEUE_H
   3
   4 #include <stdatomic.h>
   5
   6 #include <spec_lib.h>
   7 #include <stdlib.h>
   8 #include <cdsannotate.h>
   9 #include <specannotation.h>
  10 #include <model_memory.h>
  11 #include "common.h"
  12
  13 #define MAX_NODES                       0xf
  14
  15 typedef unsigned long long pointer;
  16 typedef atomic_ullong pointer_t;
  17
  18 #define MAKE_POINTER(ptr, count)        ((((pointer)count) << 32) | ptr)
  19 #define PTR_MASK 0xffffffffLL
  20 #define COUNT_MASK (0xffffffffLL << 32)
  21
  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; }
  26
  27 typedef struct node {
  28         unsigned int value;
  29         pointer_t next;
  30 } node_t;
  31
  32 typedef struct {
  33         pointer_t head;
  34         pointer_t tail;
  35         node_t nodes[MAX_NODES + 1];
  36 } queue_t;
  37
  38 void init_queue(queue_t *q, int num_threads);
  39
  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 {
  45 bool __RET__;
  46 queue_t * q;
  47 int * retVal;
  48 } Dequeue_info;
  49 /* End of info struct definition: Dequeue */
  50
  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;
  57
  58         call_id_t __ID__ = __RET__ ? * retVal : 0;
  59         return __ID__;
  60 }
  61 /* End of ID function: Dequeue */
  62
  63 /* Check action function of interface: Dequeue */
  64 inline static bool Dequeue_check_action(void *info, call_id_t __ID__, thread_id_t __TID__) {
  65         bool check_passed;
  66         Dequeue_info* theInfo = (Dequeue_info*)info;
  67         bool __RET__ = theInfo->__RET__;
  68         queue_t * q = theInfo->q;
  69         int * retVal = theInfo->retVal;
  70
  71         int elem = 0 ;
  72         if ( __RET__ ) {
  73         elem = front ( __queue ) ;
  74         pop_front ( __queue ) ;
  75         }
  76         check_passed = __RET__ ? * retVal == elem : true;
  77         if (!check_passed)
  78                 return false;
  79         return true;
  80 }
  81 /* End of check action function: Dequeue */
  82
  83 /* Definition of interface info struct: Enqueue */
  84 typedef struct Enqueue_info {
  85 queue_t * q;
  86  unsigned int val;
  87 } Enqueue_info;
  88 /* End of info struct definition: Enqueue */
  89
  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;
  95
  96         call_id_t __ID__ = val;
  97         return __ID__;
  98 }
  99 /* End of ID function: Enqueue */
 100
 101 /* Check action function of interface: Enqueue */
 102 inline static bool Enqueue_check_action(void *info, call_id_t __ID__, thread_id_t __TID__) {
 103         bool check_passed;
 104         Enqueue_info* theInfo = (Enqueue_info*)info;
 105         queue_t * q = theInfo->q;
 106          unsigned int val = theInfo->val;
 107
 108         push_back ( __queue , val ) ;
 109         return true;
 110 }
 111 /* End of check action function: Enqueue */
 112
 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;
 120         return true;
 121 }
 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__;
 126 }
 127
 128 /* Initialization of sequential varialbes */
 129 static void __SPEC_INIT__() {
 130         __queue = createIntegerList ( ) ;
 131 }
 132
 133 /* Cleanup routine of sequential variables */
 134 static bool __SPEC_CLEANUP__() {
 135         if ( __queue ) destroyIntegerList ( __queue ) ;
 136         return true ;
 137 }
 138
 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;
 163         rule->rule = "true";
 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));
 183         init->type = INIT;
 184         init->annotation = anno_init;
 185         cdsannotate(SPEC_ANALYSIS, init);
 186
 187 }
 188
 189 /* End of Global construct generation in class */
 190
 191
 192
 193
 194 void __wrapper__enqueue(queue_t * q,  unsigned int val);
 195
 196 void __wrapper__enqueue(queue_t * q,  unsigned int val) ;
 197
 198 bool __wrapper__dequeue(queue_t * q, int * retVal);
 199
 200 bool __wrapper__dequeue(queue_t * q, int * retVal) ;
 201 int get_thread_num();
 202
 203 #endif
 204