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         bool __COND__ = get(&__cond, tid);
  83         uint64_t id = get(&__id, tid);
  84
  85         // HB conditions (if any)
  86         if (HB_CONDITION1) {
  87                 anno_hb_condition hb_condition1;
  88                 hb_condition1.interface_num = 0; // Interface number
  89                 hb_condition1.hb_condition_num = 1; // HB condition number
  90                 hb_condition1.id = id;
  91                 hb_condition1.call_sequence_num = call_sequence_num;
  92                 spec_annotation annotation_hb_condition;
  93                 annotation_hb_condition.type = HB_CONDITION;
  94                 annotation_hb_condition.annotation = &hb_condition;
  95                 cdsannotate(SPEC_ANALYSIS, &annotation_hb_condition);
  96                 // And more (if any)
  97         }
  98
  99         // Post check (if any)
 100         bool post_check_passed = POST_CHECK_CONDITION;
 101         anno_post_check post_check;
 102         post_check.check_passed = post_check_passed;
 103         post_check.interface_num = interface_num;
 104         post_check.call_sequence_num = call_sequence_num;
 105         spec_annotation annotation_post_check;
 106         annotation_post_check.type = POST_CHECK;
 107         annotation_post_check.annotation = &post_check;
 108         cdsannotate(SPEC_ANALYSIS, &annotation_post_check);
 109
 110         // Post Action (if any)
 111         POST_ACTION_CODE // Unfolded in place
 112
 113         // Interface ends
 114         spec_annotation annotation_interface_end;
 115         annotation_interface_end.type = INTERFACE_END;
 116         annotation_interface_end.annotation = &interface_boundary;
 117         cdsannotate(SPEC_ANALYSIS, &annoation_interface_end);
 118 }
 119
 120
 121 ******    Example4:    ******
 122 Potential Commit Point
 123
 124 #include <threads.h>
 125 #include <cdstrace.h>
 126 #include <cdsannotate.h>
 127 #include <spec_private_hashtable.h>
 128 #include <CDSName.h>
 129
 130 thrd_t __tid = thrd_current();
 131 uint64_t __ATOMIC_RET__ = get_prev_value(tid);
 132 if (POTENTIAL_CP_DEFINE_CONDITION) {
 133         uint64_t call_sequence_num = get(&__sequential.interface_call_sequence, tid);
 134         int interface_num = get(&__sequential.interface, tid);
 135         anno_potential_cp_define potential_cp_define;
 136         potential_cp_define.interface_num = interface_num;
 137         potential_cp_define.label_num = 1; // Commit point label number
 138         potential_cp_define.call_sequence_num = call_sequence_num;
 139         spec_annotation annotation_potential_cp_define;
 140         annotation_potential_cp_define.type = POTENTIAL_CP_DEFINE;
 141         annotation_potential_cp_define.annotation = &potential_cp_define;
 142         cdsannotate(SPEC_ANALYSIS, &annotation_potential_cp_define);
 143 }
 144
 145 ******    Example5:    ******
 146 Commit Point Define
 147
 148 #include <threads.h>
 149 #include <cdstrace.h>
 150 #include <cdsannotate.h>
 151 #include <spec_private_hashtable.h>
 152 #include <CDSName.h>
 153
 154 thrd_t __tid = thrd_current();
 155 int interface_num = get(&__sequential.interface, tid);
 156 /* For all the interface check at this commit point (if there is multiple
 157  * checks here) */
 158 /* Need to compute the relationship between labels before hand */
 159 switch (interface_num) {
 160         case 0:
 161                 // Commit point 3 <=> potentialCP 4
 162                 if (COMMIT_POINT3_CONDITION && potential_cp_satisfied(3, 4)) {
 163                         if (INTERFACE0_CHECK_CONDITION) {
 164                                 check_passed = true;
 165                         }
 166                         /* For all DefineVar of INTERFACE0 (Type id = Expr) */
 167                         FIXME: Type res0 = Expr;
 168                         put(__sequential.put_id, tid,
 169                         #define _Old_Val __sequential.put_id
 170                         INTERFACE0_ACTION; // Unfolded right in place
 171
 172                         anno_cp_define cp_define;
 173                         uint64_t call_sequence_num = get(&__sequential.interface_call_sequence, tid);
 174                         bool check_passed = false;
 175                         cp_define.check_passed = check_passed;
 176                         cp_define.interface_num = interface_num;
 177                         cp_define.label_num = 3;
 178                         cp_define.call_sequence_num = call_sequence_num;
 179                         spec_annotation annotation_cp_define;
 180                         annotation_cp_define.type = CP_DEFINE;
 181                         annotation_cp_define.annotation = &cp_define;
 182                         cdsannotate(SPEC_ANALYSIS, &annotation_cp_define);
 183                 }
 184                 break;
 185         case 1:
 186                 // Commit point 5 <=> potentialCP 6
 187                 if (COMMIT_POINT5_CONDITION && potential_cp_satisfied(5, 6)) {
 188                         if (INTERFACE1_CHECK_CONDITION) {
 189                                 check_passed = true;
 190                         }
 191                         INTERFACE1_ACTION; // Unfolded right in place
 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 = 5;
 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         default:
 207                 break;
 208 }
 209
 210
 211 *****    Example6:    ******
 212 Commit Point Define Check
 213