notes/generated_code_examples.txt

   1 ******    Example1:    ******
   2 Global Variable Declaration
   3
   4
   5 /* Include all the header files that contains the interface declaration */
   6 #include <iostream>
   7 #inlcude <atomic>
   8 #include <memory>
   9 #include <assert.h>
  10
  11 /* Other necessary header files */
  12 #include <specannotation.h>
  13 #include <spec_tag.h>
  14
  15 /* All other user-defined functions */
  16 ALL_USER_DEFINED_FUNCTIONS
  17
  18 /* Definition of interface info struct (per interface) */
  19 typedef struct Put_info {
  20         shared_ptr<TypeV> __RET__;
  21         TypeK & key;
  22         TypeV & value;
  23 } Put_info;
  24
  25 typedef struct Get_info {
  26         shared_ptr<TypeV> __RET__;
  27         TypeK & key;
  28 } Get_info;
  29 /* End of info struct definition */
  30
  31 /* ID functions of interface */
  32 static id_t Put_id() {
  33         id_t id = PUT_ID;
  34         return id;
  35 }
  36
  37 static id_t Get_id() {
  38         id_t id = GET_ID;
  39         return id;
  40 }
  41 /* End of ID functions */
  42
  43 /* Initialization of interface<->function_ptr table */
  44 #define INTERFACE_SIZE 2
  45 void* func_ptr_table[INTERFACE_SIZE * 2] = {
  46         CLASS
  47
  48 /* Check_action function of interfaces */
  49 bool Put_check_action(void *info, id_t __ID__) {
  50         bool check_passed;
  51         Put_info *theInfo = (Put_info) info;
  52         shared_ptr<TypeV> __RET__ = theInfo->__RET__;
  53         TypeK & key = theInfo->key;
  54         TypeV & value = theInfo->value;
  55
  56         // __COND_SAT__
  57         bool __COND_SAT__ = PUT_CONDITION;
  58
  59         // Check
  60         check_passed = PUT_CHECK_EXPRESSION;
  61         if (!check_passed)
  62                 return false;
  63
  64         // Action
  65         PUT_ACTION
  66
  67         /* DefineVars */
  68         TypeV *_Old_Val = DefineVarExpr;
  69
  70         // Post_check
  71         check_passed = PUT_POST_CHECK_EXPRESSION;
  72         if (!check_passed)
  73                 return false;
  74
  75         // Post_action
  76         PUT_POST_ACTION
  77 }
  78
  79
  80 bool Get_check_action(void *info, id_t __ID__) {
  81         //...
  82 }
  83 /* End of check_action function definitions */
  84
  85
  86 /* Beginning of other user-defined variables */
  87 bool lock_acquired;
  88 int reader_lock_cnt;
  89 /* End of other user-defined variables */
  90
  91
  92 /* Define function for sequential code initialization */
  93 void __sequential_init() {
  94         /* Init user-defined variables */
  95         lock_acquired = false;
  96         reader_lock_cnt = 0;
  97
  98         /* Pass the happens-before initialization here */
  99         /* PutIfAbsent (putIfAbsent_Succ) -> Get (true) */
 100         anno_hb_init hbConditionInit0;
 101         hbConditionInit0.interface_num_before = 1;
 102         hbConditionInit0.hb_condition_num_before = 1;
 103         hbConditionInit0.interface_num_after = 2;
 104         hbConditionInit0.hb_condition_num_after = 0;
 105         spec_annotation hb_init0;
 106         hb_init0.type = HB_INIT;
 107         hb_init0.annotation = &hbConditionInit0;
 108         cdsannotate(SPEC_ANALYSIS, &hb_init0);
 109 }
 110
 111 #endif /* End of
 112
 113
 114 ******    Example2:    ******
 115 Interface Wrapper
 116
 117 /* Include the header files first */
 118 #include <threads.h>
 119 #include <cdsannotate.h>
 120 #include <specannotation.h>
 121 #include <spec_tag.h>
 122 #include <spec_private_hashtable.h>
 123
 124 TypeReturn interfaceName(ARGType1 arg1, ARGType2 arg2)
 125 {
 126         thrd_t tid = thrd_current();
 127         uint64_t call_sequence_num = current(&__sequential.global_call_sequence);
 128         next(&__sequential.global_call_sequence);
 129         put(&__sequential.interface_call_sequence, tid, call_sequence_num);
 130
 131         // Interface begins
 132         anno_interface_boundary interface_boundary;
 133         interface_boundary.interface_num = 0; // Interface number
 134         interface_boundary.call_sequence_num = call_sequence_num;
 135         spec_annotation annotation_interface_begin;
 136         annotation_interface_begin.type = INTERFACE_BEGIN;
 137         annotation_interface_begin.annotation = &interface_boundary;
 138         cdsannotate(SPEC_ANALYSIS, &annoation_interface_begin);
 139
 140         TypeReturn __RET__ = __wrapper_interfaceName(arg1, arg2);
 141
 142         // HB conditions (if any)
 143         if (HB_CONDITION1) {
 144                 anno_hb_condition hb_condition1;
 145                 hb_condition1.interface_num = 0; // Interface number
 146                 hb_condition1.hb_condition_num = 1; // HB condition number
 147                 hb_condition1.id = __ID__;
 148                 hb_condition1.call_sequence_num = call_sequence_num;
 149                 spec_annotation annotation_hb_condition;
 150                 annotation_hb_condition.type = HB_CONDITION;
 151                 annotation_hb_condition.annotation = &hb_condition;
 152                 cdsannotate(SPEC_ANALYSIS, &annotation_hb_condition);
 153                 // And more (if any)
 154         }
 155
 156         // Interface ends
 157         spec_annotation annotation_interface_end;
 158         annotation_interface_end.type = INTERFACE_END;
 159         annotation_interface_end.annotation = &interface_boundary;
 160         cdsannotate(SPEC_ANALYSIS, &annoation_interface_end);
 161 }
 162
 163
 164 ******    Example3:    ******
 165 Potential Commit Point
 166
 167 #include <threads.h>
 168 #include <cdstrace.h>
 169 #include <cdsannotate.h>
 170 #include <spec_private_hashtable.h>
 171 #include <_sepc_sequential_genenrated.h>
 172
 173 // FIXME
 174 /* Define MACRO */
 175 #define CAS (__ATOMIC_RET__ = CAS)
 176 #define LOAD (__ATOMIC_RET__ = LOAD)
 177 #define RMW (__ATOMIC_RET__ = RMW)
 178
 179 thrd_t tid = thrd_current();
 180 if (POTENTIAL_CP_DEFINE_CONDITION) {
 181         uint64_t call_sequence_num = get(&__sequential.interface_call_sequence, tid);
 182
 183         anno_potential_cp_define potential_cp_define;
 184         potential_cp_define.interface_num = get(&__sequential.interface, tid);
 185         potential_cp_define.label_num = 1; // Commit point label number
 186         potential_cp_define.call_sequence_num = call_sequence_num;
 187         spec_annotation annotation_potential_cp_define;
 188         annotation_potential_cp_define.type = POTENTIAL_CP_DEFINE;
 189         annotation_potential_cp_define.annotation = &potential_cp_define;
 190         cdsannotate(SPEC_ANALYSIS, &annotation_potential_cp_define);
 191 }
 192 /* Undefine MACRO */
 193 #undef CAS
 194 #undef LOAD
 195 #undef RMW
 196
 197 ******    Example4:    ******
 198 Commit Point Define
 199
 200 #include <threads.h>
 201 #include <cdstrace.h>
 202 #include <cdsannotate.h>
 203 #include <spec_private_hashtable.h>
 204 #include <_spec_sequential_generated.h>
 205
 206 thrd_t __tid = thrd_current();
 207 int interface_num = get(&__sequential.interface, tid);
 208 /* For all the interface check at this commit point (if there is multiple
 209  * checks here) */
 210 /* Need to compute the relationship between labels before hand */
 211 switch (interface_num) {
 212         case 0:
 213                 // Commit point 3 <=> potentialCP 4
 214                 if (COMMIT_POINT3_CONDITION && potential_cp_satisfied(3, 4)) {
 215                         if (INTERFACE0_CHECK_CONDITION) {
 216                                 check_passed = true;
 217                         }
 218                         /* For all DefineVar of INTERFACE0 (Type id = Expr) (Type must be a
 219                          * pointer) */
 220                         /* Unfold all if there are multiple DefineVars */
 221                         Type res0 = Expr;
 222                         put(&__sequential.put__Old_Val, tid, (uint64_t) res0);
 223                         // And more...
 224
 225                         /* Compute id; If not defined, assign the default ID */
 226                         int id = INTERFACE0_ID_EXPRESSION;
 227                         put(__sequential.id, tid, id);
 228
 229                         /* Execute actions if there's any */
 230                         #define _Old_Val res0;
 231                         INTERFACE0_ACTION; // Unfolded right in place
 232                         #undef _Old_Val
 233                         // And more...
 234
 235                         anno_cp_define cp_define;
 236                         uint64_t call_sequence_num = get(&__sequential.interface_call_sequence, tid);
 237                         bool check_passed = false;
 238                         cp_define.check_passed = check_passed;
 239                         cp_define.interface_num = interface_num;
 240                         cp_define.label_num = 3;
 241                         cp_define.call_sequence_num = call_sequence_num;
 242                         spec_annotation annotation_cp_define;
 243                         annotation_cp_define.type = CP_DEFINE;
 244                         annotation_cp_define.annotation = &cp_define;
 245                         cdsannotate(SPEC_ANALYSIS, &annotation_cp_define);
 246                 }
 247                 break;
 248         case 1:
 249                 // Commit point 5 <=> potentialCP 6
 250                 if (COMMIT_POINT5_CONDITION && potential_cp_satisfied(5, 6)) {
 251                         if (INTERFACE1_CHECK_CONDITION) {
 252                                 check_passed = true;
 253                         }
 254                         // ...
 255                         // Same as the above case
 256                 }
 257                 break;
 258         default:
 259                 break;
 260 }
 261
 262
 263 *****    Example5:    ******
 264 Commit Point Define Check
 265
 266
 267 #include <threads.h>
 268 #include <cdstrace.h>
 269 #include <cdsannotate.h>
 270 #include <spec_private_hashtable.h>
 271 #include <_spec_sequential_generated.h>
 272
 273
 274 thrd_t __tid = thrd_current();
 275 int interface_num = get(&__sequential.interface, tid);
 276 /* For all the interface check at this commit point (if there is multiple
 277  * checks here) */
 278 /* Need to compute the relationship between labels before hand */
 279 switch (interface_num) {
 280         case 0:
 281                 if (COMMIT_POINT3_CONDITION) {
 282                         if (INTERFACE0_CHECK_CONDITION) {
 283                                 check_passed = true;
 284                         }
 285                         /* For all DefineVar of INTERFACE0 (Type id = Expr) (Type must be a
 286                          * pointer) */
 287                         /* Unfold all if there are multiple DefineVars */
 288                         Type res0 = Expr;
 289                         put(&__sequential.put__Old_Val, tid, (uint64_t) res0);
 290                         // And more...
 291
 292                         /* Compute id; If not defined, assign the default ID */
 293                         int id = INTERFACE0_ID_EXPRESSION;
 294                         put(__sequential.id, tid, id);
 295
 296                         /* Execute actions if there's any */
 297                         #define _Old_Val res0;
 298                         INTERFACE0_ACTION; // Unfolded right in place
 299                         #undef _Old_Val
 300                         // And more...
 301
 302                         anno_cp_define cp_define;
 303                         uint64_t call_sequence_num = get(&__sequential.interface_call_sequence, tid);
 304                         bool check_passed = false;
 305                         cp_define.check_passed = check_passed;
 306                         cp_define.interface_num = interface_num;
 307                         cp_define.label_num = 3;
 308                         cp_define.call_sequence_num = call_sequence_num;
 309                         spec_annotation annotation_cp_define;
 310                         annotation_cp_define.type = CP_DEFINE;
 311                         annotation_cp_define.annotation = &cp_define;
 312                         cdsannotate(SPEC_ANALYSIS, &annotation_cp_define);
 313                 }
 314                 break;
 315         case 1:
 316                 if (COMMIT_POINT5_CONDITION) {
 317                         if (INTERFACE1_CHECK_CONDITION) {
 318                                 check_passed = true;
 319                         }
 320                         // ...
 321                         // Same as the above case
 322                 }
 323                 break;
 324         default:
 325                 break;
 326 }