notes/generated_code_examples.txt

   1 ******    Example1:    ******
   2 Global Variable Declaration
   3
   4 /* Include all the header files that contains the interface declaration */
   5 #inlcude <atomic>
   6 #include <memory>
   7 #include <assert.h>
   8
   9 /* Other necessary header files */
  10 #include <stdint.h>
  11 #include <specannotation.h>
  12 #include <spec_lib.h>
  13
  14 /* All other user-defined functions */
  15 ALL_USER_DEFINED_FUNCTIONS  // Make them static
  16
  17 /* Definition of interface info struct (per interface) */
  18 typedef struct Put_info {
  19         shared_ptr<TypeV> __RET__;
  20         TypeK & key;
  21         TypeV & value;
  22 } Put_info;
  23
  24 typedef struct Get_info {
  25         shared_ptr<TypeV> __RET__;
  26         TypeK & key;
  27 } Get_info;
  28 /* End of info struct definition */
  29
  30 /* ID functions of interface */
  31 static id_t Put_id() {
  32         id_t id = PUT_ID;  // Default ID == 0;
  33         return id;
  34 }
  35
  36 static id_t Get_id() {
  37         id_t id = GET_ID;
  38         return id;
  39 }
  40 /* End of ID functions */
  41
  42
  43
  44 /* Check_action function of interfaces */
  45 bool Put_check_action(void *info, id_t __ID__) {
  46         bool check_passed;
  47         Put_info *theInfo = (Put_info) info;
  48         shared_ptr<TypeV> __RET__ = theInfo->__RET__;
  49         TypeK & key = theInfo->key;
  50         TypeV & value = theInfo->value;
  51
  52         // __COND_SAT__
  53         bool __COND_SAT__ = PUT_CONDITION;
  54
  55         // Check
  56         check_passed = PUT_CHECK_EXPRESSION;
  57         if (!check_passed)
  58                 return false;
  59
  60         // Action
  61         PUT_ACTION
  62
  63         // Post_check
  64         check_passed = PUT_POST_CHECK_EXPRESSION;
  65         if (!check_passed)
  66                 return false;
  67
  68         // Post_action
  69         PUT_POST_ACTION
  70 }
  71
  72
  73 bool Get_check_action(void *info, id_t __ID__) {
  74         //...
  75 }
  76 /* End of check_action function definitions */
  77
  78 /* Initialization of interface<->function_ptr table */
  79 #define INTERFACE_SIZE 2
  80 void** func_ptr_table;
  81
  82 /* Beginning of other user-defined variables */
  83 bool lock_acquired;
  84 int reader_lock_cnt;
  85 /* End of other user-defined variables */
  86
  87
  88 /* Define function for sequential code initialization */
  89 void __sequential_init() {
  90         /* Init func_ptr_table */
  91         func_ptr_table = (void**) malloc(sizeof(void*) * 2);
  92         func_ptr_table[0] = (void*) &Put_id;
  93         func_ptr_table[1] = (void*) &Put_check_action;
  94         func_ptr_table[2] = (void*) &Get_id;
  95         func_ptr_table[3] = (void*) &Get_check_action;
  96
  97         /* Init user-defined variables */
  98         lock_acquired = false;
  99         reader_lock_cnt = 0;
 100
 101         /* Pass function table info */
 102         anno_func_table_init func_table;
 103         func_table.size = INTERFACE_SIZE;
 104         func_table.table = func_ptr_table;
 105         spec_annotation func_init;
 106         func_init.type = FUNC_TABLE_INIT;
 107         func_init.annotation = &anno_func_table_init;
 108         cdsannotate(SPEC_ANALYSIS, &func_init);
 109
 110         /* Pass the happens-before initialization here */
 111         /* PutIfAbsent (putIfAbsent_Succ) -> Get (true) */
 112         anno_hb_init hbConditionInit0;
 113         hbConditionInit0.interface_num_before = 1;
 114         hbConditionInit0.hb_condition_num_before = 1;
 115         hbConditionInit0.interface_num_after = 2;
 116         hbConditionInit0.hb_condition_num_after = 0;
 117         spec_annotation hb_init0;
 118         hb_init0.type = HB_INIT;
 119         hb_init0.annotation = &hbConditionInit0;
 120         cdsannotate(SPEC_ANALYSIS, &hb_init0);
 121 }
 122 /* End of Global construct generation in class */
 123
 124 /* The following static field declaration is necessary for class */
 125 template <typename T>
 126 bool CLASS<T>::lock_acquired;
 127
 128 template <typename T>
 129 int CLASS<T>::reader_lock_cnt;
 130 /* End of static field definition */
 131
 132
 133 ******    Example2:    ******
 134 Interface Wrapper
 135
 136 /* Include the header files first */
 137 #include <threads.h>
 138 #include <cdsannotate.h>
 139 #include <specannotation.h>
 140 #include <spec_lib.h>
 141
 142 TypeReturn interfaceName(ARGType1 arg1, ARGType2 arg2)
 143 {
 144         // Interface begins
 145         anno_interface_begin interface_begin;
 146         interface_begin.interface_num = 0; // Interface number
 147         spec_annotation annotation_interface_begin;
 148         annotation_interface_begin.type = INTERFACE_BEGIN;
 149         annotation_interface_begin.annotation = &interface_begin;
 150         cdsannotate(SPEC_ANALYSIS, &annoation_interface_begin);
 151
 152         TypeReturn __RET__ = __wrapper_interfaceName(arg1, arg2);
 153
 154         // HB conditions (if any)
 155         if (HB_CONDITION1) {
 156                 anno_hb_condition hb_condition1;
 157                 hb_condition1.interface_num = 0; // Interface number
 158                 hb_condition1.hb_condition_num = 1; // HB condition number
 159                 spec_annotation annotation_hb_condition;
 160                 annotation_hb_condition.type = HB_CONDITION;
 161                 annotation_hb_condition.annotation = &hb_condition;
 162                 cdsannotate(SPEC_ANALYSIS, &annotation_hb_condition);
 163         }
 164         // And more (if any)
 165
 166         // Interface ends
 167         INTERFACE_LABEL_info info = (INTERFACE_LABEL_info*) malloc(sizeof(INTERFACE_LABEL_info));
 168         info->__RET__ = __RET__;
 169         info->arg1 = arg1;
 170         info->arg2 = arg2;
 171         anno_interface_end interface_end;
 172         interface_end.interface_num = 0; // Interface number
 173         interface_end.info = info; // Info
 174         spec_annotation annotation_interface_end;
 175         annotation_interface_end.type = INTERFACE_END;
 176         annotation_interface_end.annotation = &interface_end;
 177         cdsannotate(SPEC_ANALYSIS, &annoation_interface_end);
 178 }
 179
 180
 181 ******    Example3:    ******
 182 Potential Commit Point
 183
 184
 185 #include <stdint.h>
 186 #include <cdsannotate.h>
 187
 188 /* Should add the __ATOMIC_RET__ if necessary */
 189 uint64_t __ATOMIC_RET = somevar.compare_exchange_explicit(...);
 190
 191 if (POTENTIAL_CP_DEFINE_CONDITION) {
 192         anno_potential_cp_define potential_cp_define;
 193         potential_cp_define.label_num = 1; // Commit point label number
 194         spec_annotation annotation_potential_cp_define;
 195         annotation_potential_cp_define.type = POTENTIAL_CP_DEFINE;
 196         annotation_potential_cp_define.annotation = &potential_cp_define;
 197         cdsannotate(SPEC_ANALYSIS, &annotation_potential_cp_define);
 198 }
 199
 200 ******    Example4:    ******
 201 Commit Point Define
 202
 203 #include <threads.h>
 204 #include <cdsannotate.h>
 205 #include <stdint.h>
 206
 207 /* Should add the __ATOMIC_RET__ if necessary */
 208 uint64_t __ATOMIC_RET = somevar.compare_exchange_explicit(...);
 209
 210 /* For all the interface check at this commit point (if there is multiple
 211  * checks here) */
 212 // Commit point 3 <=> potentialCP 4
 213 if (COMMIT_POINT3_CONDITION) {
 214         anno_cp_define cp_define;
 215         cp_define.label_num = 3;
 216         cp_define.potential_cp_label_num = 1;
 217         spec_annotation annotation_cp_define;
 218         annotation_cp_define.type = CP_DEFINE;
 219         annotation_cp_define.annotation = &cp_define;
 220         cdsannotate(SPEC_ANALYSIS, &annotation_cp_define);
 221 }
 222 // More if there are any
 223
 224 }
 225
 226
 227 *****    Example5:    ******
 228 Commit Point Define Check
 229
 230
 231 #include <threads.h>
 232 #include <cdsannotate.h>
 233 #include <stdint.h>
 234
 235 /* Should add the __ATOMIC_RET__ if necessary */
 236 uint64_t __ATOMIC_RET = somevar.compare_exchange_explicit(...);
 237
 238
 239 /* For all the interface check at this commit point (if there is multiple
 240  * checks here) */
 241 if (COMMIT_POINT3_CONDITION) {
 242         anno_cp_define cp_define;
 243         uint64_t call_sequence_num = get(&__sequential.interface_call_sequence, tid);
 244         bool check_passed = false;
 245         cp_define.check_passed = check_passed;
 246         cp_define.interface_num = interface_num;
 247         cp_define.label_num = 3;
 248         cp_define.call_sequence_num = call_sequence_num;
 249         spec_annotation annotation_cp_define;
 250         annotation_cp_define.type = CP_DEFINE;
 251         annotation_cp_define.annotation = &cp_define;
 252         cdsannotate(SPEC_ANALYSIS, &annotation_cp_define);
 253 }
 254 // More if there are any
 255
 256 }