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