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