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