notes/generated_code_examples.txt

   1 ******    Example1:    ******
   2 Global Variable Declaration
   3
   4 /* Include the header files first
   5 ** This declaration will be written into a header file
   6 */
   7 /* @file _spec_sequential_generated.h */
   8 /* @brief automatically generated file */
   9 #ifndef __SPEC_SEQUENTIAL_GENERATED_H
  10 #define __SPEC_SEQUENTIAL_GENERATED_H
  11 #include <specannotation.h>
  12 #include <spec_tag.h>
  13
  14 /* Include all the header files that contains the interface declaration */
  15 #include <iostream>
  16 #inlcude <atomic>
  17 #include <memory>
  18 #include <assert.h>
  19
  20 /* All other user-defined functions */
  21 ALL_USER_DEFINED_FUNCTIONS
  22
  23 /* Definition of interface info struct (per interface) */
  24 typedef struct Put_info {
  25         shared_ptr<TypeV> __RET__;
  26         TypeK & key;
  27         TypeV & value;
  28 } Put_info;
  29
  30 typedef struct Get_info {
  31         shared_ptr<TypeV> __RET__;
  32         TypeK & key;
  33 } Get_info;
  34 /* End of info struct definition */
  35
  36
  37 /* All function of action and check of interfaces */
  38 bool Put_check_action(void *info) {
  39         bool check_passed;
  40         Put_info *theInfo = (Put_info) info;
  41         shared_ptr<TypeV> __RET__ = theInfo->__RET__;
  42         TypeK & key = theInfo->key;
  43         TypeV & value = theInfo->value;
  44
  45         // Check
  46         check_passed = PUT_CHECK_EXPRESSION;
  47         if (!check_passed)
  48                 return false;
  49
  50         // Action
  51         PUT_ACTION
  52
  53         /* DefineVars */
  54         TypeV *_Old_Val = DefineVarExpr;
  55
  56         // Post_check
  57         check_passed = PUT_POST_CHECK_EXPRESSION;
  58         if (!check_passed)
  59                 return false;
  60
  61         // Post_action
  62         PUT_POST_ACTION
  63 }
  64
  65 id_t Put_id() {
  66         id_t id = PUT_ID;
  67         return id;
  68 }
  69
  70
  71 /* Beginning of other user-defined variables */
  72 bool lock_acquired;
  73 int reader_lock_cnt;
  74 /* End of other user-defined variables */
  75
  76
  77 /* Define function for sequential code initialization */
  78 void __sequential_init() {
  79         /* Init user-defined variables */
  80         lock_acquired = false;
  81         reader_lock_cnt = 0;
  82
  83         /* Pass the happens-before initialization here */
  84         /* PutIfAbsent (putIfAbsent_Succ) -> Get (true) */
  85         anno_hb_init hbConditionInit0;
  86         hbConditionInit0.interface_num_before = 1;
  87         hbConditionInit0.hb_condition_num_before = 1;
  88         hbConditionInit0.interface_num_after = 2;
  89         hbConditionInit0.hb_condition_num_after = 0;
  90         spec_annotation hb_init0;
  91         hb_init0.type = HB_INIT;
  92         hb_init0.annotation = &hbConditionInit0;
  93         cdsannotate(SPEC_ANALYSIS, &hb_init0);
  94 }
  95
  96 #endif
  97
  98
  99
 100 ******    Example2:    ******
 101 Interface Wrapper
 102
 103 /* Include the header files first */
 104 #include <threads.h>
 105 #include <cdsannotate.h>
 106 #include <specannotation.h>
 107 #include <spec_tag.h>
 108 #include <spec_private_hashtable.h>
 109
 110 TypeReturn interfaceName(ARGType1 arg1, ARGType2 arg2)
 111 {
 112         thrd_t tid = thrd_current();
 113         uint64_t call_sequence_num = current(&__sequential.global_call_sequence);
 114         next(&__sequential.global_call_sequence);
 115         put(&__sequential.interface_call_sequence, tid, call_sequence_num);
 116
 117         // Interface begins
 118         anno_interface_boundary interface_boundary;
 119         interface_boundary.interface_num = 0; // Interface number
 120         interface_boundary.call_sequence_num = call_sequence_num;
 121         spec_annotation annotation_interface_begin;
 122         annotation_interface_begin.type = INTERFACE_BEGIN;
 123         annotation_interface_begin.annotation = &interface_boundary;
 124         cdsannotate(SPEC_ANALYSIS, &annoation_interface_begin);
 125
 126         TypeReturn __RET__ = __wrapper_interfaceName(arg1, arg2);
 127
 128         // HB conditions (if any)
 129         if (HB_CONDITION1) {
 130                 anno_hb_condition hb_condition1;
 131                 hb_condition1.interface_num = 0; // Interface number
 132                 hb_condition1.hb_condition_num = 1; // HB condition number
 133                 hb_condition1.id = __ID__;
 134                 hb_condition1.call_sequence_num = call_sequence_num;
 135                 spec_annotation annotation_hb_condition;
 136                 annotation_hb_condition.type = HB_CONDITION;
 137                 annotation_hb_condition.annotation = &hb_condition;
 138                 cdsannotate(SPEC_ANALYSIS, &annotation_hb_condition);
 139                 // And more (if any)
 140         }
 141
 142         // Interface ends
 143         spec_annotation annotation_interface_end;
 144         annotation_interface_end.type = INTERFACE_END;
 145         annotation_interface_end.annotation = &interface_boundary;
 146         cdsannotate(SPEC_ANALYSIS, &annoation_interface_end);
 147 }
 148
 149
 150 ******    Example3:    ******
 151 Potential Commit Point
 152
 153 #include <threads.h>
 154 #include <cdstrace.h>
 155 #include <cdsannotate.h>
 156 #include <spec_private_hashtable.h>
 157 #include <_sepc_sequential_genenrated.h>
 158
 159 // FIXME
 160 /* Define MACRO */
 161 #define CAS (__ATOMIC_RET__ = CAS)
 162 #define LOAD (__ATOMIC_RET__ = LOAD)
 163 #define RMW (__ATOMIC_RET__ = RMW)
 164
 165 thrd_t tid = thrd_current();
 166 if (POTENTIAL_CP_DEFINE_CONDITION) {
 167         uint64_t call_sequence_num = get(&__sequential.interface_call_sequence, tid);
 168
 169         anno_potential_cp_define potential_cp_define;
 170         potential_cp_define.interface_num = get(&__sequential.interface, tid);
 171         potential_cp_define.label_num = 1; // Commit point label number
 172         potential_cp_define.call_sequence_num = call_sequence_num;
 173         spec_annotation annotation_potential_cp_define;
 174         annotation_potential_cp_define.type = POTENTIAL_CP_DEFINE;
 175         annotation_potential_cp_define.annotation = &potential_cp_define;
 176         cdsannotate(SPEC_ANALYSIS, &annotation_potential_cp_define);
 177 }
 178 /* Undefine MACRO */
 179 #undef CAS
 180 #undef LOAD
 181 #undef RMW
 182
 183 ******    Example4:    ******
 184 Commit Point Define
 185
 186 #include <threads.h>
 187 #include <cdstrace.h>
 188 #include <cdsannotate.h>
 189 #include <spec_private_hashtable.h>
 190 #include <_spec_sequential_generated.h>
 191
 192 thrd_t __tid = thrd_current();
 193 int interface_num = get(&__sequential.interface, tid);
 194 /* For all the interface check at this commit point (if there is multiple
 195  * checks here) */
 196 /* Need to compute the relationship between labels before hand */
 197 switch (interface_num) {
 198         case 0:
 199                 // Commit point 3 <=> potentialCP 4
 200                 if (COMMIT_POINT3_CONDITION && potential_cp_satisfied(3, 4)) {
 201                         if (INTERFACE0_CHECK_CONDITION) {
 202                                 check_passed = true;
 203                         }
 204                         /* For all DefineVar of INTERFACE0 (Type id = Expr) (Type must be a
 205                          * pointer) */
 206                         /* Unfold all if there are multiple DefineVars */
 207                         Type res0 = Expr;
 208                         put(&__sequential.put__Old_Val, tid, (uint64_t) res0);
 209                         // And more...
 210
 211                         /* Compute id; If not defined, assign the default ID */
 212                         int id = INTERFACE0_ID_EXPRESSION;
 213                         put(__sequential.id, tid, id);
 214
 215                         /* Execute actions if there's any */
 216                         #define _Old_Val res0;
 217                         INTERFACE0_ACTION; // Unfolded right in place
 218                         #undef _Old_Val
 219                         // And more...
 220
 221                         anno_cp_define cp_define;
 222                         uint64_t call_sequence_num = get(&__sequential.interface_call_sequence, tid);
 223                         bool check_passed = false;
 224                         cp_define.check_passed = check_passed;
 225                         cp_define.interface_num = interface_num;
 226                         cp_define.label_num = 3;
 227                         cp_define.call_sequence_num = call_sequence_num;
 228                         spec_annotation annotation_cp_define;
 229                         annotation_cp_define.type = CP_DEFINE;
 230                         annotation_cp_define.annotation = &cp_define;
 231                         cdsannotate(SPEC_ANALYSIS, &annotation_cp_define);
 232                 }
 233                 break;
 234         case 1:
 235                 // Commit point 5 <=> potentialCP 6
 236                 if (COMMIT_POINT5_CONDITION && potential_cp_satisfied(5, 6)) {
 237                         if (INTERFACE1_CHECK_CONDITION) {
 238                                 check_passed = true;
 239                         }
 240                         // ...
 241                         // Same as the above case
 242                 }
 243                 break;
 244         default:
 245                 break;
 246 }
 247
 248
 249 *****    Example5:    ******
 250 Commit Point Define Check
 251
 252
 253 #include <threads.h>
 254 #include <cdstrace.h>
 255 #include <cdsannotate.h>
 256 #include <spec_private_hashtable.h>
 257 #include <_spec_sequential_generated.h>
 258
 259
 260 thrd_t __tid = thrd_current();
 261 int interface_num = get(&__sequential.interface, tid);
 262 /* For all the interface check at this commit point (if there is multiple
 263  * checks here) */
 264 /* Need to compute the relationship between labels before hand */
 265 switch (interface_num) {
 266         case 0:
 267                 if (COMMIT_POINT3_CONDITION) {
 268                         if (INTERFACE0_CHECK_CONDITION) {
 269                                 check_passed = true;
 270                         }
 271                         /* For all DefineVar of INTERFACE0 (Type id = Expr) (Type must be a
 272                          * pointer) */
 273                         /* Unfold all if there are multiple DefineVars */
 274                         Type res0 = Expr;
 275                         put(&__sequential.put__Old_Val, tid, (uint64_t) res0);
 276                         // And more...
 277
 278                         /* Compute id; If not defined, assign the default ID */
 279                         int id = INTERFACE0_ID_EXPRESSION;
 280                         put(__sequential.id, tid, id);
 281
 282                         /* Execute actions if there's any */
 283                         #define _Old_Val res0;
 284                         INTERFACE0_ACTION; // Unfolded right in place
 285                         #undef _Old_Val
 286                         // And more...
 287
 288                         anno_cp_define cp_define;
 289                         uint64_t call_sequence_num = get(&__sequential.interface_call_sequence, tid);
 290                         bool check_passed = false;
 291                         cp_define.check_passed = check_passed;
 292                         cp_define.interface_num = interface_num;
 293                         cp_define.label_num = 3;
 294                         cp_define.call_sequence_num = call_sequence_num;
 295                         spec_annotation annotation_cp_define;
 296                         annotation_cp_define.type = CP_DEFINE;
 297                         annotation_cp_define.annotation = &cp_define;
 298                         cdsannotate(SPEC_ANALYSIS, &annotation_cp_define);
 299                 }
 300                 break;
 301         case 1:
 302                 if (COMMIT_POINT5_CONDITION) {
 303                         if (INTERFACE1_CHECK_CONDITION) {
 304                                 check_passed = true;
 305                         }
 306                         // ...
 307                         // Same as the above case
 308                 }
 309                 break;
 310         default:
 311                 break;
 312 }