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