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