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 the happens-before initialization here */
 102         /* PutIfAbsent (putIfAbsent_Succ) -> Get (true) */
 103         anno_hb_init hbConditionInit0;
 104         hbConditionInit0.interface_num_before = 1;
 105         hbConditionInit0.hb_condition_num_before = 1;
 106         hbConditionInit0.interface_num_after = 2;
 107         hbConditionInit0.hb_condition_num_after = 0;
 108         spec_annotation hb_init0;
 109         hb_init0.type = HB_INIT;
 110         hb_init0.annotation = &hbConditionInit0;
 111         cdsannotate(SPEC_ANALYSIS, &hb_init0);
 112 }
 113 /* End of Global construct generation in class */
 114
 115 /* The following static field declaration is necessary for class */
 116 template <typename T>
 117 bool CLASS<T>::lock_acquired;
 118
 119 template <typename T>
 120 int CLASS<T>::reader_lock_cnt;
 121 /* End of static field definition */
 122
 123
 124 ******    Example2:    ******
 125 Interface Wrapper
 126
 127 /* Include the header files first */
 128 #include <threads.h>
 129 #include <cdsannotate.h>
 130 #include <specannotation.h>
 131 #include <spec_lib.h>
 132
 133 TypeReturn interfaceName(ARGType1 arg1, ARGType2 arg2)
 134 {
 135         // Interface begins
 136         anno_interface_begin interface_begin;
 137         interface_begin.interface_num = 0; // Interface number
 138         spec_annotation annotation_interface_begin;
 139         annotation_interface_begin.type = INTERFACE_BEGIN;
 140         annotation_interface_begin.annotation = &interface_begin;
 141         cdsannotate(SPEC_ANALYSIS, &annoation_interface_begin);
 142
 143         TypeReturn __RET__ = __wrapper_interfaceName(arg1, arg2);
 144
 145         // HB conditions (if any)
 146         if (HB_CONDITION1) {
 147                 anno_hb_condition hb_condition1;
 148                 hb_condition1.interface_num = 0; // Interface number
 149                 hb_condition1.hb_condition_num = 1; // HB condition number
 150                 spec_annotation annotation_hb_condition;
 151                 annotation_hb_condition.type = HB_CONDITION;
 152                 annotation_hb_condition.annotation = &hb_condition;
 153                 cdsannotate(SPEC_ANALYSIS, &annotation_hb_condition);
 154         }
 155         // And more (if any)
 156
 157         // Interface ends
 158         INTERFACE_LABEL_info info = (INTERFACE_LABEL_info*) malloc(sizeof(INTERFACE_LABEL_info));
 159         info->__RET__ = __RET__;
 160         info->arg1 = arg1;
 161         info->arg2 = arg2;
 162         anno_interface_end interface_end;
 163         interface_end.interface_num = 0; // Interface number
 164         interface_end.info = info; // Info
 165         spec_annotation annotation_interface_end;
 166         annotation_interface_end.type = INTERFACE_END;
 167         annotation_interface_end.annotation = &interface_end;
 168         cdsannotate(SPEC_ANALYSIS, &annoation_interface_end);
 169 }
 170
 171
 172 ******    Example3:    ******
 173 Potential Commit Point
 174
 175
 176 #include <stdint.h>
 177 #include <cdsannotate.h>
 178
 179 /* Should add the __ATOMIC_RET__ if necessary */
 180 uint64_t __ATOMIC_RET = somevar.compare_exchange_explicit(...);
 181
 182 if (POTENTIAL_CP_DEFINE_CONDITION) {
 183         anno_potential_cp_define potential_cp_define;
 184         potential_cp_define.label_num = 1; // Commit point label number
 185         spec_annotation annotation_potential_cp_define;
 186         annotation_potential_cp_define.type = POTENTIAL_CP_DEFINE;
 187         annotation_potential_cp_define.annotation = &potential_cp_define;
 188         cdsannotate(SPEC_ANALYSIS, &annotation_potential_cp_define);
 189 }
 190
 191 ******    Example4:    ******
 192 Commit Point Define
 193
 194 #include <threads.h>
 195 #include <cdsannotate.h>
 196 #include <stdint.h>
 197
 198 /* Should add the __ATOMIC_RET__ if necessary */
 199 uint64_t __ATOMIC_RET = somevar.compare_exchange_explicit(...);
 200
 201 /* For all the interface check at this commit point (if there is multiple
 202  * checks here) */
 203 // Commit point 3 <=> potentialCP 4
 204 if (COMMIT_POINT3_CONDITION) {
 205         anno_cp_define cp_define;
 206         cp_define.label_num = 3;
 207         cp_define.potential_cp_label_num = 1;
 208         spec_annotation annotation_cp_define;
 209         annotation_cp_define.type = CP_DEFINE;
 210         annotation_cp_define.annotation = &cp_define;
 211         cdsannotate(SPEC_ANALYSIS, &annotation_cp_define);
 212 }
 213 // More if there are any
 214
 215 }
 216
 217
 218 *****    Example5:    ******
 219 Commit Point Define Check
 220
 221
 222 #include <threads.h>
 223 #include <cdsannotate.h>
 224 #include <stdint.h>
 225
 226 /* Should add the __ATOMIC_RET__ if necessary */
 227 uint64_t __ATOMIC_RET = somevar.compare_exchange_explicit(...);
 228
 229
 230 /* For all the interface check at this commit point (if there is multiple
 231  * checks here) */
 232 if (COMMIT_POINT3_CONDITION) {
 233         anno_cp_define cp_define;
 234         uint64_t call_sequence_num = get(&__sequential.interface_call_sequence, tid);
 235         bool check_passed = false;
 236         cp_define.check_passed = check_passed;
 237         cp_define.interface_num = interface_num;
 238         cp_define.label_num = 3;
 239         cp_define.call_sequence_num = call_sequence_num;
 240         spec_annotation annotation_cp_define;
 241         annotation_cp_define.type = CP_DEFINE;
 242         annotation_cp_define.annotation = &cp_define;
 243         cdsannotate(SPEC_ANALYSIS, &annotation_cp_define);
 244 }
 245 // More if there are any
 246
 247 }