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         // FIXME:
  86         TypeReturn __RET__ = __wrapper_interfaceName(arg1, arg2);
  87         int __COND__ = get(&__sequential.condition, tid);
  88         uint64_t __ID__ = get(&__sequential.id, tid);
  89
  90         /* Post_check action, define macros for all DefineVars */
  91         #define _Old_Val (get(&__sequential.put__Old_Val, tid))
  92         // And more...
  93         bool post_check_passed = INTERFACE_POST_CHECK_CONDITION;
  94
  95         anno_post_check post_check;
  96         post_check.check_passed = post_check_passed;
  97         post_check.interface_num = interface_num;
  98         post_check.call_sequence_num = call_sequence_num;
  99         spec_annotation annotation_post_check;
 100         annotation_post_check.type = POST_CHECK;
 101         annotation_post_check.annotation = &post_check;
 102         cdsannotate(SPEC_ANALYSIS, &annotation_post_check);
 103
 104         // Post Action (if any)
 105         POST_ACTION_CODE // Unfolded in place
 106         #undef _Old_Val
 107         // And more...
 108
 109         // HB conditions (if any)
 110         if (HB_CONDITION1) {
 111                 anno_hb_condition hb_condition1;
 112                 hb_condition1.interface_num = 0; // Interface number
 113                 hb_condition1.hb_condition_num = 1; // HB condition number
 114                 hb_condition1.id = __ID__;
 115                 hb_condition1.call_sequence_num = call_sequence_num;
 116                 spec_annotation annotation_hb_condition;
 117                 annotation_hb_condition.type = HB_CONDITION;
 118                 annotation_hb_condition.annotation = &hb_condition;
 119                 cdsannotate(SPEC_ANALYSIS, &annotation_hb_condition);
 120                 // And more (if any)
 121         }
 122
 123         // Interface ends
 124         spec_annotation annotation_interface_end;
 125         annotation_interface_end.type = INTERFACE_END;
 126         annotation_interface_end.annotation = &interface_boundary;
 127         cdsannotate(SPEC_ANALYSIS, &annoation_interface_end);
 128 }
 129
 130
 131 ******    Example3:    ******
 132 Potential Commit Point
 133
 134 #include <threads.h>
 135 #include <cdstrace.h>
 136 #include <cdsannotate.h>
 137 #include <spec_private_hashtable.h>
 138 #include <_sepc_sequential_genenrated.h>
 139
 140 thrd_t tid = thrd_current();
 141 uint64_t __ATOMIC_RET__ = get_prev_value(tid);
 142 if (POTENTIAL_CP_DEFINE_CONDITION) {
 143         uint64_t call_sequence_num = get(&__sequential.interface_call_sequence, tid);
 144
 145         anno_potential_cp_define potential_cp_define;
 146         potential_cp_define.interface_num = get(&__sequential.interface, tid);
 147         potential_cp_define.label_num = 1; // Commit point label number
 148         potential_cp_define.call_sequence_num = call_sequence_num;
 149         spec_annotation annotation_potential_cp_define;
 150         annotation_potential_cp_define.type = POTENTIAL_CP_DEFINE;
 151         annotation_potential_cp_define.annotation = &potential_cp_define;
 152         cdsannotate(SPEC_ANALYSIS, &annotation_potential_cp_define);
 153 }
 154
 155 ******    Example4:    ******
 156 Commit Point Define
 157
 158 #include <threads.h>
 159 #include <cdstrace.h>
 160 #include <cdsannotate.h>
 161 #include <spec_private_hashtable.h>
 162 #include <_spec_sequential_generated.h>
 163
 164 thrd_t __tid = thrd_current();
 165 int interface_num = get(&__sequential.interface, tid);
 166 /* For all the interface check at this commit point (if there is multiple
 167  * checks here) */
 168 /* Need to compute the relationship between labels before hand */
 169 switch (interface_num) {
 170         case 0:
 171                 // Commit point 3 <=> potentialCP 4
 172                 if (COMMIT_POINT3_CONDITION && potential_cp_satisfied(3, 4)) {
 173                         if (INTERFACE0_CHECK_CONDITION) {
 174                                 check_passed = true;
 175                         }
 176                         /* For all DefineVar of INTERFACE0 (Type id = Expr) (Type must be a
 177                          * pointer) */
 178                         /* Unfold all if there are multiple DefineVars */
 179                         Type res0 = Expr;
 180                         put(&__sequential.put__Old_Val, tid, (uint64_t) res0);
 181                         // And more...
 182
 183                         /* Compute id; If not defined, assign the default ID */
 184                         int id = INTERFACE0_ID_EXPRESSION;
 185                         put(__sequential.id, tid, id);
 186
 187                         /* Execute actions if there's any */
 188                         #define _Old_Val res0;
 189                         INTERFACE0_ACTION; // Unfolded right in place
 190                         #undef _Old_Val
 191                         // And more...
 192
 193                         anno_cp_define cp_define;
 194                         uint64_t call_sequence_num = get(&__sequential.interface_call_sequence, tid);
 195                         bool check_passed = false;
 196                         cp_define.check_passed = check_passed;
 197                         cp_define.interface_num = interface_num;
 198                         cp_define.label_num = 3;
 199                         cp_define.call_sequence_num = call_sequence_num;
 200                         spec_annotation annotation_cp_define;
 201                         annotation_cp_define.type = CP_DEFINE;
 202                         annotation_cp_define.annotation = &cp_define;
 203                         cdsannotate(SPEC_ANALYSIS, &annotation_cp_define);
 204                 }
 205                 break;
 206         case 1:
 207                 // Commit point 5 <=> potentialCP 6
 208                 if (COMMIT_POINT5_CONDITION && potential_cp_satisfied(5, 6)) {
 209                         if (INTERFACE1_CHECK_CONDITION) {
 210                                 check_passed = true;
 211                         }
 212                         // ...
 213                         // Same as the above case
 214                 }
 215                 break;
 216         default:
 217                 break;
 218 }
 219
 220
 221 *****    Example5:    ******
 222 Commit Point Define Check
 223
 224
 225 #include <threads.h>
 226 #include <cdstrace.h>
 227 #include <cdsannotate.h>
 228 #include <spec_private_hashtable.h>
 229 #include <_spec_sequential_generated.h>
 230
 231
 232 thrd_t __tid = thrd_current();
 233 int interface_num = get(&__sequential.interface, tid);
 234 /* For all the interface check at this commit point (if there is multiple
 235  * checks here) */
 236 /* Need to compute the relationship between labels before hand */
 237 switch (interface_num) {
 238         case 0:
 239                 if (COMMIT_POINT3_CONDITION) {
 240                         if (INTERFACE0_CHECK_CONDITION) {
 241                                 check_passed = true;
 242                         }
 243                         /* For all DefineVar of INTERFACE0 (Type id = Expr) (Type must be a
 244                          * pointer) */
 245                         /* Unfold all if there are multiple DefineVars */
 246                         Type res0 = Expr;
 247                         put(&__sequential.put__Old_Val, tid, (uint64_t) res0);
 248                         // And more...
 249
 250                         /* Compute id; If not defined, assign the default ID */
 251                         int id = INTERFACE0_ID_EXPRESSION;
 252                         put(__sequential.id, tid, id);
 253
 254                         /* Execute actions if there's any */
 255                         #define _Old_Val res0;
 256                         INTERFACE0_ACTION; // Unfolded right in place
 257                         #undef _Old_Val
 258                         // And more...
 259
 260                         anno_cp_define cp_define;
 261                         uint64_t call_sequence_num = get(&__sequential.interface_call_sequence, tid);
 262                         bool check_passed = false;
 263                         cp_define.check_passed = check_passed;
 264                         cp_define.interface_num = interface_num;
 265                         cp_define.label_num = 3;
 266                         cp_define.call_sequence_num = call_sequence_num;
 267                         spec_annotation annotation_cp_define;
 268                         annotation_cp_define.type = CP_DEFINE;
 269                         annotation_cp_define.annotation = &cp_define;
 270                         cdsannotate(SPEC_ANALYSIS, &annotation_cp_define);
 271                 }
 272                 break;
 273         case 1:
 274                 if (COMMIT_POINT5_CONDITION) {
 275                         if (INTERFACE1_CHECK_CONDITION) {
 276                                 check_passed = true;
 277                         }
 278                         // ...
 279                         // Same as the above case
 280                 }
 281                 break;
 282         default:
 283                 break;
 284 }