output/read-copy-update/rcu.cc

   1 #include <atomic>
   2 #include <threads.h>
   3 #include <stdatomic.h>
   4 #include <stdlib.h>
   5 #include <stdio.h>
   6
   7 #include <spec_lib.h>
   8 #include <stdlib.h>
   9 #include <cdsannotate.h>
  10 #include <specannotation.h>
  11 #include <model_memory.h>
  12 #include "common.h"
  13
  14 #include "librace.h"
  15
  16
  17
  18 typedef struct Data {
  19         int data1;
  20         int data2;
  21 } Data;
  22
  23 atomic<Data*> data;
  24
  25 /* All other user-defined structs */
  26 static IntegerList * set;
  27 /* All other user-defined functions */
  28 inline static call_id_t getID ( int64_t d1 , int64_t d2 ) {
  29 return d1 + d2 ;
  30 }
  31
  32 inline static bool print ( int64_t p ) {
  33 Data * d = ( Data * ) p ;
  34 model_print ( "Elem-> d1 = %d, d2 = %d\n" , d -> data1 , d -> data2 ) ;
  35 }
  36 bool equal ( int64_t p1 , int64_t p2 ) {
  37 if ( ! p1 || ! p2 ) return false ;
  38 Data * d1 = ( Data * ) p1 ;
  39 Data * d2 = ( Data * ) p2 ;
  40 if ( d1 -> data1 == d2 -> data1 && d1 -> data2 == d2 -> data2 ) {
  41 return true ;
  42 }
  43 else {
  44 return false ;
  45 }
  46 }
  47
  48 inline static void _write ( int64_t d1 , int64_t d2 ) {
  49 Data * d = ( Data * ) MODEL_MALLOC ( sizeof ( Data ) ) ;
  50 d -> data1 = d1 ;
  51 d -> data2 = d2 ;
  52 push_back ( set , ( int64_t ) d ) ;
  53 }
  54
  55 inline static bool _read ( Data * res ) {
  56 bool hasElem = has_elem_by_value ( set , ( int64_t ) res , & equal ) ;
  57 return hasElem ;
  58 }
  59
  60 /* Definition of interface info struct: Write */
  61 typedef struct Write_info {
  62 Data * __RET__;
  63 int d1;
  64 int d2;
  65 } Write_info;
  66 /* End of info struct definition: Write */
  67
  68 /* ID function of interface: Write */
  69 inline static call_id_t Write_id(void *info, thread_id_t __TID__) {
  70         Write_info* theInfo = (Write_info*)info;
  71         Data * __RET__ = theInfo->__RET__;
  72         int d1 = theInfo->d1;
  73         int d2 = theInfo->d2;
  74
  75         call_id_t __ID__ = getID ( d1 , d2 ) ;;
  76         return __ID__;
  77 }
  78 /* End of ID function: Write */
  79
  80 /* Check action function of interface: Write */
  81 inline static bool Write_check_action(void *info, call_id_t __ID__, thread_id_t __TID__) {
  82         bool check_passed;
  83         Write_info* theInfo = (Write_info*)info;
  84         Data * __RET__ = theInfo->__RET__;
  85         int d1 = theInfo->d1;
  86         int d2 = theInfo->d2;
  87
  88         _write ( d1 , d2 ) ;
  89         return true;
  90 }
  91 /* End of check action function: Write */
  92
  93 /* Definition of interface info struct: Read */
  94 typedef struct Read_info {
  95 Data * __RET__;
  96 } Read_info;
  97 /* End of info struct definition: Read */
  98
  99 /* ID function of interface: Read */
 100 inline static call_id_t Read_id(void *info, thread_id_t __TID__) {
 101         Read_info* theInfo = (Read_info*)info;
 102         Data * __RET__ = theInfo->__RET__;
 103
 104         call_id_t __ID__ = getID ( __RET__ -> data1 , __RET__ -> data2 );
 105         return __ID__;
 106 }
 107 /* End of ID function: Read */
 108
 109 /* Check action function of interface: Read */
 110 inline static bool Read_check_action(void *info, call_id_t __ID__, thread_id_t __TID__) {
 111         bool check_passed;
 112         Read_info* theInfo = (Read_info*)info;
 113         Data * __RET__ = theInfo->__RET__;
 114
 115         check_passed = _read ( __RET__ ) ;;
 116         if (!check_passed)
 117                 return false;
 118         return true;
 119 }
 120 /* End of check action function: Read */
 121
 122 #define INTERFACE_SIZE 2
 123 static void** func_ptr_table;
 124 static hb_rule** hb_rule_table;
 125 static commutativity_rule** commutativity_rule_table;
 126 inline static bool CommutativityCondition0(void *info1, void *info2) {
 127         Write_info *_info1 = (Write_info*) info1;
 128         Read_info *_info2 = (Read_info*) info2;
 129         return true;
 130 }
 131
 132 /* Initialization of sequential varialbes */
 133 static void __SPEC_INIT__() {
 134         set = createIntegerList ( ) ;
 135         Data * d = ( Data * ) MODEL_MALLOC ( sizeof ( Data ) ) ;
 136         d -> data1 = 0 ;
 137         d -> data2 = 0 ;
 138         push_back ( set , ( int64_t ) d ) ;
 139 }
 140
 141 /* Cleanup routine of sequential variables */
 142 static bool __SPEC_CLEANUP__() {
 143         if ( set ) destroyIntegerList ( set ) ;
 144         return true ;
 145 }
 146
 147 /* Define function for sequential code initialization */
 148 inline static void __sequential_init() {
 149         /* Init func_ptr_table */
 150         func_ptr_table = (void**) malloc(sizeof(void*) * 2 * 2);
 151         func_ptr_table[2 * 1] = (void*) &Write_id;
 152         func_ptr_table[2 * 1 + 1] = (void*) &Write_check_action;
 153         func_ptr_table[2 * 0] = (void*) &Read_id;
 154         func_ptr_table[2 * 0 + 1] = (void*) &Read_check_action;
 155         /* Write(true) -> Read(true) */
 156         struct hb_rule *hbConditionInit0 = (struct hb_rule*) malloc(sizeof(struct hb_rule));
 157         hbConditionInit0->interface_num_before = 1; // Write
 158         hbConditionInit0->hb_condition_num_before = 0; //
 159         hbConditionInit0->interface_num_after = 0; // Read
 160         hbConditionInit0->hb_condition_num_after = 0; //
 161         /* Write(true) -> Write(true) */
 162         struct hb_rule *hbConditionInit1 = (struct hb_rule*) malloc(sizeof(struct hb_rule));
 163         hbConditionInit1->interface_num_before = 1; // Write
 164         hbConditionInit1->hb_condition_num_before = 0; //
 165         hbConditionInit1->interface_num_after = 1; // Write
 166         hbConditionInit1->hb_condition_num_after = 0; //
 167         /* Init hb_rule_table */
 168         hb_rule_table = (hb_rule**) malloc(sizeof(hb_rule*) * 2);
 169         #define HB_RULE_TABLE_SIZE 2
 170         hb_rule_table[0] = hbConditionInit0;
 171         hb_rule_table[1] = hbConditionInit1;
 172         /* Init commutativity_rule_table */
 173         commutativity_rule_table = (commutativity_rule**) malloc(sizeof(commutativity_rule*) * 1);
 174         commutativity_rule* rule;
 175         rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
 176         rule->interface_num_before = 1;
 177         rule->interface_num_after = 0;
 178         rule->rule = "true";
 179         rule->condition = CommutativityCondition0;
 180         commutativity_rule_table[0] = rule;
 181         /* Pass init info, including function table info & HB rules & Commutativity Rules */
 182         struct anno_init *anno_init = (struct anno_init*) malloc(sizeof(struct anno_init));
 183         anno_init->init_func = (void_func_t) __SPEC_INIT__;
 184         anno_init->cleanup_func = (cleanup_func_t) __SPEC_CLEANUP__;
 185         anno_init->func_table = func_ptr_table;
 186         anno_init->func_table_size = INTERFACE_SIZE;
 187         anno_init->hb_rule_table = hb_rule_table;
 188         anno_init->hb_rule_table_size = HB_RULE_TABLE_SIZE;
 189         anno_init->commutativity_rule_table = commutativity_rule_table;
 190         anno_init->commutativity_rule_table_size = 1;
 191         struct spec_annotation *init = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 192         init->type = INIT;
 193         init->annotation = anno_init;
 194         cdsannotate(SPEC_ANALYSIS, init);
 195
 196 }
 197
 198 /* End of Global construct generation in class */
 199
 200
 201 Data * __wrapper__read();
 202
 203 Data * read() {
 204         /* Interface begins */
 205         struct anno_interface_begin *interface_begin = (struct anno_interface_begin*) malloc(sizeof(struct anno_interface_begin));
 206         interface_begin->interface_num = 0; // Read
 207                 interface_begin->interface_name = "Read";
 208         struct spec_annotation *annotation_interface_begin = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 209         annotation_interface_begin->type = INTERFACE_BEGIN;
 210         annotation_interface_begin->annotation = interface_begin;
 211         cdsannotate(SPEC_ANALYSIS, annotation_interface_begin);
 212         Data * __RET__ = __wrapper__read();
 213         struct anno_hb_condition *hb_condition = (struct anno_hb_condition*) malloc(sizeof(struct anno_hb_condition));
 214         hb_condition->interface_num = 0; // Read
 215         hb_condition->hb_condition_num = 0;
 216         struct spec_annotation *annotation_hb_condition = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 217         annotation_hb_condition->type = HB_CONDITION;
 218         annotation_hb_condition->annotation = hb_condition;
 219         cdsannotate(SPEC_ANALYSIS, annotation_hb_condition);
 220
 221         Read_info* info = (Read_info*) malloc(sizeof(Read_info));
 222         info->__RET__ = __RET__;
 223         struct anno_interface_end *interface_end = (struct anno_interface_end*) malloc(sizeof(struct anno_interface_end));
 224         interface_end->interface_num = 0; // Read
 225         interface_end->info = info;
 226         struct spec_annotation *annoation_interface_end = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 227         annoation_interface_end->type = INTERFACE_END;
 228         annoation_interface_end->annotation = interface_end;
 229         cdsannotate(SPEC_ANALYSIS, annoation_interface_end);
 230         return __RET__;
 231 }
 232
 233 Data * __wrapper__read() {
 234
 235         Data *res = data.load(memory_order_acquire);
 236         /* Automatically generated code for commit point define check: Read_Success_Point */
 237
 238         if (true) {
 239                 struct anno_cp_define_check *cp_define_check = (struct anno_cp_define_check*) malloc(sizeof(struct anno_cp_define_check));
 240                 cp_define_check->label_num = 0;
 241                 cp_define_check->label_name = "Read_Success_Point";
 242                 cp_define_check->interface_num = 0;
 243                 struct spec_annotation *annotation_cp_define_check = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 244                 annotation_cp_define_check->type = CP_DEFINE_CHECK;
 245                 annotation_cp_define_check->annotation = cp_define_check;
 246                 cdsannotate(SPEC_ANALYSIS, annotation_cp_define_check);
 247         }
 248
 249         return res;
 250 }
 251
 252 Data * __wrapper__write(int d1, int d2);
 253
 254 Data * write(int d1, int d2) {
 255         /* Interface begins */
 256         struct anno_interface_begin *interface_begin = (struct anno_interface_begin*) malloc(sizeof(struct anno_interface_begin));
 257         interface_begin->interface_num = 1; // Write
 258                 interface_begin->interface_name = "Write";
 259         struct spec_annotation *annotation_interface_begin = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 260         annotation_interface_begin->type = INTERFACE_BEGIN;
 261         annotation_interface_begin->annotation = interface_begin;
 262         cdsannotate(SPEC_ANALYSIS, annotation_interface_begin);
 263         Data * __RET__ = __wrapper__write(d1, d2);
 264         struct anno_hb_condition *hb_condition = (struct anno_hb_condition*) malloc(sizeof(struct anno_hb_condition));
 265         hb_condition->interface_num = 1; // Write
 266         hb_condition->hb_condition_num = 0;
 267         struct spec_annotation *annotation_hb_condition = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 268         annotation_hb_condition->type = HB_CONDITION;
 269         annotation_hb_condition->annotation = hb_condition;
 270         cdsannotate(SPEC_ANALYSIS, annotation_hb_condition);
 271
 272         Write_info* info = (Write_info*) malloc(sizeof(Write_info));
 273         info->__RET__ = __RET__;
 274         info->d1 = d1;
 275         info->d2 = d2;
 276         struct anno_interface_end *interface_end = (struct anno_interface_end*) malloc(sizeof(struct anno_interface_end));
 277         interface_end->interface_num = 1; // Write
 278         interface_end->info = info;
 279         struct spec_annotation *annoation_interface_end = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 280         annoation_interface_end->type = INTERFACE_END;
 281         annoation_interface_end->annotation = interface_end;
 282         cdsannotate(SPEC_ANALYSIS, annoation_interface_end);
 283         return __RET__;
 284 }
 285
 286 Data * __wrapper__write(int d1, int d2) {
 287         bool succ = false;
 288         Data *tmp = (Data*) malloc(sizeof(Data));
 289         do {
 290
 291                 Data *prev = data.load(memory_order_acquire);
 292         tmp->data1 = d1;
 293             tmp->data2 = d2;
 294
 295         succ = data.compare_exchange_strong(prev, tmp,
 296             memory_order_release, memory_order_relaxed);
 297         /* Automatically generated code for commit point define check: Write_Success_Point */
 298
 299         if (succ) {
 300                 struct anno_cp_define_check *cp_define_check = (struct anno_cp_define_check*) malloc(sizeof(struct anno_cp_define_check));
 301                 cp_define_check->label_num = 1;
 302                 cp_define_check->label_name = "Write_Success_Point";
 303                 cp_define_check->interface_num = 1;
 304                 struct spec_annotation *annotation_cp_define_check = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
 305                 annotation_cp_define_check->type = CP_DEFINE_CHECK;
 306                 annotation_cp_define_check->annotation = cp_define_check;
 307                 cdsannotate(SPEC_ANALYSIS, annotation_cp_define_check);
 308         }
 309
 310         } while (!succ);
 311                 return tmp;
 312 }
 313
 314
 315 void threadA(void *arg) {
 316         write(1, 0);
 317 }
 318
 319 void threadB(void *arg) {
 320         write(0, 2);
 321 }
 322
 323 void threadC(void *arg) {
 324         write(2, 2);
 325 }
 326
 327 void threadD(void *arg) {
 328         Data *d = read();
 329         printf("ThreadD: d1=%d, d2=%d\n", d->data1, d->data2);
 330 }
 331
 332 int user_main(int argc, char **argv) {
 333         __sequential_init();
 334
 335
 336         thrd_t t1, t2, t3, t4;
 337         Data *dataInit = (Data*) malloc(sizeof(Data));
 338         dataInit->data1 = 0;
 339         dataInit->data2 = 0;
 340         atomic_init(&data, dataInit);
 341
 342         thrd_create(&t1, threadA, NULL);
 343         thrd_create(&t2, threadB, NULL);
 344                 thrd_create(&t4, threadD, NULL);
 345
 346         thrd_join(t1);
 347         thrd_join(t2);
 348                 thrd_join(t4);
 349
 350         return 0;
 351 }
 352