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