notes/generated_code_examples.txt

   1 ******    Example1:    ******
   2 Global Variable Declaration
   3
   4 /* Include all the header files that contains the interface declaration */
   5 #include <iostream>
   6 #inlcude <atomic>
   7 #include <memory>
   8 #include <assert.h>
   9
  10 /* Other necessary header files */
  11 #include <specannotation.h>
  12 #include <spec_tag.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_tag.h>
 125 #include <spec_private_hashtable.h>
 126
 127 TypeReturn interfaceName(ARGType1 arg1, ARGType2 arg2)
 128 {
 129         // Interface begins
 130         anno_interface_begin interface_begin;
 131         interface_begin.interface_num = 0; // Interface number
 132         spec_annotation annotation_interface_begin;
 133         annotation_interface_begin.type = INTERFACE_BEGIN;
 134         annotation_interface_begin.annotation = &interface_begin;
 135         cdsannotate(SPEC_ANALYSIS, &annoation_interface_begin);
 136
 137         TypeReturn __RET__ = __wrapper_interfaceName(arg1, arg2);
 138
 139         // HB conditions (if any)
 140         if (HB_CONDITION1) {
 141                 anno_hb_condition hb_condition1;
 142                 hb_condition1.interface_num = 0; // Interface number
 143                 hb_condition1.hb_condition_num = 1; // HB condition number
 144                 spec_annotation annotation_hb_condition;
 145                 annotation_hb_condition.type = HB_CONDITION;
 146                 annotation_hb_condition.annotation = &hb_condition;
 147                 cdsannotate(SPEC_ANALYSIS, &annotation_hb_condition);
 148         }
 149         // And more (if any)
 150
 151         // Interface ends
 152         spec_annotation annotation_interface_end;
 153         INTERFACE_LABEL_info info = (INTERFACE_LABEL_info*) malloc(sizeof(INTERFACE_LABEL_info));
 154         info->__RET__ = __RET__;
 155         info->arg1 = arg1;
 156         info->arg2 = arg2;
 157         anno_interface_end interface_end;
 158         interface_end.interface_num = 0; // Interface number
 159         interface_end.info = info; // Info
 160         annotation_interface_end.type = INTERFACE_END;
 161         annotation_interface_end.annotation = &interface_end;
 162         cdsannotate(SPEC_ANALYSIS, &annoation_interface_end);
 163 }
 164
 165
 166 ******    Example3:    ******
 167 Potential Commit Point
 168
 169
 170 #include <threads.h>
 171 #include <cdstrace.h>
 172 #include <cdsannotate.h>
 173 #include <spec_private_hashtable.h>
 174 #include <stdint.h>
 175
 176 /* Should add the __ATOMIC_RET__ if necessary */
 177 uint64_t __ATOMIC_RET = somevar.compare_exchange_explicit(...);
 178
 179 if (POTENTIAL_CP_DEFINE_CONDITION) {
 180         anno_potential_cp_define potential_cp_define;
 181         potential_cp_define.label_num = 1; // Commit point label number
 182         spec_annotation annotation_potential_cp_define;
 183         annotation_potential_cp_define.type = POTENTIAL_CP_DEFINE;
 184         annotation_potential_cp_define.annotation = &potential_cp_define;
 185         cdsannotate(SPEC_ANALYSIS, &annotation_potential_cp_define);
 186 }
 187
 188 ******    Example4:    ******
 189 Commit Point Define
 190
 191 #include <threads.h>
 192 #include <cdstrace.h>
 193 #include <cdsannotate.h>
 194 #include <spec_private_hashtable.h>
 195 #include <_spec_sequential_generated.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 <cdstrace.h>
 224 #include <cdsannotate.h>
 225 #include <spec_private_hashtable.h>
 226 #include <_spec_sequential_generated.h>
 227 #include <stdint.h>
 228
 229 /* Should add the __ATOMIC_RET__ if necessary */
 230 uint64_t __ATOMIC_RET = somevar.compare_exchange_explicit(...);
 231
 232
 233 /* For all the interface check at this commit point (if there is multiple
 234  * checks here) */
 235 if (COMMIT_POINT3_CONDITION) {
 236         anno_cp_define cp_define;
 237         uint64_t call_sequence_num = get(&__sequential.interface_call_sequence, tid);
 238         bool check_passed = false;
 239         cp_define.check_passed = check_passed;
 240         cp_define.interface_num = interface_num;
 241         cp_define.label_num = 3;
 242         cp_define.call_sequence_num = call_sequence_num;
 243         spec_annotation annotation_cp_define;
 244         annotation_cp_define.type = CP_DEFINE;
 245         annotation_cp_define.annotation = &cp_define;
 246         cdsannotate(SPEC_ANALYSIS, &annotation_cp_define);
 247 }
 248 // More if there are any
 249
 250 }